Mathlib.Algebra.FreeAlgebra

Module docstring

{"# Free Algebras

Given a commutative semiring R, and a type X, we construct the free unital, associative R-algebra on X.

Notation

FreeAlgebra R X is the free algebra itself. It is endowed with an R-algebra structure.
FreeAlgebra.ι R is the function X → FreeAlgebra R X.
Given a function f : X → A to an R-algebra A, lift R f is the lift of f to an R-algebra morphism FreeAlgebra R X → A.

Theorems

ι_comp_lift states that the composition (lift R f) ∘ (ι R) is identical to f.
lift_unique states that whenever an R-algebra morphism g : FreeAlgebra R X → A is given whose composition with ι R is f, then one has g = lift R f.
hom_ext is a variant of lift_unique in the form of an extensionality theorem.
lift_comp_ι is a combination of ι_comp_lift and lift_unique. It states that the lift of the composition of an algebra morphism with ι is the algebra morphism itself.
equivMonoidAlgebraFreeMonoid : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)
An inductive principle induction.

Implementation details

We construct the free algebra on X as a quotient of an inductive type FreeAlgebra.Pre by an inductively defined relation FreeAlgebra.Rel. Explicitly, the construction involves three steps: 1. We construct an inductive type FreeAlgebra.Pre R X, the terms of which should be thought of as representatives for the elements of FreeAlgebra R X. It is the free type with maps from R and X, and with two binary operations add and mul. 2. We construct an inductive relation FreeAlgebra.Rel R X on FreeAlgebra.Pre R X. This is the smallest relation for which the quotient is an R-algebra where addition resp. multiplication are induced by add resp. mul from 1., and for which the map from R is the structure map for the algebra. 3. The free algebra FreeAlgebra R X is the quotient of FreeAlgebra.Pre R X by the relation FreeAlgebra.Rel R X. ","Define the basic operations ","Build the semiring structure. We do this one piece at a time as this is convenient for proving the nsmul fields. ","Since we have set the basic definitions as @[Irreducible], from this point onwards one should only use the universal properties of the free algebra, and consider the actual implementation as a quotient of an inductive type as completely hidden. "}

FreeAlgebra.Pre inductive

Full source

/-- This inductive type is used to express representatives of the free algebra.
-/
inductive Pre
  | of : X → Pre
  | ofScalar : R → Pre
  | add : Pre → Pre → Pre
  | mul : Pre → Pre → Pre

Preliminary terms for free algebra construction

Informal description

The inductive type `FreeAlgebra.Pre R X` represents preliminary terms for constructing the free unital associative $R$-algebra over a type $X$. These terms are generated from: 1. Elements of the commutative semiring $R$ 2. Elements of the type $X$ 3. Binary operations `add` and `mul` representing addition and multiplication This type serves as an intermediate step before quotienting by relations that enforce the $R$-algebra structure.

FreeAlgebra.Pre.instInhabited instance

: Inhabited (Pre R X)

Full source

instance : Inhabited (Pre R X) := ⟨ofScalar 0⟩

Inhabitedness of Free Algebra Preliminary Terms

Informal description

The preliminary terms $\text{Pre}\ R\ X$ for constructing the free unital associative $R$-algebra over a type $X$ are always inhabited.

FreeAlgebra.Pre.hasCoeGenerator definition

: Coe X (Pre R X)

Full source

/-- Coercion from `X` to `Pre R X`. Note: Used for notation only. -/
def hasCoeGenerator : Coe X (Pre R X) := ⟨of⟩

Embedding of generators into free algebra preliminary terms

Informal description

The canonical embedding of an element $x$ from the type $X$ into the preliminary terms $\text{Pre}\ R\ X$ of the free algebra construction, given by the constructor $\text{of}$.

FreeAlgebra.Pre.hasCoeSemiring definition

: Coe R (Pre R X)

Full source

/-- Coercion from `R` to `Pre R X`. Note: Used for notation only. -/
def hasCoeSemiring : Coe R (Pre R X) := ⟨ofScalar⟩

Embedding of semiring elements into free algebra preliminary terms

Informal description

The canonical embedding of an element $r$ from the commutative semiring $R$ into the preliminary terms $\text{Pre}\ R\ X$ of the free algebra construction, given by the constructor $\text{ofScalar}$.

FreeAlgebra.Pre.hasMul definition

: Mul (Pre R X)

Full source

/-- Multiplication in `Pre R X` defined as `Pre.mul`. Note: Used for notation only. -/
def hasMul : Mul (Pre R X) := ⟨mul⟩

Multiplication in preliminary free algebra terms

Informal description

The multiplication operation on the preliminary terms `Pre R X` of the free algebra construction is defined using the binary operation `mul` from the inductive type `Pre R X`. This operation will later be used to induce multiplication in the quotient algebra `FreeAlgebra R X`.

FreeAlgebra.Pre.hasAdd definition

: Add (Pre R X)

Full source

/-- Addition in `Pre R X` defined as `Pre.add`. Note: Used for notation only. -/
def hasAdd : Add (Pre R X) := ⟨add⟩

Addition in preliminary free algebra terms

Informal description

The addition operation on the preliminary terms `Pre R X` of the free algebra construction is defined using the binary operation `add` from the inductive type `Pre R X`. This operation will later be used to induce addition in the quotient algebra `FreeAlgebra R X`.

FreeAlgebra.Pre.hasZero definition

: Zero (Pre R X)

Full source

/-- Zero in `Pre R X` defined as the image of `0` from `R`. Note: Used for notation only. -/
def hasZero : Zero (Pre R X) := ⟨ofScalar 0⟩

Zero element in free algebra preliminary terms

Informal description

The zero element in the preliminary terms `Pre R X` of the free algebra construction is defined as the image of the zero element from the commutative semiring $R$ under the canonical embedding `ofScalar`.

FreeAlgebra.Pre.hasOne definition

: One (Pre R X)

Full source

/-- One in `Pre R X` defined as the image of `1` from `R`. Note: Used for notation only. -/
def hasOne : One (Pre R X) := ⟨ofScalar 1⟩

Multiplicative identity in free algebra preliminary terms

Informal description

The multiplicative identity element in the preliminary terms `Pre R X` of the free algebra construction is defined as the image of the multiplicative identity $1$ from the commutative semiring $R$ under the canonical embedding `ofScalar`.

FreeAlgebra.Pre.hasSMul definition

: SMul R (Pre R X)

Full source

