# 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
Instances For
instance instRingFreeRing (α : Type u) :
Ring ()
Equations
instance instInhabitedFreeRing (α : Type u) :
Equations
• = id inferInstance
def FreeRing.of {α : Type u} (x : α) :

The canonical map from α to FreeRing α.

Equations
Instances For
theorem FreeRing.induction_on {α : Type u} {C : Prop} (z : ) (hn1 : C (-1)) (hb : ∀ (b : α), C ()) (ha : ∀ (x y : ), C xC yC (x + y)) (hm : ∀ (x y : ), C xC yC (x * y)) :
C z
def FreeRing.lift {α : Type u} {R : Type v} [Ring R] :
(αR) ( →+* R)

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

Equations
• FreeRing.lift = FreeMonoid.lift.trans FreeAbelianGroup.liftMonoid
Instances For
@[simp]
theorem FreeRing.lift_of {α : Type u} {R : Type v} [Ring R] (f : αR) (x : α) :
(FreeRing.lift f) () = f x
@[simp]
theorem FreeRing.lift_comp_of {α : Type u} {R : Type v} [Ring R] (f : →+* R) :
FreeRing.lift (f FreeRing.of) = f
theorem FreeRing.hom_ext {α : Type u} {R : Type v} [Ring R] ⦃f : →+* R ⦃g : →+* R (h : ∀ (x : α), f () = g ()) :
f = g
def FreeRing.map {α : Type u} {β : Type v} (f : αβ) :

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

Equations
• = FreeRing.lift (FreeRing.of f)
Instances For
@[simp]
theorem FreeRing.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
() () = FreeRing.of (f x)