English
Using involution, the twisted conjugation by an invertible Lipschitz group element keeps the image of ι in its range; more precisely, involute(↑x) ι Q m ↑x^{-1} ∈ range(ι Q).
Русский
С коммутированием через инволюцию, образ ι сохраняется в диапазоне; involute(↑x) ι Q m ↑x^{-1} ∈ range(ι Q).
LaTeX
$$$$\\text{involute}(Q)\\, (x) \\; ι_Q(m) \\; x^{-1} \\in \\mathrm{range}(ι_Q).$$$$
Lean4
/-- This is another version of `lipschitzGroup.conjAct_smul_ι_mem_range_ι` which uses `involute`. -/
theorem involute_act_ι_mem_range_ι [Invertible (2 : R)] {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q) (b : M) :
involute (Q := Q) ↑x * ι Q b * ↑x⁻¹ ∈ LinearMap.range (ι Q) :=
by
unfold lipschitzGroup at hx
induction hx using Subgroup.closure_induction'' generalizing b 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, involute_ι, neg_mul, ι_mul_ι_mul_invOf_ι Q a b, ← map_neg, 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, map_invOf, involute_ι, invOf_neg, neg_mul, invOf_ι_mul_ι_mul_ι, ← map_neg,
LinearMap.mem_range_self]
| one => simp_rw [inv_one, Units.val_one, map_one, one_mul, mul_one, LinearMap.mem_range_self]
| mul y z _ _ hy hz =>
simp_rw [mul_inv_rev, Units.val_mul, map_mul]
suffices involute (Q := Q) ↑y * (involute (Q := Q) ↑z * ι Q b * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
simpa only [mul_assoc] using this
obtain ⟨z', hz'⟩ := hz b
obtain ⟨y', hy'⟩ := hy z'
simp_rw [← hz', ← hy', LinearMap.mem_range_self]
