English
There is an equivalence between linear maps M → A satisfying f(m)^2 = 0 and algebra homomorphisms ExteriorAlgebra R M → A.
Русский
Существует эквивалентность между линейными отображениями M → A, удовлетворяющими f(m)^2 = 0, и алгебра-хомоморфизмами ExteriorAlgebra R M → A.
LaTeX
$$ExteriorAlgebra.lift : { f : M →ₗ[R] A // ∀ m, f m * f m = 0 } ≃ (ExteriorAlgebra R M →ₐ[R] A)$$
Lean4
/-- 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`.
-/
@[simps! symm_apply]
def lift : { f : M →ₗ[R] A // ∀ m, f m * f m = 0 } ≃ (ExteriorAlgebra R M →ₐ[R] A) :=
Equiv.trans (Equiv.subtypeEquiv (Equiv.refl _) <| by simp) <| CliffordAlgebra.lift _
