TensorAlgebra.ι_range_disjoint_one
theorem TensorAlgebra.ι_range_disjoint_one :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Disjoint (LinearMap.range (TensorAlgebra.ι R)) 1
The theorem `TensorAlgebra.ι_range_disjoint_one` states that for any type `R` with commutative semiring structure, and any type `M` with additive commutative monoid structure and module over `R`, the generators of the tensor algebra (which are the range of the canonical linear map `TensorAlgebra.ι R` from `M` to the tensor algebra) are disjoint from its scalars. Here, disjointness is defined in the sense of lattice theory; i.e., two elements `a` and `b` of a lattice are considered disjoint if for any element `x` of the lattice, if `x` is lesser than or equal to `a` and `b`, then `x` is also lesser than or equal to the bottom element of the lattice. In the context of the tensor algebra, this theorem implies that the generators and the scalars are distinct and do not overlap.
More concisely: The generators of the tensor algebra over a commutative semiring `R` on a module `M` are disjoint from the scalars in the sense of lattice theory.
|
TensorAlgebra.lift_ι_apply
theorem TensorAlgebra.lift_ι_apply :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (x : M),
((TensorAlgebra.lift R) f) ((TensorAlgebra.ι R) x) = f x
The theorem `TensorAlgebra.lift_ι_apply` states that for any commutative semiring `R`, additive commutative monoid `M`, and `M` is a module over `R`, and for any semiring `A` with `A` being an algebra over `R`, and a linear map `f` from `M` to `A`, the composition of the lift of `f` to the tensor algebra of `M` over `R` and the canonical linear map from `M` to that tensor algebra, when applied to any element `x` of `M`, is equal to the application of `f` to `x`. In simpler terms, this theorem confirms that the lifting operation on the tensor algebra correctly interprets the linear map when it is applied to elements of the module `M`.
More concisely: For any commutative semiring `R`, additive commutative monoid `M` being an `R`-module, semiring `A` an `R`-algebra, and linear map `f` from `M` to `A`, the composition of `f`'s lift to the tensor algebra of `M` over `R` and the canonical map from `M` to the tensor algebra equals `f` itself when applied to any `x` in `M`.
|
TensorAlgebra.hom_ext
theorem TensorAlgebra.hom_ext :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : TensorAlgebra R M →ₐ[R] A},
f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R → f = g
The theorem `TensorAlgebra.hom_ext` is a statement about the uniqueness of algebra homomorphisms from a tensor algebra to any other algebra. Concretely, it states that for any commutative semiring `R`, any `R`-module `M`, and any `R`-algebra `A`, if `f` and `g` are two algebra homomorphisms from the tensor algebra of `M` over `R` to `A`, and if these two homomorphisms agree on the linear map from `M` itself to the tensor algebra (that is, `f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R`), then `f` and `g` must be the same homomorphism. This theorem is a specific instance of a more general principle in mathematics, that morphisms (here, algebra homomorphisms) are determined by their action on "generators" (here, the elements of `M` viewed inside the tensor algebra).
More concisely: Given a commutative semiring `R`, an `R`-module `M`, and an `R`-algebra `A`, if two algebra homomorphisms from the tensor algebra of `M` over `R` to `A` agree on the elements of `M`, then they are equal.
|
TensorAlgebra.algebraMap_leftInverse
theorem TensorAlgebra.algebraMap_leftInverse :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Function.LeftInverse ⇑TensorAlgebra.algebraMapInv ⇑(algebraMap R (TensorAlgebra R M))
This theorem asserts that for any type `R` which is a commutative semiring, and any type `M` which is both an additive commutative monoid and a module over `R`, the function `TensorAlgebra.algebraMapInv` serves as a left inverse to the algebra map from `R` to the tensor algebra of `M` over `R`. In other words, for all `x` in `R`, when you first apply the algebra map to `x` and then apply `TensorAlgebra.algebraMapInv` to the result, you will get `x` back. This means that `TensorAlgebra.algebraMapInv` undoes the effect of the algebra map, but only when applied after the algebra map --- which is what it means to be a left inverse.
More concisely: For any commutative semiring `R` and an additive commutative monoid `M` that is an `R`-module, the function `TensorAlgebra.algebraMapInv` is a left inverse to the algebra map from `R` to the tensor algebra of `M` over `R`. That is, for all `x` in `R`, `algebraMap (x) = TensorAlgebra.algebramapInv (algebraMapInv x)`.
|
TensorAlgebra.induction
theorem TensorAlgebra.induction :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{C : TensorAlgebra R M → Prop},
(∀ (r : R), C ((algebraMap R (TensorAlgebra R M)) r)) →
(∀ (x : M), C ((TensorAlgebra.ι R) x)) →
(∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)) →
(∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)) → ∀ (a : TensorAlgebra R M), C a
The theorem `TensorAlgebra.induction` states that if a property `C` holds for the image of a scalar `r` under the algebra structure from `R` into the tensor algebra `TensorAlgebra R M` (that is, `C ((algebraMap R (TensorAlgebra R M)) r)`) and for the image of `x` from the module `M` under the canonical linear map into the tensor algebra (that is, `C ((TensorAlgebra.ι R) x)`), and if `C` is preserved under both addition and multiplication in the tensor algebra (meaning that if `C` holds for both `a` and `b`, it also holds for `(a * b)` and `(a + b)`), then `C` holds for all elements of the tensor algebra. In simpler words, it affirms that properties held by scalars and module elements, and preserved under the algebra operations, holds for all elements within the tensor algebra.
More concisely: If a property preserves scalar and linear map applications and is closed under addition and multiplication in the tensor algebra, then it holds for all elements in the tensor algebra.
|