English
For x a unit in CliffordAlgebra Q, the coe image lies in the submonoid image of LipschitzGroup iff x itself lies in LipschitzGroup.
Русский
Для единицы x в CliffordAlgebra Q образ через coe лежит в образе подмона LipschitzGroup тогда и только тогда, когда сама x принадлежит LipschitzGroup.
LaTeX
$$$$\\uparrow x \\in (\\mathrm{lipschitzGroup}(Q)).toSubmonoid.map (\\mathrm{Units.coeHom} \\lvert\\!\\!\\! CliffordAlgebra Q) \iff x \\in \\mathrm{lipschitzGroup}(Q).$$$$
Lean4
/-- If x is in `lipschitzGroup Q`, then `(ι Q).range` is closed under twisted conjugation.
The reverse statement presumably is true only in finite dimensions. -/
theorem conjAct_smul_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q) [Invertible (2 : R)] :
ConjAct.toConjAct x • LinearMap.range (ι Q) = LinearMap.range (ι Q) :=
by
suffices ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • LinearMap.range (ι Q) ≤ LinearMap.range (ι Q)
by
apply le_antisymm
· exact this _ hx
· have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)
refine Eq.trans_le ?_ this
simp only [map_inv, smul_inv_smul]
intro x hx
erw [Submodule.map_le_iff_le_comap]
rintro _ ⟨m, rfl⟩
exact conjAct_smul_ι_mem_range_ι hx _
