English
The morphism of exterior algebras induced by a linear map f: M → N exists and is functorial: map f is an R-algebra homomorphism extending f.
Русский
Существует и к ней применима морфизм алгебр внешних степеней, индуцированный линейным отображением f: M → N; отображение map f является гомоморфизмом R-алгебр, расширяющим f.
LaTeX
$$$ map\\_f = \\operatorname{ExteriorAlgebra}(f) : \\operatorname{ExteriorAlgebra}_R M \\to \\operatorname{ExteriorAlgebra}_R N, \\quad map_f \\circ \\iota_R = \\iota_R \\circ f. $$$
Lean4
/-- The morphism of exterior algebras induced by a linear map. -/
def map (f : M →ₗ[R] N) : ExteriorAlgebra R M →ₐ[R] ExteriorAlgebra R N :=
CliffordAlgebra.map { f with map_app' := fun _ => rfl }