/-- Scalar multiplication defined as multiplication by the image of elements from `R`.
Note: Used for notation only.
-/
def hasSMul : SMul R (Pre R X) := ⟨fun r m ↦ mul (ofScalar r) m⟩

Scalar multiplication on free algebra preliminary terms

Informal description

The scalar multiplication operation on the preliminary terms `Pre R X` of the free algebra construction is defined as multiplication by the image of elements from the commutative semiring `R`. Specifically, for any element `r ∈ R` and any term `m ∈ Pre R X`, the scalar multiplication `r • m` is given by the product of the scalar term `ofScalar r` with `m`.

FreeAlgebra.liftFun definition

{A : Type*} [Semiring A] [Algebra R A] (f : X → A) : Pre R X → A

Full source

/-- Given a function from `X` to an `R`-algebra `A`, `lift_fun` provides a lift of `f` to a function
from `Pre R X` to `A`. This is mainly used in the construction of `FreeAlgebra.lift`. -/
def liftFun {A : Type*} [Semiring A] [Algebra R A] (f : X → A) :
    Pre R X → A
  | .of t => f t
  | .add a b => liftFun f a + liftFun f b
  | .mul a b => liftFun f a * liftFun f b
  | .ofScalar c => algebraMap _ _ c

Lifting function for free algebra construction

Informal description

Given a commutative semiring $R$, a type $X$, and an $R$-algebra $A$ with a function $f : X \to A$, the function $\text{liftFun}\, f$ maps preliminary terms in $\text{Pre}\, R\, X$ to elements of $A$ as follows: 1. For terms $\text{of}\, t$ (where $t \in X$), it applies $f$ directly: $\text{liftFun}\, f\, (\text{of}\, t) = f\, t$ 2. For addition terms $\text{add}\, a\, b$, it adds the lifted results: $\text{liftFun}\, f\, (\text{add}\, a\, b) = \text{liftFun}\, f\, a + \text{liftFun}\, f\, b$ 3. For multiplication terms $\text{mul}\, a\, b$, it multiplies the lifted results: $\text{liftFun}\, f\, (\text{mul}\, a\, b) = \text{liftFun}\, f\, a \times \text{liftFun}\, f\, b$ 4. For scalar terms $\text{ofScalar}\, c$ (where $c \in R$), it uses the algebra map: $\text{liftFun}\, f\, (\text{ofScalar}\, c) = \text{algebraMap}\, R\, A\, c$ This function serves as the foundation for constructing the universal lift of $f$ to an $R$-algebra homomorphism from the free algebra.

FreeAlgebra.Rel inductive

 :
  Pre R X →
    Pre R X →
      Prop
        -- force `ofScalar` to be a central semiring morphism

Full source

/-- An inductively defined relation on `Pre R X` used to force the initial algebra structure on
the associated quotient.
-/
inductive Rel : Pre R X → Pre R X → Prop
  -- force `ofScalar` to be a central semiring morphism
  | add_scalar {r s : R} : Rel (↑(r + s)) (↑r + ↑s)
  | mul_scalar {r s : R} : Rel (↑(r * s)) (↑r * ↑s)
  | central_scalar {r : R} {a : Pre R X} : Rel (r * a) (a * r)

  -- commutative additive semigroup
  | add_assoc {a b c : Pre R X} : Rel (a + b + c) (a + (b + c))
  | add_comm {a b : Pre R X} : Rel (a + b) (b + a)
  | zero_add {a : Pre R X} : Rel (0 + a) a

  -- multiplicative monoid
  | mul_assoc {a b c : Pre R X} : Rel (a * b * c) (a * (b * c))
  | one_mul {a : Pre R X} : Rel (1 * a) a
  | mul_one {a : Pre R X} : Rel (a * 1) a

  -- distributivity
  | left_distrib {a b c : Pre R X} : Rel (a * (b + c)) (a * b + a * c)
  | right_distrib {a b c : Pre R X} :
      Rel ((a + b) * c) (a * c + b * c)

  -- other relations needed for semiring
  | zero_mul {a : Pre R X} : Rel (0 * a) 0
  | mul_zero {a : Pre R X} : Rel (a * 0) 0

  -- compatibility
  | add_compat_left {a b c : Pre R X} : Rel a b → Rel (a + c) (b + c)
  | add_compat_right {a b c : Pre R X} : Rel a b → Rel (c + a) (c + b)
  | mul_compat_left {a b c : Pre R X} : Rel a b → Rel (a * c) (b * c)
  | mul_compat_right {a b c : Pre R X} : Rel a b → Rel (c * a) (c * b)

Relation for Free Algebra Construction

Informal description

The inductive relation `FreeAlgebra.Rel R X` on `FreeAlgebra.Pre R X` is the smallest relation that enforces the structure of an $R$-algebra on the quotient `FreeAlgebra R X`. Specifically, it ensures that: 1. The map from $R$ is a central semiring morphism. 2. The binary operations `add` and `mul` on `Pre R X` induce the addition and multiplication operations on the quotient algebra. This relation is used to construct the free unital associative $R$-algebra over $X$ by taking the quotient of `Pre R X` by `Rel R X`.

FreeAlgebra definition

Full source

/--
If `α` is a type, and `R` is a commutative semiring, then `FreeAlgebra R α` is the
free (unital, associative) `R`-algebra generated by `α`.
This is an `R`-algebra equipped with a function `FreeAlgebra.ι R : α → FreeAlgebra R α` which has
the following universal property: if `A` is any `R`-algebra, and `f : α → A` is any function,
then this function is the composite of `FreeAlgebra.ι R` and a unique `R`-algebra homomorphism
`FreeAlgebra.lift R f : FreeAlgebra R α →ₐ[R] A`.

A typical element of `FreeAlgebra R α` is an `R`-linear
combination of formal products of elements of `α`.
For example if `x` and `y` are terms of type `α` and `a`, `b` are terms of type `R` then
`(3 * a * a) • (x * y * x) + (2 * b + 1) • (y * x) + (a * b * b + 3)` is a
"typical" element of `FreeAlgebra R α`. In particular if `α` is empty
then `FreeAlgebra R α` is isomorphic to `R`, and if `α` has one term `t`
then `FreeAlgebra R α` is isomorphic to the polynomial ring `R[t]`.
If `α` has two or more terms then `FreeAlgebra R α` is not commutative.
One can think of `FreeAlgebra R α` as the free non-commutative polynomial ring
with coefficients in `R` and variables indexed by `α`.
-/
def FreeAlgebra :=
  Quot (FreeAlgebra.Rel R X)

