English
The natural map from ExteriorAlgebra toTrivSqZeroExt composed with map f equals TrivSqZeroExt.map f composed with toTrivSqZeroExt; i.e., the two routes give the same result on maps.
Русский
Естественное отображение ExteriorAlgebra →toTrivSqZeroExt после map f равно TrivSqZeroExt.map f после toTrivSqZeroExt; оба пути дают одинаковый результат.
LaTeX
$$$ toTrivSqZeroExt \\circ (map\\ f) = (TrivSqZeroExt.map\\ f) \\circ toTrivSqZeroExt. $$$
Lean4
/-- 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`. -/
@[simp]
theorem leftInverse_map_iff {f : M →ₗ[R] N} {g : N →ₗ[R] M} : LeftInverse (map g) (map f) ↔ LeftInverse g f :=
by
refine ⟨fun h x => ?_, fun h => CliffordAlgebra.leftInverse_map_of_leftInverse _ _ h⟩
simpa using h (ι _ x)
