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.

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]
def 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.

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

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

    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) :
      g (↑(ExteriorAlgebra.ι R) m) * g (↑(ExteriorAlgebra.ι R) m) = 0
      @[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 = { val := ↑((CliffordAlgebra.lift 0).symm a), property := (_ : ∀ (m : M), ↑((CliffordAlgebra.lift 0).symm a) m * ↑((CliffordAlgebra.lift 0).symm a) m = 0) }
      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 : 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.

      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) :
        LinearMap.comp (AlgHom.toLinearMap (↑(ExteriorAlgebra.lift R) { val := f, property := cond })) (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) { val := f, property := 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) :
        LinearMap.comp (AlgHom.toLinearMap g) (ExteriorAlgebra.ι R) = f g = ↑(ExteriorAlgebra.lift R) { val := f, property := 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) { val := LinearMap.comp (AlgHom.toLinearMap g) (ExteriorAlgebra.ι R), property := (_ : ∀ (m : M), g (↑(ExteriorAlgebra.ι R) m) * g (↑(ExteriorAlgebra.ι R) m) = 0) } = 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} (h_grade0 : (r : R) → C (↑(algebraMap R (ExteriorAlgebra R M)) r)) (h_grade1 : (x : M) → C (↑(ExteriorAlgebra.ι R) x)) (h_mul : (a b : ExteriorAlgebra R M) → C aC bC (a * b)) (h_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.

        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) :
          ↑(algebraMap R (ExteriorAlgebra R M)) x = ↑(algebraMap R (ExteriorAlgebra R M)) y x = y
          @[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
          theorem ExteriorAlgebra.isUnit_algebraMap {R : Type u1} [CommRing R] (M : Type u2) [AddCommGroup M] [Module R M] (r : R) :
          @[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.

          Instances For

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

            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.

              Instances For
                theorem ExteriorAlgebra.ι_leftInverse {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] :
                Function.LeftInverse ExteriorAlgebra.ιInv.toAddHom ↑(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) :
                ↑(ExteriorAlgebra.ι R) x = 0 x = 0
                @[simp]
                theorem ExteriorAlgebra.ι_eq_algebraMap_iff {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (x : M) (r : R) :
                ↑(ExteriorAlgebra.ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r x = 0 r = 0
                @[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.prod (List.ofFn fun i => ↑(ExteriorAlgebra.ι R) (f i)) = 0
                def ExteriorAlgebra.ιMulti (R : Type u1) [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (n : ) :

                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.

                Instances For
                  theorem ExteriorAlgebra.ιMulti_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {n : } (v : Fin nM) :
                  @[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 (Nat.succ n)M) :

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

                  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