FreeAlgebra.hom_ext
theorem FreeAlgebra.hom_ext :
∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
{f g : FreeAlgebra R X →ₐ[R] A}, ⇑f ∘ FreeAlgebra.ι R = ⇑g ∘ FreeAlgebra.ι R → f = g
The theorem `FreeAlgebra.hom_ext` establishes an extensionality criterion for morphisms from a free algebra to another algebra over a commutative semiring. Specifically, it states that for any commutative semiring `R`, type `X`, semiring `A`, algebra structure for `A` over `R`, and two algebra homomorphisms `f` and `g` from the free algebra over `R` on `X` to `A`, if these two algebra homomorphisms agree on the canonical injection from `X` to the free algebra (i.e., `⇑f ∘ FreeAlgebra.ι R = ⇑g ∘ FreeAlgebra.ι R`), then `f` and `g` must be the same. This theorem is useful when proving two algebra homomorphisms are equal, as it suffices to show that they agree on the canonical injection.
More concisely: Given a commutative semiring `R`, a type `X`, a semiring `A`, an algebra structure for `A` over `R`, and two algebra homomorphisms `f` and `g` from the free algebra over `R` on `X` to `A`, if `f ∘ FreeAlgebra.ι R = g ∘ FreeAlgebra.ι R`, then `f = g`.
|
Algebra.adjoin_eq_range_freeAlgebra_lift
theorem Algebra.adjoin_eq_range_freeAlgebra_lift :
∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
Algebra.adjoin R s = ((FreeAlgebra.lift R) Subtype.val).range
This theorem, `Algebra.adjoin_eq_range_freeAlgebra_lift`, states that for any commutative semiring `R` and any semiring `A` which is an `R`-algebra, and for any set `s` of elements from `A`, the minimal subalgebra that includes `s` (as given by `Algebra.adjoin R s`) is equal to the range of the unique lift of the identity function on `s` (as given by `(FreeAlgebra.lift R) Subtype.val`). This lift is from the free `R`-algebra on `s` to `A`. In other words, every element in the minimal subalgebra that includes `s` can be expressed as a linear combination of elements from `s`, and each such linear combination corresponds to a unique element in the free `R`-algebra on `s`.
More concisely: For any commutative semiring R and R-algebra A, the minimal subalgebra of A generated by a set s is equal to the range of the unique lift of the identity function on s from the free R-algebra on s to A.
|
FreeAlgebra.ι_def
theorem FreeAlgebra.ι_def :
∀ (R : Type u_3) [inst : CommSemiring R] {X : Type u_4} (m : X),
FreeAlgebra.ι R m = Quot.mk (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m)
The theorem `FreeAlgebra.ι_def` states that for any commutative semiring `R` and any type `X`, the canonical function `FreeAlgebra.ι R` that takes an element `m` of `X` and maps it to an element of the free algebra of `X` over `R`, is equal to the function `Quot.mk` applied to the relation `FreeAlgebra.Rel R X` and `FreeAlgebra.Pre.of m`. Here, `Quot.mk` constructs a quotient type using the given relation and `FreeAlgebra.Pre.of m` constructs an element of the pre-algebra. In mathematical terms, this theorem specifies how elements from `X` are embedded into the free algebra.
More concisely: The canonical embedding of an element from `X` into the free algebra over a commutative semiring `R` is equal to the quotient type construction using the relation `FreeAlgebra.Rel R X` and the pre-algebra element `FreeAlgebra.Pre.of m`.
|
FreeAlgebra.lift_ι_apply
theorem FreeAlgebra.lift_ι_apply :
∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(f : X → A) (x : X), ((FreeAlgebra.lift R) f) (FreeAlgebra.ι R x) = f x
The theorem `FreeAlgebra.lift_ι_apply` states that for any commutative semiring `R`, any types `X` and `A`, any semiring structure on `A`, any `R`-algebra structure on `A`, and any function `f : X → A`, when you apply the function `FreeAlgebra.ι R` (which is a canonical function from `X` to `FreeAlgebra R X`) to an element `x : X`, and then apply `FreeAlgebra.lift R f` (which is the unique lift of `f` to a morphism of `R`-algebras `FreeAlgebra R X → A`) to the result, it is equal to the result of applying `f` directly to `x`. In other words, `FreeAlgebra.lift R f` and `FreeAlgebra.ι R` commute with `f`.
More concisely: For any commutative semiring `R`, given an `R`-algebra `A` with a semiring structure and an `R`-algebra homomorphism `f : FreeAlgebra R X → A` from the free algebra over a type `X` to `A`, the application of `f` to an element `x : X` is equal to the composition of `FreeAlgebra.lift R f` with `FreeAlgebra.ι R x`.
|
FreeAlgebra.algebraMap_leftInverse
theorem FreeAlgebra.algebraMap_leftInverse :
∀ {R : Type u_1} [inst : CommSemiring R] {X : Type u_2},
Function.LeftInverse ⇑FreeAlgebra.algebraMapInv ⇑(algebraMap R (FreeAlgebra R X))
The theorem `FreeAlgebra.algebraMap_leftInverse` states that for any type `R` with a commutative semiring structure and any type `X`, the function `FreeAlgebra.algebraMapInv` is a left inverse to the function `algebraMap R (FreeAlgebra R X)`. In other words, for any element `x` of type `R`, applying `algebraMap R (FreeAlgebra R X)` to `x` and then applying `FreeAlgebra.algebraMapInv` to the result will return `x`. This is denoted in Lean 4 as `Function.LeftInverse ⇑FreeAlgebra.algebraMapInv ⇑(algebraMap R (FreeAlgebra R X))`.
More concisely: For any commutative semiring `R` and type `X`, the function `FreeAlgebra.algebraMapInv` is the left inverse of `algebraMap R` on `FreeAlgebra R X`, i.e., `algebraMap R ∘ FreeAlgebra.algebraMapInv = id` on elements of `FreeAlgebra R X`.
|
Algebra.adjoin_range_eq_range_freeAlgebra_lift
theorem Algebra.adjoin_range_eq_range_freeAlgebra_lift :
∀ (R : Type u_1) [inst : CommSemiring R] (X : Type u_2) {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(f : X → A), Algebra.adjoin R (Set.range f) = ((FreeAlgebra.lift R) f).range
The theorem `Algebra.adjoin_range_eq_range_freeAlgebra_lift` states that for any commutative semiring `R`, type `X`, and an `R`-algebra `A` where `A` is a semiring, given a function `f` mapping `X` to `A`, the minimal subalgebra of `A` that includes the range of `f` (algebraically adjoined to `R`) is identical to the range of the morphism of `R`-algebras from the free algebra over `R` on `X` to `A` that uniquely lifts `f`. In simpler terms, this theorem shows a correspondence between algebraically adjoining the values of a function to a ring and lifting the function to a free algebra.
More concisely: For any commutative semiring R, type X, and R-algebra A, the subalgebra of A generated by the range of a function from X to A is equal to the image of the unique morphism of R-algebras from the free algebra over R on X to A that lifts the function.
|
FreeAlgebra.lift.proof_2
theorem FreeAlgebra.lift.proof_2 :
∀ (R : Type u_1) [inst : CommSemiring R] {X : Type u_2} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ⇑F ∘ FreeAlgebra.ι R) F) = F
This theorem states that for any commutative semiring `R`, any type `X`, any semiring `A` equipped with an algebra structure over `R`, and any algebra homomorphism `F` from the free algebra of `X` over `R` to `A`, the lift of the composition of `F` and the canonical injection from `X` to the free algebra of `X` over `R` is equal to `F` itself. Essentially, this encapsulates the universal property of the free algebra in the context of algebra homomorphisms.
More concisely: For any commutative semiring `R`, any type `X`, any semiring `A` with an algebra structure over `R`, and any algebra homomorphism `F` from the free algebra of `X` over `R` to `A`, the following diagram commutes:
```
FreeAlgebra X R ───────── F ─── A
│ │
└─── sink(x) ───┐
│ │
X ──────┘─── injection ───┐
```
Or in mathematical notation, `F ∘ injection = F ∘ sink(x)`, where `sink(x)` is the sink map from `X` to the free algebra of `X` over `R`.
|
FreeAlgebra.induction
theorem FreeAlgebra.induction :
∀ (R : Type u_1) [inst : CommSemiring R] (X : Type u_2) {C : FreeAlgebra R X → Prop},
(∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)) →
(∀ (x : X), C (FreeAlgebra.ι R x)) →
(∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)) →
(∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)) → ∀ (a : FreeAlgebra R X), C a
The `FreeAlgebra.induction` theorem is an induction principle for the free algebra. It states that for a given commutative semiring `R` and a type `X`, if a property `C` holds for every element of `R` mapped into the free algebra `FreeAlgebra R X` using the `algebraMap`, for every element of `X` using the canonical function `FreeAlgebra.ι R`, and `C` is preserved under the operations of addition and multiplication in the free algebra, then `C` holds for every element of the free algebra `FreeAlgebra R X`.
More concisely: If a property is preserved under the algebra maps and operations in a free algebra over a commutative semiring, then it holds for every element in the free algebra.
|
FreeAlgebra.lift.proof_1
theorem FreeAlgebra.lift.proof_1 :
∀ (R : Type u_3) [inst : CommSemiring R] {X : Type u_1} {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(f : X → A), (fun F => ⇑F ∘ FreeAlgebra.ι R) (FreeAlgebra.liftAux R f) = f
The theorem `FreeAlgebra.lift.proof_1` states that for any types `R`, `X`, `A`, any commutative semiring structure on `R`, any semiring structure on `A`, any algebra structure over `R` on `A`, and any function `f` from `X` to `A`, the function obtained by composing the function `f` with the canonical embedding `FreeAlgebra.ι R` of `X` into the free algebra over `R` on `X` and then applying `FreeAlgebra.liftAux R f`, is equal to the original function `f`.
In other words, this indicates that the `FreeAlgebra.liftAux` operation essentially "undoes" the mapping performed by the canonical embedding `FreeAlgebra.ι R`, returning us back to our original function `f`.
More concisely: The theorem asserts that applying `FreeAlgebra.liftAux` to the composite of a function with the canonical embedding of a set into its free algebra over a commutative semiring yields the original function.
|
FreeAlgebra.lift_symm_apply
theorem FreeAlgebra.lift_symm_apply :
∀ (R : Type u_1) [inst : CommSemiring R] {X : Type u_2} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
(F : FreeAlgebra R X →ₐ[R] A), (FreeAlgebra.lift R).symm F = ⇑F ∘ FreeAlgebra.ι R
The theorem `FreeAlgebra.lift_symm_apply` states that for any commutative semiring `R`, any type `X`, an `R`-algebra `A`, and any `R`-algebra homomorphism `F` from the free algebra over `X` and `R` to `A`, the inverse of the lift of `F` (obtained via the `FreeAlgebra.lift R` function) is equal to the composition of `F` and the canonical function `FreeAlgebra.ι R` from `X` to the free algebra over `X` and `R`. In other words, it expresses a relationship between the lift of an algebra homomorphism and the canonical function into a free algebra.
More concisely: For any commutative semiring `R`, type `X`, `R`-algebra `A`, and `R`-algebra homomorphism `F` from the free algebra over `X` and `R` to `A`, the inverse of `FreeAlgebra.lift R F` is equal to `FreeAlgebra.ι R` composed with `F`.
|