Exterior Algebras #
We construct the exterior algebra of a module M over a commutative semiring R.
Notation #
The exterior algebra of the R-module M is denoted as exterior_algebra R M.
It is endowed with the structure of an R-algebra.
Given a linear morphism f : M → A from a module M to another R-algebra A, such that
cond : ∀ m : M, f m * f m = 0, there is a (unique) lift of f to an R-algebra morphism,
which is denoted exterior_algebra.lift R f cond.
The canonical linear map M → exterior_algebra R M is denoted exterior_algebra.ι R.
Theorems #
The main theorems proved ensure that exterior_algebra R M satisfies the universal property
of the exterior algebra.
ι_comp_liftis fact that the composition ofι Rwithlift R f condagrees withf.lift_uniqueensures the uniqueness oflift R f condwith respect to 1.
Definitions #
ι_multiis thealternating_mapcorresponding to the wedge product ofι R mterms.
Implementation details #
The exterior algebra of M is constructed as a quotient of the tensor algebra, as follows.
- We define a relation
exterior_algebra.rel R Montensor_algebra R M. This is the smallest relation which identifies squares of elements ofMwith0. - The exterior algebra is the quotient of the tensor algebra by this relation.
inductive
exterior_algebra.rel
(R : Type u1)
[comm_semiring R]
(M : Type u2)
[add_comm_monoid M]
[module R M] :
tensor_algebra R M → tensor_algebra R M → Prop
- of : ∀ (R : Type u1) [_inst_1 : comm_semiring R] (M : Type u2) [_inst_2 : add_comm_monoid M] [_inst_3 : module R M] (m : M), exterior_algebra.rel R M ((⇑(tensor_algebra.ι R) m) * ⇑(tensor_algebra.ι R) m) 0
rel relates each ι m * ι m, for m : M, with 0.
The exterior algebra of M is defined as the quotient modulo this relation.
def
exterior_algebra
(R : Type u1)
[comm_semiring R]
(M : Type u2)
[add_comm_monoid M]
[module R M] :
Type (max u1 u2)
The exterior algebra of an R-module M.
Equations
- exterior_algebra R M = ring_quot (exterior_algebra.rel R M)
@[protected, instance]
def
exterior_algebra.inhabited
(R : Type u1)
[comm_semiring R]
(M : Type u2)
[add_comm_monoid M]
[module R M] :
inhabited (exterior_algebra R M)
@[protected, instance]
def
exterior_algebra.semiring
(R : Type u1)
[comm_semiring R]
(M : Type u2)
[add_comm_monoid M]
[module R M] :
semiring (exterior_algebra R M)
@[protected, instance]
def
exterior_algebra.algebra
(R : Type u1)
[comm_semiring R]
(M : Type u2)
[add_comm_monoid M]
[module R M] :
algebra R (exterior_algebra R M)
@[protected, instance]
def
exterior_algebra.ring
{M : Type u2}
[add_comm_monoid M]
{S : Type u3}
[comm_ring S]
[module S M] :
ring (exterior_algebra S M)
Equations
def
exterior_algebra.ι
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M] :
M →ₗ[R] exterior_algebra R M
The canonical linear map M →ₗ[R] exterior_algebra R M.
Equations
@[simp]
theorem
exterior_algebra.ι_sq_zero
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
(m : M) :
(⇑(exterior_algebra.ι R) m) * ⇑(exterior_algebra.ι R) m = 0
As well as being linear, ι m squares to zero
@[simp]
theorem
exterior_algebra.comp_ι_sq_zero
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
(g : exterior_algebra R M →ₐ[R] A)
(m : M) :
(⇑g (⇑(exterior_algebra.ι R) m)) * ⇑g (⇑(exterior_algebra.ι R) m) = 0
def
exterior_algebra.lift
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A] :
Given a linear map f : M →ₗ[R] A into an R-algebra A, which satisfies the condition:
cond : ∀ m : M, f m * f m = 0, this is the canonical lift of f to a morphism of R-algebras
from exterior_algebra R M to A.
Equations
- exterior_algebra.lift R = {to_fun := λ (f : {f // ∀ (m : M), (⇑f m) * ⇑f m = 0}), ⇑(ring_quot.lift_alg_hom R) ⟨⇑(tensor_algebra.lift R) ↑f, _⟩, inv_fun := λ (F : exterior_algebra R M →ₐ[R] A), ⟨F.to_linear_map.comp (exterior_algebra.ι R), _⟩, left_inv := _, right_inv := _}
@[simp]
theorem
exterior_algebra.lift_symm_apply
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
(F : exterior_algebra R M →ₐ[R] A) :
⇑((exterior_algebra.lift R).symm) F = ⟨F.to_linear_map.comp (exterior_algebra.ι R), _⟩
@[simp]
theorem
exterior_algebra.ι_comp_lift
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(cond : ∀ (m : M), (⇑f m) * ⇑f m = 0) :
(⇑(exterior_algebra.lift R) ⟨f, cond⟩).to_linear_map.comp (exterior_algebra.ι R) = f
@[simp]
theorem
exterior_algebra.lift_ι_apply
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(cond : ∀ (m : M), (⇑f m) * ⇑f m = 0)
(x : M) :
⇑(⇑(exterior_algebra.lift R) ⟨f, cond⟩) (⇑(exterior_algebra.ι R) x) = ⇑f x
@[simp]
theorem
exterior_algebra.lift_unique
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
(f : M →ₗ[R] A)
(cond : ∀ (m : M), (⇑f m) * ⇑f m = 0)
(g : exterior_algebra R M →ₐ[R] A) :
g.to_linear_map.comp (exterior_algebra.ι R) = f ↔ g = ⇑(exterior_algebra.lift R) ⟨f, cond⟩
@[simp]
theorem
exterior_algebra.lift_comp_ι
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
(g : exterior_algebra R M →ₐ[R] A) :
⇑(exterior_algebra.lift R) ⟨g.to_linear_map.comp (exterior_algebra.ι R), _⟩ = g
@[ext]
theorem
exterior_algebra.hom_ext
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{A : Type u_1}
[semiring A]
[algebra R A]
{f g : exterior_algebra R M →ₐ[R] A}
(h : f.to_linear_map.comp (exterior_algebra.ι R) = g.to_linear_map.comp (exterior_algebra.ι R)) :
f = g
theorem
exterior_algebra.induction
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{C : exterior_algebra R M → Prop}
(h_grade0 : ∀ (r : R), C (⇑(algebra_map R (exterior_algebra R M)) r))
(h_grade1 : ∀ (x : M), C (⇑(exterior_algebra.ι R) x))
(h_mul : ∀ (a b : exterior_algebra R M), C a → C b → C (a * b))
(h_add : ∀ (a b : exterior_algebra R M), C a → C b → C (a + b))
(a : exterior_algebra R M) :
C a
If C holds for the algebra_map of r : R into exterior_algebra R M, the ι of x : M,
and is preserved under addition and muliplication, then it holds for all of exterior_algebra R M.
def
exterior_algebra.algebra_map_inv
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M] :
exterior_algebra R M →ₐ[R] R
The left-inverse of algebra_map.
Equations
theorem
exterior_algebra.algebra_map_left_inverse
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M] :
def
exterior_algebra.ι_inv
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M] :
exterior_algebra R M →ₗ[R] M
The left-inverse of ι.
As an implementation detail, we implement this using triv_sq_zero_ext which has a suitable
algebra structure.
Equations
- exterior_algebra.ι_inv = (triv_sq_zero_ext.snd_hom R M).comp (⇑(exterior_algebra.lift R) ⟨triv_sq_zero_ext.inr_hom R M _inst_3, _⟩).to_linear_map
theorem
exterior_algebra.ι_left_inverse
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M] :
@[simp]
theorem
exterior_algebra.ι_add_mul_swap
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
(x y : M) :
(⇑(exterior_algebra.ι R) x) * ⇑(exterior_algebra.ι R) y + (⇑(exterior_algebra.ι R) y) * ⇑(exterior_algebra.ι R) x = 0
theorem
exterior_algebra.ι_mul_prod_list
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{n : ℕ}
(f : fin n → M)
(i : fin n) :
(⇑(exterior_algebra.ι R) (f i)) * (list.of_fn (λ (i : fin n), ⇑(exterior_algebra.ι R) (f i))).prod = 0
def
exterior_algebra.ι_multi
(R : Type u1)
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
(n : ℕ) :
alternating_map R M (exterior_algebra R M) (fin n)
The product of n terms of the form ι R m is an alternating map.
This is a special case of multilinear_map.mk_pi_algebra_fin
Equations
- exterior_algebra.ι_multi R n = let F : multilinear_map R (λ (i : fin n), M) (exterior_algebra R M) := (multilinear_map.mk_pi_algebra_fin R n (exterior_algebra R M)).comp_linear_map (λ (i : fin n), exterior_algebra.ι R) in {to_fun := ⇑F, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
theorem
exterior_algebra.ι_multi_apply
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
{n : ℕ}
(v : fin n → M) :
⇑(exterior_algebra.ι_multi R n) v = (list.of_fn (λ (i : fin n), ⇑(exterior_algebra.ι R) (v i))).prod
def
tensor_algebra.to_exterior
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M] :
tensor_algebra R M →ₐ[R] exterior_algebra R M
The canonical image of the tensor_algebra in the exterior_algebra, which maps
tensor_algebra.ι R x to exterior_algebra.ι R x.
Equations
@[simp]
theorem
tensor_algebra.to_exterior_ι
{R : Type u1}
[comm_semiring R]
{M : Type u2}
[add_comm_monoid M]
[module R M]
(m : M) :
⇑tensor_algebra.to_exterior (⇑(tensor_algebra.ι R) m) = ⇑(exterior_algebra.ι R) m