Theorems · Definition · linear algebra

ExteriorAlgebra.lift

(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 // ∀ (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.

Defined in

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Cited by

6 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleSemiringAlgebra