English
If g is a left inverse of f between quadratic forms (g ∘ f = id on Q1) and both preserve the forms, then the induced Clifford maps form a left inverse: map g is a left inverse of map f.
Русский
Если g является левым обратным к f между квадратичными формами (g ∘ f = id на Q1) и оба отображают формы, то индуцированные отображения CliffordAlgebra образуют левый обратный: map g является левым обратным к map f.
LaTeX
$$$ \text{LeftInverse }(\mathrm{map} g) (\mathrm{map} f). $$$
Lean4
/-- If `f` is a linear map from `M₁` to `M₂` that preserves the quadratic forms, and if it has
a linear retraction `g` that also preserves the quadratic forms, then `CliffordAlgebra.map g`
is a retraction of `CliffordAlgebra.map f`. -/
theorem leftInverse_map_of_leftInverse {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂)
(g : Q₂ →qᵢ Q₁) (h : LeftInverse g f) : LeftInverse (map g) (map f) :=
by
refine fun x => ?_
replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h
rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
