ExteriorAlgebra.hom_ext
theorem ExteriorAlgebra.hom_ext :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
[inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : ExteriorAlgebra R M →ₐ[R] A},
f.toLinearMap ∘ₗ ExteriorAlgebra.ι R = g.toLinearMap ∘ₗ ExteriorAlgebra.ι R → f = g
This theorem, `ExteriorAlgebra.hom_ext`, asserts that for any commutative ring `R`, additive commutative group `M` that is also a module over `R`, and another semiring `A` that is an algebra over `R`, if `f` and `g` are two algebra homomorphisms from the exterior algebra of `M` over `R` to `A` such that their compositions with the canonical linear map from `M` to the exterior algebra are equal, then `f` and `g` themselves must be equal. This is essentially a statement about the uniqueness of algebra homomorphisms under certain conditions.
More concisely: If `R` is a commutative ring, `M` is an additive commutative group and an `R`-module, `A` is an `R`-algebra, and `f` and `g` are algebra homomorphisms from the exterior algebra of `M` over `R` to `A` such that the composite of each with the canonical map from `M` to the exterior algebra is equal, then `f` and `g` are equal.
|
ExteriorAlgebra.map.proof_1
theorem ExteriorAlgebra.map.proof_1 :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_2}
[inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) (x : M), 0 (f.toFun x) = 0 (f.toFun x)
This theorem states that for any commutative ring `R`, any types `M` and `N` that are both additive commutative groups and `R`-modules, and any linear map `f` from `M` to `N`, applying the function `f` to a value `x` from `M` and then applying the zero function results in the same output as first applying the zero function to `f(x)`. In mathematical terms, it says that for linear map `f: M → N`, we have `0(f(x)) = 0(f(x))` for all `x` in `M`.
More concisely: For any linear map `f` from an additive commutative group `M` to an additive commutative group `N` and any element `x` in `M`, we have `0(f(x)) = 0(f(0))`, where `0` denotes the zero function.
|
ExteriorAlgebra.induction
theorem ExteriorAlgebra.induction :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{C : ExteriorAlgebra R M → Prop},
(∀ (r : R), C ((algebraMap R (ExteriorAlgebra R M)) r)) →
(∀ (x : M), C ((ExteriorAlgebra.ι R) x)) →
(∀ (a b : ExteriorAlgebra R M), C a → C b → C (a * b)) →
(∀ (a b : ExteriorAlgebra R M), C a → C b → C (a + b)) → ∀ (a : ExteriorAlgebra R M), C a
The theorem `ExteriorAlgebra.induction` states that for any commutative ring `R`, and any module `M` over `R`, if a property `C` holds for the `algebraMap` of any element `r` of `R` into `ExteriorAlgebra R M`, and for the `ι` of any element `x` of `M`, and if this property `C` is preserved under both addition and multiplication in `ExteriorAlgebra R M`, then this property `C` holds for all elements of `ExteriorAlgebra R M`.
More concisely: If a property `C` holds for the `algebraMap` of all elements in a commutative ring `R` and the `ι` of all elements in a module `M` over `R`, and `C` is additive and multiplicative in the exterior algebra `ExteriorAlgebra R M`, then `C` holds for all elements in `ExteriorAlgebra R M`.
|
ExteriorAlgebra.ι_sq_zero
theorem ExteriorAlgebra.ι_sq_zero :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (m : M),
(ExteriorAlgebra.ι R) m * (ExteriorAlgebra.ι R) m = 0
This theorem states that, for any given commutative ring `R` and a module `M` over `R` that also forms an additive commutative group, the function `ι` from `M` to the exterior algebra of `R` and `M` has the property that the square of its application to any element `m` of `M` is zero. In other words, if you apply the function `ι` to an element `m` of `M` and then square the result, you always get zero. This property is fundamental for understanding the algebraic structure and behavior of the exterior algebra.
More concisely: For any commutative ring `R` and an additive commutative group `M` that is an `R`-module, the square of the map `ι : M → ∧ⁱ⁺ⁱ (*: Type*) (M : Type*) (R : Type*) : M → ∧ⁱ⁺ⁱ R M, from a module `M` to the exterior algebra `∧ⁱ⁺ⁱ R M`, maps every element `m` in `M` to zero.
|
ExteriorAlgebra.lift.proof_1
theorem ExteriorAlgebra.lift.proof_1 :
∀ (R : Type u_3) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
[inst_3 : Semiring A] [inst_4 : Algebra R A] (a : M →ₗ[R] A),
(∀ (m : M), a m * a m = 0) ↔ ∀ (a_1 : M), a a_1 * a a_1 = (algebraMap R A) 0
The theorem `ExteriorAlgebra.lift.proof_1` states that for any commutative ring `R`, additive commutative group `M`, module `M` over `R`, semiring `A`, and an algebra `A` over `R`, given a linear map `a` from `M` to `A`, the condition that the square of the image of any element of `M` under `a` equals zero is equivalent to the condition that the square of the image of any element of `M` under `a` equals the image of zero from `R` under the algebra map to `A`.
In simpler terms, this means that if for a linear map, the square of the result of mapping any element is always zero, it's the same as saying the square of the result of mapping any element is always the image of zero in the algebra structure.
More concisely: For a linear map from an additive commutative group to an algebra over a commutative ring, the condition that the image of any element squared is zero is equivalent to the image of any element squared being the image of zero under the algebra map.
|
ExteriorAlgebra.ι_range_disjoint_one
theorem ExteriorAlgebra.ι_range_disjoint_one :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Disjoint (LinearMap.range (ExteriorAlgebra.ι R)) 1
This theorem states that the generators of the exterior algebra are disjoint from its scalars. In other words, for any commutative ring R and any additive commutative group M that is also an R-module, the range of the canonical linear map (the map that generates the exterior algebra) does not intersect with the set of scalar multiples of the identity. Here, disjointness is defined in the sense of lattice theory, i.e., two elements are considered disjoint if their infimum is the bottom element.
More concisely: The canonical map from an R-module M to its exterior algebra over a commutative ring R maps M to a subspace that is disjoint from the scalars in the lattice of subspaces.
|
ExteriorAlgebra.algebraMap_leftInverse
theorem ExteriorAlgebra.algebraMap_leftInverse :
∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Function.LeftInverse ⇑ExteriorAlgebra.algebraMapInv ⇑(algebraMap R (ExteriorAlgebra R M))
This theorem states that for any commutative ring `R` and any type `M` that has additional structures of an additive commutative group and an `R`-module, the function `ExteriorAlgebra.algebraMapInv` acts as a left inverse to the function `algebraMap R (ExteriorAlgebra R M)`. In other words, if you first apply `algebraMap R (ExteriorAlgebra R M)` to any element of `R`, and then apply `ExteriorAlgebra.algebraMapInv` to the result, you will get back your original element of `R`. This is expressed as `Function.LeftInverse ⇑ExteriorAlgebra.algebraMapInv ⇑(algebraMap R (ExteriorAlgebra R M))`.
More concisely: For any commutative ring `R` and `R`-module `M` with additional structure of an additive commutative group, the map `ExteriorAlgebra.algebraMapInv` is the left inverse of `algebraMap R` on `ExteriorAlgebra R M`.
|