Documentation

Mathlib.RingTheory.FreeRing

Free rings #

The theory of the free ring over a type.

Main definitions #

FreeRing α : the free (not commutative in general) ring over a type.
lift (f : α → R) : the ring hom FreeRing α →+* R induced by f.
map (f : α → β) : the ring hom FreeRing α →+* FreeRing β induced by f.

Implementation details #

FreeRing α is implemented as the free abelian group over the free monoid on α.

Tags #

free ring

def FreeRing (α : Type u) :

The free ring over a type α.

Equations

FreeRing α = FreeAbelianGroup (FreeMonoid α)

Instances For

instance instRingFreeRing (α : Type u) :

Ring (FreeRing α)

Equations

instRingFreeRing α = FreeAbelianGroup.ring (FreeMonoid α)

instance instInhabitedFreeRing (α : Type u) :

Inhabited (FreeRing α)

Equations

instInhabitedFreeRing α = id inferInstance

def FreeRing.of {α : Type u} (x : α) :

The canonical map from α to FreeRing α.

Equations

FreeRing.of x = FreeAbelianGroup.of (FreeMonoid.of x)

theorem FreeRing.of_injective {α : Type u} :

Function.Injective FreeRing.of

theorem FreeRing.induction_on {α : Type u} {C : FreeRing α → Prop} (z : FreeRing α) (hn1 : C (-1)) (hb : ∀ (b : α), C (FreeRing.of b)) (ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)) (hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)) :

C z

def FreeRing.lift {α : Type u} {R : Type v} [Ring R] :

(α → R) ≃ (FreeRing α →+* R)

The ring homomorphism FreeRing α →+* R induced from a map α → R.

Equations

FreeRing.lift = FreeMonoid.lift.trans FreeAbelianGroup.liftMonoid

@[simp]

theorem FreeRing.lift_of {α : Type u} {R : Type v} [Ring R] (f : α → R) (x : α) :

(FreeRing.lift f) (FreeRing.of x) = f x

@[simp]

theorem FreeRing.lift_comp_of {α : Type u} {R : Type v} [Ring R] (f : FreeRing α →+* R) :

FreeRing.lift (⇑f ∘ FreeRing.of) = f

theorem FreeRing.hom_ext {α : Type u} {R : Type v} [Ring R] ⦃f : FreeRing α →+* R⦄ ⦃g : FreeRing α →+* R⦄ (h : ∀ (x : α), f (FreeRing.of x) = g (FreeRing.of x)) :

f = g

def FreeRing.map {α : Type u} {β : Type v} (f : α → β) :

FreeRing α →+* FreeRing β

The canonical ring homomorphism FreeRing α →+* FreeRing β generated by a map α → β.

Equations

FreeRing.map f = FreeRing.lift (FreeRing.of ∘ f)

@[simp]

theorem FreeRing.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :

(FreeRing.map f) (FreeRing.of x) = FreeRing.of (f x)