English
If f is a surjective isometry between quadratic forms, then CliffordAlgebra.map f is surjective.
Русский
Если f является сюръективной изометрией между квадратичными формами, то CliffordAlgebra.map f сюръективно отображает CliffordAlgebra Q1 в CliffordAlgebra Q2.
LaTeX
$$$ \forall y \in \mathrm{CliffordAlgebra}(Q_2), \exists x \in \mathrm{CliffordAlgebra}(Q_1): \mathrm{CliffordAlgebra.map} f (x) = y. $$$
Lean4
/-- If a linear map preserves the quadratic forms and is surjective, then the algebra
maps it induces between Clifford algebras is also surjective. -/
theorem map_surjective {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂)
(hf : Function.Surjective f) : Function.Surjective (CliffordAlgebra.map f) :=
CliffordAlgebra.induction (fun r ↦ ⟨algebraMap R (CliffordAlgebra Q₁) r, by simp only [AlgHom.commutes]⟩)
(fun y ↦
let ⟨x, hx⟩ := hf y;
⟨CliffordAlgebra.ι Q₁ x, by simp only [map_apply_ι, hx]⟩)
(fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x * y, by simp only [map_mul, hx, hy]⟩)
(fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x + y, by simp only [map_add, hx, hy]⟩)