Free unital associative algebra over a commutative semiring

Informal description

Given a commutative semiring $R$ and a type $X$, the free (unital, associative) $R$-algebra generated by $X$, denoted $\text{FreeAlgebra}\, R\, X$, is constructed as the quotient of the inductive type $\text{Pre}\, R\, X$ by the relation $\text{Rel}\, R\, X$. This algebra satisfies the universal property that for any $R$-algebra $A$ and any function $f : X \to A$, there exists a unique $R$-algebra homomorphism $\text{lift}\, R\, f : \text{FreeAlgebra}\, R\, X \to A$ such that the composition $(\text{lift}\, R\, f) \circ (\iota\, R)$ equals $f$, where $\iota\, R : X \to \text{FreeAlgebra}\, R\, X$ is the inclusion map. Elements of $\text{FreeAlgebra}\, R\, X$ can be thought of as $R$-linear combinations of formal (non-commutative) products of elements from $X$. For example, if $x, y \in X$ and $a, b \in R$, then $(3a^2) \cdot (xyx) + (2b + 1) \cdot (yx) + (ab^2 + 3)$ is a typical element.

FreeAlgebra.instSMul instance

{A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X)

Full source

instance instSMul {A} [CommSemiring A] [Algebra R A] : SMul R (FreeAlgebra A X) where
  smul r := Quot.map (HMul.hMul (algebraMap R A r : Pre A X)) fun _ _ ↦ Rel.mul_compat_right

Scalar Multiplication on Free Algebra

Informal description

For any commutative semiring $A$ equipped with an $R$-algebra structure, the free algebra $\text{FreeAlgebra}\, A\, X$ has a scalar multiplication operation by elements of $R$.

FreeAlgebra.instZero instance

: Zero (FreeAlgebra R X)

Full source

instance instZero : Zero (FreeAlgebra R X) where zero := Quot.mk _ 0

Zero Element in Free Algebra

Informal description

The free algebra $\text{FreeAlgebra}\, R\, X$ has a zero element.

FreeAlgebra.instOne instance

: One (FreeAlgebra R X)

Full source

instance instOne : One (FreeAlgebra R X) where one := Quot.mk _ 1

Multiplicative Identity in Free Algebra

Informal description

The free algebra $\text{FreeAlgebra}\, R\, X$ has a multiplicative identity element.

FreeAlgebra.instAdd instance

: Add (FreeAlgebra R X)

Full source

instance instAdd : Add (FreeAlgebra R X) where
  add := Quot.map₂ HAdd.hAdd (fun _ _ _ ↦ Rel.add_compat_right) fun _ _ _ ↦ Rel.add_compat_left

Addition in the Free Algebra

Informal description

The free unital associative $R$-algebra $\text{FreeAlgebra}\, R\, X$ is equipped with an addition operation.

FreeAlgebra.instMul instance

: Mul (FreeAlgebra R X)

Full source

instance instMul : Mul (FreeAlgebra R X) where
  mul := Quot.map₂ HMul.hMul (fun _ _ _ ↦ Rel.mul_compat_right) fun _ _ _ ↦ Rel.mul_compat_left

Multiplication Operation in Free Algebra

Informal description

The free unital associative $R$-algebra $\text{FreeAlgebra}\, R\, X$ is equipped with a multiplication operation, which is induced from the multiplication operation on the preliminary terms $\text{Pre}\, R\, X$ via the quotient construction.

FreeAlgebra.instMonoidWithZero instance

: MonoidWithZero (FreeAlgebra R X)

Full source

instance instMonoidWithZero : MonoidWithZero (FreeAlgebra R X) where
  mul_assoc := by
    rintro ⟨⟩ ⟨⟩ ⟨⟩
    exact Quot.sound Rel.mul_assoc
  one := Quot.mk _ 1
  one_mul := by
    rintro ⟨⟩
    exact Quot.sound Rel.one_mul
  mul_one := by
    rintro ⟨⟩
    exact Quot.sound Rel.mul_one
  zero_mul := by
    rintro ⟨⟩
    exact Quot.sound Rel.zero_mul
  mul_zero := by
    rintro ⟨⟩
    exact Quot.sound Rel.mul_zero

Free Algebra as a Monoid with Zero

Informal description

The free unital associative $R$-algebra $\text{FreeAlgebra}\, R\, X$ is a monoid with zero, meaning it has a multiplicative identity (1) and a zero element (0), and multiplication is associative and distributes over addition.

FreeAlgebra.instDistrib instance

: Distrib (FreeAlgebra R X)

Full source

instance instDistrib : Distrib (FreeAlgebra R X) where
  left_distrib := by
    rintro ⟨⟩ ⟨⟩ ⟨⟩
    exact Quot.sound Rel.left_distrib
  right_distrib := by
    rintro ⟨⟩ ⟨⟩ ⟨⟩
    exact Quot.sound Rel.right_distrib

Distributivity in the Free Algebra

Informal description

The free unital associative $R$-algebra $\text{FreeAlgebra}\, R\, X$ is equipped with a distributive structure, meaning that multiplication distributes over addition. Specifically, for any elements $a, b, c \in \text{FreeAlgebra}\, R\, X$, the following identities hold: - $a \cdot (b + c) = a \cdot b + a \cdot c$ (left distributivity) - $(a + b) \cdot c = a \cdot c + b \cdot c$ (right distributivity)

FreeAlgebra.instAddCommMonoid instance

: AddCommMonoid (FreeAlgebra R X)

Full source

instance instAddCommMonoid : AddCommMonoid (FreeAlgebra R X) where
  add_assoc := by
    rintro ⟨⟩ ⟨⟩ ⟨⟩
    exact Quot.sound Rel.add_assoc
  zero_add := by
    rintro ⟨⟩
    exact Quot.sound Rel.zero_add
  add_zero := by
    rintro ⟨⟩
    change Quot.mk _ _ = _
    rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]
  add_comm := by
    rintro ⟨⟩ ⟨⟩
    exact Quot.sound Rel.add_comm
  nsmul := (· • ·)
  nsmul_zero := by
    rintro ⟨⟩
    change Quot.mk _ (_ * _) = _
    rw [map_zero]
    exact Quot.sound Rel.zero_mul
  nsmul_succ n := by
    rintro ⟨a⟩
    dsimp only [HSMul.hSMul, instSMul, Quot.map]
    rw [map_add, map_one, mk_mul, mk_mul, ← add_one_mul (_ : FreeAlgebra R X)]
    congr 1
    exact Quot.sound Rel.add_scalar

