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

If α is a type, then FreeRing α is the free ring generated by α. This is a ring equipped with a function FreeRing.of : α → FreeRing α which has the following universal property: if R is any ring, and f : α → R is any function, then this function is the composite of FreeRing.of and a unique ring homomorphism FreeRing.lift f : FreeRing α →+* R.

A typical element of FreeRing α is a ℤ-linear combination of formal products of elements of α. For example if x and y are terms of type α then 3 * x * y * x - 2 * y * x + 1 is a "typical" element of FreeRing α. In particular if α is empty then FreeRing α is isomorphic to ℤ, and if α has one term t then FreeRing α is isomorphic to the polynomial ring ℤ[t]. If α has two or more terms then FreeRing α is not commutative. One can think of FreeRing α as the free non-commutative polynomial ring with coefficients in the integers and variables indexed by α.

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 α)

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 of

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem FreeRing.induction_on {α : Type u} {C : FreeRing α → Prop} (z : FreeRing α) (hn1 : C (-1)) (hb : ∀ (b : α), C (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 : α) : (lift f) (of x) = f x

@[simp]

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

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

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

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 : α) : (map f) (of x) = of (f x)