Documentation

Mathlib.RingTheory.FreeRing

Free rings #

The theory of the free ring over a type.

Main definitions #

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
    Equations
    def FreeRing.of {α : Type u} (x : α) :

    The canonical map from α to FreeRing α.

    Equations
    Instances For
      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 xC yC (x + y)) (hm : ∀ (x y : FreeRing α), C xC yC (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
      Instances For
        @[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 : αβ) :

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

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