Commutative Monoid Structure of Addition in Free Algebra

Informal description

The free unital associative $R$-algebra $\text{FreeAlgebra}\, R\, X$ is equipped with a commutative monoid structure under addition. This means that addition in the free algebra is associative, commutative, and has a zero element that acts as an additive identity.

FreeAlgebra.instSemiring instance

: Semiring (FreeAlgebra R X)

Full source

instance : Semiring (FreeAlgebra R X) where
  __ := instMonoidWithZero R X
  __ := instAddCommMonoid R X
  __ := instDistrib R X
  natCast n := Quot.mk _ (n : R)
  natCast_zero := by simp; rfl
  natCast_succ n := by simpa using Quot.sound Rel.add_scalar

Semiring Structure on the Free Algebra

Informal description

The free unital associative $R$-algebra $\text{FreeAlgebra}\, R\, X$ is a semiring, meaning it is equipped with associative and commutative addition, associative multiplication with a multiplicative identity, and multiplication that distributes over addition.

FreeAlgebra.instInhabited instance

: Inhabited (FreeAlgebra R X)

Full source

instance : Inhabited (FreeAlgebra R X) :=
  ⟨0⟩

Inhabitedness of the Free Algebra

Informal description

The free algebra $\text{FreeAlgebra}\, R\, X$ is an inhabited type, meaning it contains at least one element.

FreeAlgebra.instAlgebra instance

{A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra A X)

Full source

