English
If x lies in the Lipschitz group, then conjugation by x sends vectors in M to linear maps that still land in the image of ι Q. In particular, ConjAct.x acts by automorphisms preserving range(ι Q).
Русский
Если x принадлежит LipschitzGroup, то конъюгация x отправляет вектора в M в линейные отображения, которые по-прежнему попадают в образ ι_Q; диапазон ι_Q сохраняется.
LaTeX
$$$$\\forall x\\in\\mathrm{lipschitzGroup}(Q),\\ ConjAct^{\\!toConjAct}(x) \\cdot \\mathrm{range}(\\iota_Q) \\subseteq \\mathrm{range}(\\iota_Q). $$$$
Lean4
/-- The conjugation action by elements of the Lipschitz group keeps vectors as vectors. -/
theorem conjAct_smul_ι_mem_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q) [Invertible (2 : R)] (m : M) :
ConjAct.toConjAct x • ι Q m ∈ LinearMap.range (ι Q) :=
by
unfold lipschitzGroup at hx
rw [ConjAct.units_smul_def, ConjAct.ofConjAct_toConjAct]
induction hx using Subgroup.closure_induction'' generalizing m with
| mem x hx =>
obtain ⟨a, ha⟩ := hx
letI := x.invertible
letI : Invertible (ι Q a) := by rwa [ha]
letI : Invertible (Q a) := invertibleOfInvertibleι Q a
simp_rw [← invOf_units x, ← ha, ι_mul_ι_mul_invOf_ι, LinearMap.mem_range_self]
| inv_mem x hx =>
obtain ⟨a, ha⟩ := hx
letI := x.invertible
letI : Invertible (ι Q a) := by rwa [ha]
letI : Invertible (Q a) := invertibleOfInvertibleι Q a
letI := invertibleNeg (ι Q a)
letI := Invertible.map involute (ι Q a)
simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, LinearMap.mem_range_self]
| one => simp_rw [inv_one, Units.val_one, one_mul, mul_one, LinearMap.mem_range_self]
| mul y z _ _ hy hz =>
simp_rw [mul_inv_rev, Units.val_mul]
suffices ↑y * (↑z * ι Q m * ↑z⁻¹) * ↑y⁻¹ ∈ _ by simpa only [mul_assoc] using this
obtain ⟨z', hz'⟩ := hz m
obtain ⟨y', hy'⟩ := hy z'
simp_rw [← hz', ← hy', LinearMap.mem_range_self]
