Commit 2024-02-16 17:31 29c27c39

feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation (#9718) This does a few things:

• Define the algebra morphism TrivSqZeroExt.map f between trivial square-zero extensions induced by a linear mapf, and establish some of its basic properties (functoriality, composition with the basic maps to/from TrivSqZeroExt). Note that we only consider the case of a commutative base ring, because the case of a general base ring requires morphisms of bimodules, which we do not have.
• Define the algebra morphism ExteriorAlgebra.map f between exterior algebras induced by a linear map f. This is a straightforward application of the similar construction for Clifford algebras, but I think it is still useful to have. Basic properties of this construction are proved: functoriality, composition with ExteriorAlgebra.ι, ExteriorAlgebra.ιInv (this part uses the first point) and ExteriorAlgebra.ιMulti. Then exactness properties of the construction is studied:
  • If the linear map is surjective, then the map on exterior algebras is also surjective. This actually holds for Clifford algebras, so I added a lemma called CliffordAlgebra.map_surjective in LinearAlgebra/CliffordAlgebra/Basic.lean. For exterior algebras, the converse holds and is also proved.
  • If the linear map has a retraction, then the map on exterior algebras is injective. So if the base ring is a field, the map on exterior algebras is injective if the linear map is injective.
• Establish some properties of ExteriorAlgebra.ιMulti:
  • ExteriorAlgebra.ιMulti_range: The range of ιMulti R n is contained in the nth exterior power (define here as LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n).
  • ExteriorAlgebra.ιMulti_span_fixedDegree: This range spans the nth exterior power.
  • ExteriorAlgebra.ιMulti_span: The union over all n of the range of ιMulti R n spans the whole exterior algebra (this is in LinearAlgebra/ExteriorAlgebra/Grading.lean because the proof uses the graded module structure, but it might be possible to do something simpler).
• Construct ExteriorAlgebra.ιMulti_family: This takes a natural number n and a family of vectors v indexed by a linearly ordered type I, and it returns the family of n-fold products of the v i in the exterior algebra, indexed by the set of finsets of I of cardinality n. (The point, to be proved in another PR, is that when v is a basis, then ExteriorAlgebra.ιMulti_family R n v is a basis of the nth exterior power.)