mathlib documentation

ring_theory.free_ring

Free rings

The theory of the free ring over a type.

Main definitions

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

Implementation details

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

Tags

free ring

def free_ring (α : Type u) :

Type u

The free ring over a type α.

Equations

free_ring α = free_abelian_group (free_monoid α)

@[instance]

def free_ring.ring (α : Type u) :

ring (free_ring α)

Equations

free_ring.ring α = free_abelian_group.ring (free_monoid α)

@[instance]

def free_ring.inhabited (α : Type u) :

inhabited (free_ring α)

Equations

free_ring.inhabited α = {default := 0}

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

The canonical map from α to free_ring α.

Equations

free_ring.of x = free_abelian_group.of [x]

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

C z

def free_ring.lift {α : Type u} {R : Type v} [ring R] (f : α → R) :

free_ring α →+* R

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

Equations

free_ring.lift f = {to_fun := (free_abelian_group.lift (λ (L : list α), (list.map f L).prod)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

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

⇑(free_ring.lift f) (free_ring.of x) = f x

@[simp]

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

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

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

free_ring α →+* free_ring β

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

Equations

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

@[simp]

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

⇑(free_ring.map f) (free_ring.of x) = free_ring.of (f x)