instance instAlgebra {A} [CommSemiring A] [Algebra R A] : Algebra R (FreeAlgebra A X) where
  algebraMap := ({
      toFun := fun r => Quot.mk _ r
      map_one' := rfl
      map_mul' := fun _ _ => Quot.sound Rel.mul_scalar
      map_zero' := rfl
      map_add' := fun _ _ => Quot.sound Rel.add_scalar } : A →+* FreeAlgebra A X).comp
      (algebraMap R A)
  commutes' _ := by
    rintro ⟨⟩
    exact Quot.sound Rel.central_scalar
  smul_def' _ _ := rfl

$R$-Algebra Structure on Free Algebra over $A$

Informal description

For any commutative semiring $A$ equipped with an $R$-algebra structure, the free algebra $\text{FreeAlgebra}\, A\, X$ inherits an $R$-algebra structure.

FreeAlgebra.instIsScalarTower instance

 {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [SMul R S] [Algebra R A] [Algebra S A]
  [IsScalarTower R S A] : IsScalarTower R S (FreeAlgebra A X)

Full source

instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A]
    [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] :
    IsScalarTower R S (FreeAlgebra A X) where
  smul_assoc r s x := by
    change algebraMap S A (r • s) • x = algebraMap R A _ • (algebraMap S A _ • x)
    rw [← smul_assoc]
    congr
    simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
    rw [smul_assoc, ← smul_one_mul]

Scalar Tower Property for Free Algebras

Informal description

For commutative semirings $R$, $S$, and $A$, where $A$ is equipped with both $R$-algebra and $S$-algebra structures, and with a scalar multiplication operation $R \times S \to S$ that forms a scalar tower (i.e., $(r \cdot s) \cdot a = r \cdot (s \cdot a)$ for all $r \in R$, $s \in S$, $a \in A$), the free algebra $\text{FreeAlgebra}\, A\, X$ also forms a scalar tower with respect to $R$ and $S$. This means that for any $r \in R$, $s \in S$, and $x \in \text{FreeAlgebra}\, A\, X$, the scalar multiplications satisfy $(r \cdot s) \cdot x = r \cdot (s \cdot x)$.

FreeAlgebra.instSMulCommClass instance

 {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] :
  SMulCommClass R S (FreeAlgebra A X)

Full source

instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [Algebra R A] [Algebra S A] :
    SMulCommClass R S (FreeAlgebra A X) where
  smul_comm r s x := smul_comm (algebraMap R A r) (algebraMap S A s) x

Commutativity of Scalar Multiplication in Free Algebra

Informal description

For any commutative semirings $R$ and $S$, and a commutative semiring $A$ equipped with both $R$-algebra and $S$-algebra structures, the scalar multiplications by $R$ and $S$ on the free algebra $\text{FreeAlgebra}\, A\, X$ commute. That is, for any $r \in R$, $s \in S$, and $x \in \text{FreeAlgebra}\, A\, X$, we have $r \cdot (s \cdot x) = s \cdot (r \cdot x)$.

FreeAlgebra.instRing instance

{S : Type*} [CommRing S] : Ring (FreeAlgebra S X)

Full source

instance {S : Type*} [CommRing S] : Ring (FreeAlgebra S X) :=
  Algebra.semiringToRing S

Ring Structure on the Free Algebra over a Commutative Ring

Informal description

For any commutative ring $S$, the free unital associative $S$-algebra $\text{FreeAlgebra}\, S\, X$ is a ring. This means it is equipped with associative and commutative addition, associative multiplication with a multiplicative identity, and multiplication that distributes over addition, along with additive inverses.

FreeAlgebra.ι definition

Full source

/-- The canonical function `X → FreeAlgebra R X`.
-/
irreducible_def ι : X → FreeAlgebra R X := fun m ↦ Quot.mk _ m

Inclusion map into the free algebra

Informal description

The canonical inclusion map $\iota : X \to \text{FreeAlgebra}\, R\, X$ sends an element $m \in X$ to its equivalence class in the free algebra over $R$ generated by $X$.

FreeAlgebra.ι_def theorem

: eta_helper Eq✝ @ι.{} @(delta% @definition✝)

Full source

/-- The canonical function `X → FreeAlgebra R X`.
-/
irreducible_def ι : X → FreeAlgebra R X := fun m ↦ Quot.mk _ m

Definition of the inclusion map into free algebra

Informal description

The definition of the inclusion map $\iota : X \to \text{FreeAlgebra}\, R\, X$ is given by $\iota(m) = [m]$, where $[m]$ denotes the equivalence class of $m \in X$ in the quotient algebra $\text{FreeAlgebra}\, R\, X$.

FreeAlgebra.quot_mk_eq_ι theorem

(m : X) : Quot.mk (FreeAlgebra.Rel R X) m = ι R m

Full source

@[simp]
theorem quot_mk_eq_ι (m : X) : Quot.mk (FreeAlgebra.Rel R X) m = ι R m := by rw [ι_def]

Equivalence of Quotient Map and Inclusion in Free Algebra

Informal description

For any element $m$ in the type $X$, the equivalence class of $m$ in the quotient algebra $\text{FreeAlgebra}\, R\, X$ (constructed via the relation $\text{Rel}\, R\, X$) is equal to the image of $m$ under the inclusion map $\iota : X \to \text{FreeAlgebra}\, R\, X$. In other words, $[m] = \iota(m)$, where $[m]$ denotes the equivalence class of $m$ in the quotient.

FreeAlgebra.lift definition

: (X → A) ≃ (FreeAlgebra R X →ₐ[R] A)

Full source

/-- Given a function `f : X → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
of `f` to a morphism of `R`-algebras `FreeAlgebra R X → A`. -/
@[irreducible]
def lift : (X → A) ≃ (FreeAlgebra R X →ₐ[R] A) :=
  { toFun := liftAux R
    invFun := fun F ↦ F ∘ ι R
    left_inv := fun f ↦ by
      ext
      simp only [Function.comp_apply, ι_def]
      rfl
    right_inv := fun F ↦ by
      ext t
      rcases t with ⟨x⟩
      induction x with
      | of =>
        change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
        simp only [Function.comp_apply, ι_def]
      | ofScalar x =>
        change algebraMap _ _ x = F (algebraMap _ _ x)
        rw [AlgHom.commutes F _]
      | add a b ha hb =>
        -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
        -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
        rw [map_add, map_add, ha, hb]
      | mul a b ha hb =>
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        rw [map_mul, map_mul, ha, hb] }

Universal property of the free algebra

Informal description

Given a commutative semiring $R$, a type $X$, and an $R$-algebra $A$, the function $\text{lift}\, R$ maps any function $f : X \to A$ to the unique $R$-algebra homomorphism $\text{FreeAlgebra}\, R\, X \to A$ that extends $f$. More precisely, $\text{lift}\, R\, f$ is the unique $R$-algebra homomorphism such that the composition $(\text{lift}\, R\, f) \circ (\iota\, R)$ equals $f$, where $\iota\, R : X \to \text{FreeAlgebra}\, R\, X$ is the canonical inclusion map. This construction establishes a bijective correspondence between functions $X \to A$ and $R$-algebra homomorphisms $\text{FreeAlgebra}\, R\, X \to A$.

FreeAlgebra.liftAux_eq theorem

(f : X → A) : liftAux R f = lift R f

Full source

@[simp]
theorem liftAux_eq (f : X → A) : liftAux R f = lift R f := by
  rw [lift]
  rfl

Equality of Auxiliary and Universal Lift Functions in Free Algebra

Informal description

For any function $f : X \to A$ from a type $X$ to an $R$-algebra $A$, the auxiliary lift function $\text{liftAux}\, R\, f$ is equal to the universal lift $\text{lift}\, R\, f$ from the free algebra $\text{FreeAlgebra}\, R\, X$ to $A$.

FreeAlgebra.lift_symm_apply theorem

(F : FreeAlgebra R X →ₐ[R] A) : (lift R).symm F = F ∘ ι R

Full source

@[simp]
theorem lift_symm_apply (F : FreeAlgebraFreeAlgebra R X →ₐ[R] A) : (lift R).symm F = F ∘ ι R := by
  rw [lift]
  rfl

Inverse of Lift Map Equals Composition with Inclusion

Informal description

For any $R$-algebra homomorphism $F : \text{FreeAlgebra}\, R\, X \to A$, the inverse of the lift map $\text{lift}\, R$ evaluated at $F$ equals the composition $F \circ \iota\, R$, where $\iota\, R : X \to \text{FreeAlgebra}\, R\, X$ is the canonical inclusion map.

FreeAlgebra.ι_comp_lift theorem

(f : X → A) : (lift R f : FreeAlgebra R X → A) ∘ ι R = f

Full source

@[simp]
theorem ι_comp_lift (f : X → A) : (lift R f : FreeAlgebra R X → A) ∘ ι R = f := by
  ext
  rw [Function.comp_apply, ι_def, lift]
  rfl

Compatibility of Lift with Inclusion: $(\text{lift}_R\, f) \circ \iota_R = f$

Informal description

For any function $f \colon X \to A$ to an $R$-algebra $A$, the composition of the lifted algebra homomorphism $\text{lift}_R\, f \colon \text{FreeAlgebra}\, R\, X \to A$ with the inclusion map $\iota_R \colon X \to \text{FreeAlgebra}\, R\, X$ equals $f$. In other words, $(\text{lift}_R\, f) \circ \iota_R = f$.

FreeAlgebra.lift_ι_apply theorem

(f : X → A) (x) : lift R f (ι R x) = f x

Full source

@[simp]
theorem lift_ι_apply (f : X → A) (x) : lift R f (ι R x) = f x := by
  rw [ι_def, lift]
  rfl

Evaluation of the lift on generators: $\text{lift}_R f (\iota_R x) = f(x)$

Informal description

For any function $f \colon X \to A$ to an $R$-algebra $A$ and any element $x \in X$, the lift of $f$ to an $R$-algebra homomorphism $\text{lift}_R f \colon \text{FreeAlgebra}\, R\, X \to A$ satisfies $\text{lift}_R f (\iota_R x) = f(x)$, where $\iota_R \colon X \to \text{FreeAlgebra}\, R\, X$ is the canonical inclusion map.

FreeAlgebra.lift_unique theorem

(f : X → A) (g : FreeAlgebra R X →ₐ[R] A) : (g : FreeAlgebra R X → A) ∘ ι R = f ↔ g = lift R f

Full source

@[simp]
theorem lift_unique (f : X → A) (g : FreeAlgebraFreeAlgebra R X →ₐ[R] A) :
    (g : FreeAlgebra R X → A) ∘ ι R(g : FreeAlgebra R X → A) ∘ ι R = f ↔ g = lift R f := by
  rw [← (lift R).symm_apply_eq, lift]
  rfl

Uniqueness of the Lift in the Free Algebra Universal Property

Informal description

Let $R$ be a commutative semiring, $X$ a type, and $A$ an $R$-algebra. Given a function $f : X \to A$ and an $R$-algebra homomorphism $g : \text{FreeAlgebra}\, R\, X \to A$, the composition $g \circ \iota$ equals $f$ if and only if $g$ is equal to the lift of $f$, i.e., $g = \text{lift}\, R\, f$, where $\iota : X \to \text{FreeAlgebra}\, R\, X$ is the canonical inclusion map.

FreeAlgebra.lift_comp_ι theorem

(g : FreeAlgebra R X →ₐ[R] A) : lift R ((g : FreeAlgebra R X → A) ∘ ι R) = g

Full source

@[simp]
theorem lift_comp_ι (g : FreeAlgebraFreeAlgebra R X →ₐ[R] A) :
    lift R ((g : FreeAlgebra R X → A) ∘ ι R) = g := by
  rw [← lift_symm_apply]
  exact (lift R).apply_symm_apply g

Lift of Composition with Inclusion Equals Original Homomorphism

Informal description

For any $R$-algebra homomorphism $g \colon \text{FreeAlgebra}\, R\, X \to A$, the lift of the composition $g \circ \iota_R$ equals $g$, where $\iota_R \colon X \to \text{FreeAlgebra}\, R\, X$ is the canonical inclusion map.

FreeAlgebra.hom_ext theorem

 {f g : FreeAlgebra R X →ₐ[R] A} (w : (f : FreeAlgebra R X → A) ∘ ι R = (g : FreeAlgebra R X → A) ∘ ι R) : f = g

Full source

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem hom_ext {f g : FreeAlgebraFreeAlgebra R X →ₐ[R] A}
    (w : (f : FreeAlgebra R X → A) ∘ ι R = (g : FreeAlgebra R X → A) ∘ ι R) : f = g := by
  rw [← lift_symm_apply, ← lift_symm_apply] at w
  exact (lift R).symm.injective w

Extensionality of Free Algebra Homomorphisms via Inclusion Map

Informal description

Let $R$ be a commutative semiring, $X$ a type, and $A$ an $R$-algebra. For any two $R$-algebra homomorphisms $f, g : \text{FreeAlgebra}\, R\, X \to A$, if their compositions with the inclusion map $\iota R : X \to \text{FreeAlgebra}\, R\, X$ are equal (i.e., $f \circ \iota R = g \circ \iota R$), then $f = g$.

FreeAlgebra.equivMonoidAlgebraFreeMonoid definition

: FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X)

Full source

/-- The free algebra on `X` is "just" the monoid algebra on the free monoid on `X`.

This would be useful when constructing linear maps out of a free algebra,
for example.
-/
noncomputable def equivMonoidAlgebraFreeMonoid :
    FreeAlgebraFreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X) :=
  AlgEquiv.ofAlgHom (lift R fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
    ((MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (FreeMonoid.lift (ι R)))
    (by
      apply MonoidAlgebra.algHom_ext; intro x
      refine FreeMonoid.recOn x ?_ ?_
      · simp
        rfl
      · intro x y ih
        simp at ih
        simp [ih])
    (by
      ext
      simp)

Isomorphism between free algebra and monoid algebra of free monoid

Informal description

The algebra equivalence $\text{FreeAlgebra}\, R\, X \simeq_{\text{Alg}[R]} \text{MonoidAlgebra}\, R\, (\text{FreeMonoid}\, X)$ establishes an isomorphism between the free $R$-algebra on $X$ and the monoid algebra of the free monoid on $X$ over $R$. This equivalence is constructed via two algebra homomorphisms: 1. The forward map lifts the inclusion $X \to \text{MonoidAlgebra}\, R\, (\text{FreeMonoid}\, X)$ to an algebra homomorphism $\text{FreeAlgebra}\, R\, X \to \text{MonoidAlgebra}\, R\, (\text{FreeMonoid}\, X)$. 2. The backward map extends the monoid homomorphism $\text{FreeMonoid}\, X \to \text{FreeAlgebra}\, R\, X$ (induced by $\iota R$) to an algebra homomorphism $\text{MonoidAlgebra}\, R\, (\text{FreeMonoid}\, X) \to \text{FreeAlgebra}\, R\, X$. The composition of these maps in both directions yields the identity, proving the equivalence.

FreeAlgebra.instNontrivial instance

[Nontrivial R] : Nontrivial (FreeAlgebra R X)

Full source

/-- `FreeAlgebra R X` is nontrivial when `R` is. -/
instance [Nontrivial R] : Nontrivial (FreeAlgebra R X) :=
  equivMonoidAlgebraFreeMonoid.surjective.nontrivial

Nontriviality of Free Algebras over Nontrivial Semirings

Informal description

For any nontrivial commutative semiring $R$ and any type $X$, the free algebra $\text{FreeAlgebra}\, R\, X$ is also nontrivial.

FreeAlgebra.instNoZeroDivisors instance

[NoZeroDivisors R] : NoZeroDivisors (FreeAlgebra R X)

Full source

/-- `FreeAlgebra R X` has no zero-divisors when `R` has no zero-divisors. -/
instance instNoZeroDivisors [NoZeroDivisors R] : NoZeroDivisors (FreeAlgebra R X) :=
  equivMonoidAlgebraFreeMonoid.toMulEquiv.noZeroDivisors

Free Algebra Preserves No Zero-Divisors Property

Informal description

For any commutative semiring $R$ with no zero-divisors and any type $X$, the free algebra $\text{FreeAlgebra}\, R\, X$ has no zero-divisors. That is, if $a, b \in \text{FreeAlgebra}\, R\, X$ satisfy $a \cdot b = 0$, then either $a = 0$ or $b = 0$.

FreeAlgebra.instIsDomain instance

{R X} [CommRing R] [IsDomain R] : IsDomain (FreeAlgebra R X)

Full source

/-- `FreeAlgebra R X` is a domain when `R` is an integral domain. -/
instance instIsDomain {R X} [CommRing R] [IsDomain R] : IsDomain (FreeAlgebra R X) :=
  NoZeroDivisors.to_isDomain _

Free Algebras over Domains are Domains

Informal description

For any commutative domain $R$ and any type $X$, the free algebra $\text{FreeAlgebra}\, R\, X$ is also a domain. That is, it is a nontrivial ring with no zero-divisors.

FreeAlgebra.algebraMapInv definition

: FreeAlgebra R X →ₐ[R] R

Full source

/-- The left-inverse of `algebraMap`. -/
def algebraMapInv : FreeAlgebraFreeAlgebra R X →ₐ[R] R :=
  lift R (0 : X → R)

Left inverse of the algebra map for free algebras

Informal description

The algebra homomorphism $\text{algebraMapInv} : \text{FreeAlgebra}\, R\, X \to R$ is defined as the lift of the zero function $0 : X \to R$ via the universal property of the free algebra. It serves as a left inverse to the algebra map $\text{algebraMap} : R \to \text{FreeAlgebra}\, R\, X$, meaning that $\text{algebraMapInv} \circ \text{algebraMap}$ is the identity on $R$.

FreeAlgebra.algebraMap_leftInverse theorem

: Function.LeftInverse algebraMapInv (algebraMap R <| FreeAlgebra R X)

Full source

theorem algebraMap_leftInverse :
    Function.LeftInverse algebraMapInv (algebraMap R <| FreeAlgebra R X) := fun x ↦ by
  simp [algebraMapInv]

Left Inverse Property of the Algebra Map in Free Algebras

Informal description

The algebra homomorphism $\text{algebraMapInv} : \text{FreeAlgebra}\, R\, X \to R$ is a left inverse of the algebra map $\text{algebraMap} : R \to \text{FreeAlgebra}\, R\, X$, meaning that for any $x \in R$, we have $\text{algebraMapInv}(\text{algebraMap}(x)) = x$.

FreeAlgebra.algebraMap_inj theorem

(x y : R) : algebraMap R (FreeAlgebra R X) x = algebraMap R (FreeAlgebra R X) y ↔ x = y

Full source

@[simp]
theorem algebraMap_inj (x y : R) :
    algebraMapalgebraMap R (FreeAlgebra R X) x = algebraMap R (FreeAlgebra R X) y ↔ x = y :=
  algebraMap_leftInverse.injective.eq_iff

Injectivity of the Algebra Map into Free Algebra

Informal description

For any elements $x, y$ in a commutative semiring $R$, the algebra homomorphism $\text{algebraMap} : R \to \text{FreeAlgebra}\, R\, X$ satisfies $\text{algebraMap}(x) = \text{algebraMap}(y)$ if and only if $x = y$.

FreeAlgebra.algebraMap_eq_zero_iff theorem

(x : R) : algebraMap R (FreeAlgebra R X) x = 0 ↔ x = 0

Full source

@[simp]
theorem algebraMap_eq_zero_iff (x : R) : algebraMapalgebraMap R (FreeAlgebra R X) x = 0 ↔ x = 0 :=
  map_eq_zero_iff (algebraMap _ _) algebraMap_leftInverse.injective

Injectivity of Zero in the Algebra Map for Free Algebras

Informal description

For any element $x$ in a commutative semiring $R$, the algebra homomorphism $\text{algebraMap} \colon R \to \text{FreeAlgebra}\, R\, X$ maps $x$ to zero if and only if $x$ is zero in $R$, i.e., $\text{algebraMap}(x) = 0 \leftrightarrow x = 0$.

FreeAlgebra.algebraMap_eq_one_iff theorem

(x : R) : algebraMap R (FreeAlgebra R X) x = 1 ↔ x = 1

Full source

@[simp]
theorem algebraMap_eq_one_iff (x : R) : algebraMapalgebraMap R (FreeAlgebra R X) x = 1 ↔ x = 1 :=
  map_eq_one_iff (algebraMap _ _) algebraMap_leftInverse.injective

Characterization of the Multiplicative Identity via the Algebra Map in Free Algebras

Informal description

For any element $x$ in a commutative semiring $R$, the algebra map $\text{algebraMap} \colon R \to \text{FreeAlgebra}\, R\, X$ sends $x$ to the multiplicative identity $1$ in the free algebra if and only if $x$ is the multiplicative identity in $R$. In other words, $\text{algebraMap}(x) = 1$ if and only if $x = 1$.

FreeAlgebra.ι_injective theorem

[Nontrivial R] : Function.Injective (ι R : X → FreeAlgebra R X)

Full source

theorem ι_injective [Nontrivial R] : Function.Injective (ι R : X → FreeAlgebra R X) :=
  fun x y hoxy ↦
  by_contradiction <| by
    classical exact fun hxy : x ≠ y ↦
        let f : FreeAlgebraFreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
        have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
        have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
        have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
        one_ne_zero <| hfy1.symm.trans hfy0

Injectivity of the Inclusion Map into the Free Algebra

Informal description

For a nontrivial commutative semiring $R$, the canonical inclusion map $\iota_R \colon X \to \text{FreeAlgebra}\, R\, X$ is injective. That is, for any $x, y \in X$, if $\iota_R(x) = \iota_R(y)$, then $x = y$.

FreeAlgebra.ι_inj theorem

[Nontrivial R] (x y : X) : ι R x = ι R y ↔ x = y

Full source

@[simp]
theorem ι_inj [Nontrivial R] (x y : X) : ιι R x = ι R y ↔ x = y :=
  ι_injective.eq_iff

Injectivity of the Free Algebra Inclusion Map: $\iota_R(x) = \iota_R(y) \leftrightarrow x = y$

Informal description

For a nontrivial commutative semiring $R$ and any elements $x, y \in X$, the images of $x$ and $y$ under the inclusion map $\iota_R \colon X \to \text{FreeAlgebra}\, R\, X$ are equal if and only if $x = y$. That is, $\iota_R(x) = \iota_R(y) \leftrightarrow x = y$.

FreeAlgebra.ι_ne_algebraMap theorem

[Nontrivial R] (x : X) (r : R) : ι R x ≠ algebraMap R _ r

Full source

@[simp]
theorem ι_ne_algebraMap [Nontrivial R] (x : X) (r : R) : ιι R x ≠ algebraMap R _ r := fun h ↦ by
  let f0 : FreeAlgebraFreeAlgebra R X →ₐ[R] R := lift R 0
  let f1 : FreeAlgebraFreeAlgebra R X →ₐ[R] R := lift R 1
  have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _
  have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _
  rw [h, f0.commutes, Algebra.id.map_eq_self] at hf0
  rw [h, f1.commutes, Algebra.id.map_eq_self] at hf1
  exact zero_ne_one (hf0.symm.trans hf1)

Generators are distinct from scalar images in free algebra

Informal description

For any nontrivial commutative semiring $R$, element $x \in X$, and scalar $r \in R$, the image of $x$ under the inclusion map $\iota_R : X \to \text{FreeAlgebra}\, R\, X$ is not equal to the image of $r$ under the algebra structure map $\text{algebraMap}\, R\, (\text{FreeAlgebra}\, R\, X)$. In other words, $\iota_R(x) \neq \text{algebraMap}\, R\, (\text{FreeAlgebra}\, R\, X)\, r$.

FreeAlgebra.ι_ne_zero theorem

[Nontrivial R] (x : X) : ι R x ≠ 0

Full source

@[simp]
theorem ι_ne_zero [Nontrivial R] (x : X) : ιι R x ≠ 0 :=
  ι_ne_algebraMap x 0

Nonzero Property of Generators in Free Algebra

Informal description

For any nontrivial commutative semiring $R$ and any element $x \in X$, the image of $x$ under the inclusion map $\iota_R : X \to \text{FreeAlgebra}\, R\, X$ is not equal to the zero element of the free algebra. In other words, $\iota_R(x) \neq 0$.

FreeAlgebra.ι_ne_one theorem

[Nontrivial R] (x : X) : ι R x ≠ 1

Full source

@[simp]
theorem ι_ne_one [Nontrivial R] (x : X) : ιι R x ≠ 1 :=
  ι_ne_algebraMap x 1

Generators are distinct from the identity in free algebra

Informal description

For any nontrivial commutative semiring $R$ and any element $x \in X$, the image of $x$ under the inclusion map $\iota_R : X \to \text{FreeAlgebra}\, R\, X$ is not equal to the multiplicative identity $1$ of the free algebra. In other words, $\iota_R(x) \neq 1$.

FreeAlgebra.induction theorem

 {motive : FreeAlgebra R X → Prop} (grade0 : ∀ r, motive (algebraMap R (FreeAlgebra R X) r))
  (grade1 : ∀ x, motive (ι R x)) (mul : ∀ a b, motive a → motive b → motive (a * b))
  (add : ∀ a b, motive a → motive b → motive (a + b)) (a : FreeAlgebra R X) : motive a

Full source

/-- An induction principle for the free algebra.

If `C` holds for the `algebraMap` of `r : R` into `FreeAlgebra R X`, the `ι` of `x : X`, and is
preserved under addition and multiplication, then it holds for all of `FreeAlgebra R X`.
-/
@[elab_as_elim, induction_eliminator]
theorem induction {motive : FreeAlgebra R X → Prop}
    (grade0 : ∀ r, motive (algebraMap R (FreeAlgebra R X) r)) (grade1 : ∀ x, motive (ι R x))
    (mul : ∀ a b, motive a → motive b → motive (a * b))
    (add : ∀ a b, motive a → motive b → motive (a + b))
    (a : FreeAlgebra R X) : motive a := by
  -- the arguments are enough to construct a subalgebra, and a mapping into it from X
  let s : Subalgebra R (FreeAlgebra R X) :=
    { carrier := motive
      mul_mem' := mul _ _
      add_mem' := add _ _
      algebraMap_mem' := grade0 }
  let of : X → s := Subtype.coind (ι R) grade1
  -- the mapping through the subalgebra is the identity
  have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp (lift R of) := by
    ext
    simp [of, Subtype.coind]
  -- finding a proof is finding an element of the subalgebra
  suffices a = lift R of a by
    rw [this]
    exact Subtype.prop (lift R of a)
  simp [AlgHom.ext_iff] at of_id
  exact of_id a

Induction Principle for Free Algebra over $R$ Generated by $X$

Informal description

Let $R$ be a commutative semiring and $X$ a type. For any predicate $\text{motive}$ on $\text{FreeAlgebra}\, R\, X$, if: 1. $\text{motive}$ holds for all elements in the image of the algebra map $R \to \text{FreeAlgebra}\, R\, X$, 2. $\text{motive}$ holds for all elements in the image of the inclusion map $\iota R : X \to \text{FreeAlgebra}\, R\, X$, 3. $\text{motive}$ is preserved under multiplication (i.e., if $\text{motive}\, a$ and $\text{motive}\, b$ hold, then $\text{motive}\, (a * b)$ holds), and 4. $\text{motive}$ is preserved under addition (i.e., if $\text{motive}\, a$ and $\text{motive}\, b$ hold, then $\text{motive}\, (a + b)$ holds), then $\text{motive}$ holds for all elements of $\text{FreeAlgebra}\, R\, X$.

FreeAlgebra.adjoin_range_ι theorem

: Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) = ⊤

Full source

@[simp]
theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X)) = ⊤ := by
  set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X))
  refine top_unique fun x hx => ?_; clear hx
  induction x with
  | grade0 => exact S.algebraMap_mem _
  | add x y hx hy => exact S.add_mem hx hy
  | mul x y hx hy => exact S.mul_mem hx hy
  | grade1 x => exact Algebra.subset_adjoin (Set.mem_range_self _)

Generators of Free Algebra Span the Entire Algebra

Informal description

The $R$-subalgebra generated by the image of the inclusion map $\iota_R : X \to \text{FreeAlgebra}\, R\, X$ is equal to the entire free algebra $\text{FreeAlgebra}\, R\, X$. In other words, $\text{adjoin}_R (\text{range}\, \iota_R) = \top$.

Algebra.adjoin_range_eq_range_freeAlgebra_lift theorem

(f : X → A) : Algebra.adjoin R (Set.range f) = (FreeAlgebra.lift R f).range

Full source

/-- Noncommutative version of `Algebra.adjoin_range_eq_range_aeval`. -/
theorem _root_.Algebra.adjoin_range_eq_range_freeAlgebra_lift (f : X → A) :
    Algebra.adjoin R (Set.range f) = (FreeAlgebra.lift R f).range := by
  simp only [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]

Adjoint Subalgebra Equals Range of Free Algebra Lift

Informal description

For any commutative semiring $R$, type $X$, and $R$-algebra $A$, given a function $f \colon X \to A$, the $R$-subalgebra generated by the range of $f$ is equal to the range of the lifted $R$-algebra homomorphism $\text{lift}_R f \colon \text{FreeAlgebra}\, R\, X \to A$.

Algebra.adjoin_eq_range_freeAlgebra_lift theorem

(s : Set A) : Algebra.adjoin R s = (FreeAlgebra.lift R ((↑) : s → A)).range

Full source

/-- Noncommutative version of `Algebra.adjoin_range_eq_range`. -/
theorem _root_.Algebra.adjoin_eq_range_freeAlgebra_lift (s : Set A) :
    Algebra.adjoin R s = (FreeAlgebra.lift R ((↑) : s → A)).range := by
  rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]

Subalgebra Generation Equals Range of Free Algebra Lift on Subset

Informal description

For any commutative semiring $R$, $R$-algebra $A$, and subset $s \subseteq A$, the $R$-subalgebra generated by $s$ is equal to the range of the lifted $R$-algebra homomorphism $\text{lift}_R (\iota : s \to A) : \text{FreeAlgebra}\, R\, s \to A$, where $\iota$ is the inclusion map of $s$ into $A$.