Documentation

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

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 ExteriorAlgebra R M. It is endowed with the structure of an R-algebra.

The nth exterior power of the R-module M is denoted by exteriorPower R n M; it is of type Submodule R (ExteriorAlgebra R M) and defined as LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n. We also introduce the notation ⋀[R]^n M for exteriorPower R n M.

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 ExteriorAlgebra.lift R f cond.

The canonical linear map M → ExteriorAlgebra R M is denoted ExteriorAlgebra.ι R.

Theorems #

The main theorems proved ensure that ExteriorAlgebra R M satisfies the universal property of the exterior algebra.

  1. ι_comp_lift is the fact that the composition of ι R with lift R f cond agrees with f.
  2. lift_unique ensures the uniqueness of lift R f cond with respect to 1.

Definitions #

Implementation details #

The exterior algebra of M is constructed as simply CliffordAlgebra (0 : QuadraticForm R M), as this avoids us having to duplicate API.

@[reducible, inline]
abbrev ExteriorAlgebra (R : Type u1) [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] :
Type (max u2 u1)

The exterior algebra of an R-module M.

Equations
Instances For
    @[reducible, inline]
    abbrev ExteriorAlgebra.ι (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :

    The canonical linear map M →ₗ[R] ExteriorAlgebra R M.

    Equations
    Instances For
      @[reducible, inline]
      abbrev ExteriorAlgebra.exteriorPower (R : Type u1) [CommRing R] (n : ) (M : Type u2) [AddCommGroup M] [Module R M] :

      Definition of the nth exterior power of a R-module N. We introduce the notation ⋀[R]^n M for exteriorPower R n M.

      Equations
      Instances For

        Definition of the nth exterior power of a R-module N. We introduce the notation ⋀[R]^n M for exteriorPower R n M.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem ExteriorAlgebra.ι_sq_zero {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (m : M) :

          As well as being linear, ι m squares to zero.

          theorem ExteriorAlgebra.comp_ι_sq_zero {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] (g : ExteriorAlgebra R M →ₐ[R] A) (m : M) :
          @[simp]
          theorem ExteriorAlgebra.lift_symm_apply (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] :
          ∀ (a : ExteriorAlgebra R M →ₐ[R] A), (ExteriorAlgebra.lift R).symm a = ((CliffordAlgebra.lift 0).symm a),
          def ExteriorAlgebra.lift (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] :
          { f : M →ₗ[R] A // ∀ (m : M), f m * f m = 0 } (ExteriorAlgebra R M →ₐ[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 ExteriorAlgebra R M to A.

          Equations
          Instances For
            @[simp]
            theorem ExteriorAlgebra.ι_comp_lift (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup 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) :
            ((ExteriorAlgebra.lift R) f, cond).toLinearMap ∘ₗ ExteriorAlgebra.ι R = f
            @[simp]
            theorem ExteriorAlgebra.lift_ι_apply (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup 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) :
            ((ExteriorAlgebra.lift R) f, cond) ((ExteriorAlgebra.ι R) x) = f x
            @[simp]
            theorem ExteriorAlgebra.lift_unique (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup 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 : ExteriorAlgebra R M →ₐ[R] A) :
            g.toLinearMap ∘ₗ ExteriorAlgebra.ι R = f g = (ExteriorAlgebra.lift R) f, cond
            @[simp]
            theorem ExteriorAlgebra.lift_comp_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] (g : ExteriorAlgebra R M →ₐ[R] A) :
            (ExteriorAlgebra.lift R) g.toLinearMap ∘ₗ ExteriorAlgebra.ι R, = g
            theorem ExteriorAlgebra.hom_ext {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {A : Type u_1} [Semiring A] [Algebra R A] {f : ExteriorAlgebra R M →ₐ[R] A} {g : ExteriorAlgebra R M →ₐ[R] A} (h : f.toLinearMap ∘ₗ ExteriorAlgebra.ι R = g.toLinearMap ∘ₗ ExteriorAlgebra.ι R) :
            f = g

            See note [partially-applied ext lemmas].

            theorem ExteriorAlgebra.induction {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {C : ExteriorAlgebra R MProp} (algebraMap : ∀ (r : R), C ((_root_.algebraMap R (ExteriorAlgebra R M)) r)) (ι : ∀ (x : M), C ((ExteriorAlgebra.ι R) x)) (mul : ∀ (a b : ExteriorAlgebra R M), C aC bC (a * b)) (add : ∀ (a b : ExteriorAlgebra R M), C aC bC (a + b)) (a : ExteriorAlgebra R M) :
            C a

            If C holds for the algebraMap of r : R into ExteriorAlgebra R M, the ι of x : M, and is preserved under addition and muliplication, then it holds for all of ExteriorAlgebra R M.

            The left-inverse of algebraMap.

            Equations
            Instances For
              theorem ExteriorAlgebra.algebraMap_leftInverse {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] :
              Function.LeftInverse ExteriorAlgebra.algebraMapInv (algebraMap R (ExteriorAlgebra R M))
              @[simp]
              theorem ExteriorAlgebra.algebraMap_inj {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (x : R) (y : R) :
              @[simp]
              theorem ExteriorAlgebra.algebraMap_eq_zero_iff {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (x : R) :
              (algebraMap R (ExteriorAlgebra R M)) x = 0 x = 0
              @[simp]
              theorem ExteriorAlgebra.algebraMap_eq_one_iff {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (x : R) :
              (algebraMap R (ExteriorAlgebra R M)) x = 1 x = 1
              @[simp]
              theorem ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (r : R) :
              ∀ (x : Invertible ((algebraMap R (ExteriorAlgebra R M)) r)), r = (ExteriorAlgebra.algebraMapInv ((algebraMap R (ExteriorAlgebra R M)) r))

              Invertibility in the exterior algebra is the same as invertibility of the base ring.

              Equations
              Instances For

                The canonical map from ExteriorAlgebra R M into TrivSqZeroExt R M that sends ExteriorAlgebra.ι to TrivSqZeroExt.inr.

                Equations
                Instances For
                  @[simp]
                  theorem ExteriorAlgebra.toTrivSqZeroExt_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] (x : M) :
                  ExteriorAlgebra.toTrivSqZeroExt ((ExteriorAlgebra.ι R) x) = TrivSqZeroExt.inr x

                  The left-inverse of ι.

                  As an implementation detail, we implement this using TrivSqZeroExt which has a suitable algebra structure.

                  Equations
                  Instances For
                    theorem ExteriorAlgebra.ι_leftInverse {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :
                    Function.LeftInverse ExteriorAlgebra.ιInv (ExteriorAlgebra.ι R)
                    @[simp]
                    theorem ExteriorAlgebra.ι_inj (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (y : M) :
                    @[simp]
                    theorem ExteriorAlgebra.ι_eq_zero_iff {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) :
                    @[simp]
                    theorem ExteriorAlgebra.ι_eq_algebraMap_iff {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (r : R) :
                    @[simp]
                    theorem ExteriorAlgebra.ι_ne_one {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] [Nontrivial R] (x : M) :

                    The generators of the exterior algebra are disjoint from its scalars.

                    @[simp]
                    theorem ExteriorAlgebra.ι_add_mul_swap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (y : M) :
                    theorem ExteriorAlgebra.ι_mul_prod_list {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : } (f : Fin nM) (i : Fin n) :
                    (ExteriorAlgebra.ι R) (f i) * (List.ofFn fun (i : Fin n) => (ExteriorAlgebra.ι R) (f i)).prod = 0

                    The product of n terms of the form ι R m is an alternating map.

                    This is a special case of MultilinearMap.mkPiAlgebraFin, and the exterior algebra version of TensorAlgebra.tprod.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem ExteriorAlgebra.ιMulti_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : } (v : Fin nM) :
                      (ExteriorAlgebra.ιMulti R n) v = (List.ofFn fun (i : Fin n) => (ExteriorAlgebra.ι R) (v i)).prod
                      @[simp]
                      theorem ExteriorAlgebra.ιMulti_zero_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (v : Fin 0M) :
                      @[simp]
                      theorem ExteriorAlgebra.ιMulti_succ_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : } (v : Fin n.succM) :
                      theorem ExteriorAlgebra.ιMulti_succ_curryLeft {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : } (m : M) :
                      (ExteriorAlgebra.ιMulti R n.succ).curryLeft m = (LinearMap.mulLeft R ((ExteriorAlgebra.ι R) m)).compAlternatingMap (ExteriorAlgebra.ιMulti R n)
                      theorem ExteriorAlgebra.ιMulti_range (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ) :

                      The image of ExteriorAlgebra.ιMulti R n is contained in the nth exterior power.

                      The image of ExteriorAlgebra.ιMulti R n spans the nth exterior power, as a submodule of the exterior algebra.

                      @[reducible, inline]
                      abbrev ExteriorAlgebra.ιMulti_family (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ) {I : Type u_2} [LinearOrder I] (v : IM) (s : { s : Finset I // s.card = n }) :

                      Given a linearly ordered family v of vectors of M and a natural number n, produce the family of nfold exterior products of elements of v, seen as members of the exterior algebra.

                      Equations
                      Instances For

                        An ExteriorAlgebra over a nontrivial ring is nontrivial.

                        Equations
                        • =

                        Functoriality of the exterior algebra.

                        def ExteriorAlgebra.map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) :

                        The morphism of exterior algebras induced by a linear map.

                        Equations
                        Instances For
                          @[simp]
                          theorem ExteriorAlgebra.map_comp_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) :
                          (ExteriorAlgebra.map f).toLinearMap ∘ₗ ExteriorAlgebra.ι R = ExteriorAlgebra.ι R ∘ₗ f
                          @[simp]
                          theorem ExteriorAlgebra.map_apply_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (m : M) :
                          @[simp]
                          theorem ExteriorAlgebra.map_apply_ιMulti {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {n : } (f : M →ₗ[R] N) (m : Fin nM) :
                          @[simp]
                          theorem ExteriorAlgebra.map_comp_ιMulti {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {n : } (f : M →ₗ[R] N) :
                          (ExteriorAlgebra.map f).toLinearMap.compAlternatingMap (ExteriorAlgebra.ιMulti R n) = (ExteriorAlgebra.ιMulti R n).compLinearMap f
                          @[simp]
                          theorem ExteriorAlgebra.map_id {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :
                          @[simp]
                          theorem ExteriorAlgebra.map_comp_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} {N' : Type u5} [AddCommGroup N] [Module R N] [AddCommGroup N'] [Module R N'] (f : M →ₗ[R] N) (g : N →ₗ[R] N') :
                          theorem ExteriorAlgebra.toTrivSqZeroExt_comp_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module Rᵐᵒᵖ N] [IsCentralScalar R N] (f : M →ₗ[R] N) :
                          ExteriorAlgebra.toTrivSqZeroExt.comp (ExteriorAlgebra.map f) = (TrivSqZeroExt.map f).comp ExteriorAlgebra.toTrivSqZeroExt
                          theorem ExteriorAlgebra.ιInv_comp_map {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) :
                          ExteriorAlgebra.ιInv ∘ₗ (ExteriorAlgebra.map f).toLinearMap = f ∘ₗ ExteriorAlgebra.ιInv
                          @[simp]

                          For a linear map f from M to N, ExteriorAlgebra.map g is a retraction of ExteriorAlgebra.map f iff g is a retraction of f.

                          theorem ExteriorAlgebra.map_injective {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {N : Type u4} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : ∃ (g : N →ₗ[R] M), g ∘ₗ f = LinearMap.id) :

                          A morphism of modules that admits a linear retraction induces an injective morphism of exterior algebras.

                          @[simp]

                          A morphism of modules is surjective if and only the morphism of exterior algebras that it induces is surjective.

                          theorem ExteriorAlgebra.map_injective_field {K : Type u_2} {E : Type u_3} {F : Type u_4} [Field K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] {f : E →ₗ[K] F} (hf : LinearMap.ker f = ) :

                          An injective morphism of vector spaces induces an injective morphism of exterior algebras.

                          The canonical image of the TensorAlgebra in the ExteriorAlgebra, which maps TensorAlgebra.ι R x to ExteriorAlgebra.ι R x.

                          Equations
                          Instances For
                            @[simp]
                            theorem TensorAlgebra.toExterior_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (m : M) :
                            TensorAlgebra.toExterior ((TensorAlgebra.ι R) m) = (ExteriorAlgebra.ι R) m