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) : Type u

The free ring over a type α.

Equations

• FreeRing α = FreeAbelianGroup (FreeMonoid α)

instance instRingFreeRing (α : Type u) : Ring (FreeRing α)

Equations

• instRingFreeRing α = FreeAbelianGroup.ring (FreeMonoid α)

instance instInhabitedFreeRing (α : Type u) : Inhabited (FreeRing α)

Equations

• instInhabitedFreeRing α = id inferInstance

instance instNontrivialFreeRing (α : Type u) : Nontrivial (FreeRing α)

Equations

• ⋯ = ⋯

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

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

@[simp]

theorem FreeRing.of_ne_zero {α : Type u} (x : α) : FreeRing.of x ≠ 0

@[simp]

theorem FreeRing.zero_ne_of {α : Type u} (x : α) : 0 ≠ FreeRing.of x

@[simp]

theorem FreeRing.of_ne_one {α : Type u} (x : α) : FreeRing.of x ≠ 1

@[simp]

theorem FreeRing.one_ne_of {α : Type u} (x : α) : 1 ≠ FreeRing.of x

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_iff {α : Type u} {R : Type v} [Ring R] {f : FreeRing α →+* R} {g : FreeRing α →+* R} : f = g ↔ ∀ (x : α), f (FreeRing.of x) = g (FreeRing.of x)

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)