English
Let F be a real finite-dimensional inner product space. For any φ in the orthogonal group O(F) there exists a finite sequence of vectors v1, v2, ..., vm in F with m ≤ n (where n bounds the dimension of the orthogonal complement of the fixed subspace of φ) such that φ is the product of reflections across the hyperplanes orthogonal to these vectors, i.e. φ equals the composition of reflections refl(v1), refl(v2), ..., refl(vm).
Русский
Пусть F — конечномерное вещественное вложенное векторное пространство с внутренним произведением. Для любого φ из ортогональной группы O(F) существует конечная последовательность векторов v1, v2, ..., vm в F такая, что m ≤ n и φ является произведением отражений в гиперплоскостях, ортогональных v1, v2, ..., vm.
LaTeX
$$$\\exists l :\\text{List } F, l$.length ≤ n ∧ φ = (l.map (fun v => (\\mathbb{R} \\cdot v)^{\\perp}.reflection)).prod$$
Lean4
/-- An element `φ` of the orthogonal group of `F` can be factored as a product of reflections, and
specifically at most as many reflections as the dimension of the complement of the fixed subspace
of `φ`. -/
theorem reflections_generate_dim_aux [FiniteDimensional ℝ F] {n : ℕ} (φ : F ≃ₗᵢ[ℝ] F)
(hn : finrank ℝ (ker (ContinuousLinearMap.id ℝ F - φ))ᗮ ≤ n) :
∃ l : List F, l.length ≤ n ∧ φ = (l.map fun v => (ℝ ∙ v)ᗮ.reflection).prod := by
-- We prove this by strong induction on `n`, the dimension of the orthogonal complement of the
-- fixed subspace of the endomorphism `φ`
induction n generalizing φ with
| zero => -- Base case: `n = 0`, the fixed subspace is the whole space, so `φ = id`
refine ⟨[], rfl.le, show φ = 1 from ?_⟩
have : ker (ContinuousLinearMap.id ℝ F - φ) = ⊤ := by
rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
symm
ext x
have := LinearMap.congr_fun (LinearMap.ker_eq_top.mp this) x
simpa only [sub_eq_zero, ContinuousLinearMap.coe_sub, LinearMap.sub_apply, LinearMap.zero_apply] using this
| succ n IH =>
-- Inductive step. Let `W` be the fixed subspace of `φ`. We suppose its complement to have
-- dimension at most n + 1.
let W := ker (ContinuousLinearMap.id ℝ F - φ)
have hW : ∀ w ∈ W, φ w = w := fun w hw => (sub_eq_zero.mp hw).symm
by_cases hn' : finrank ℝ Wᗮ ≤ n
· obtain ⟨V, hV₁, hV₂⟩ := IH φ hn'
exact
⟨V, hV₁.trans n.le_succ, hV₂⟩
-- Take a nonzero element `v` of the orthogonal complement of `W`.
haveI : Nontrivial Wᗮ := nontrivial_of_finrank_pos (by cutsat : 0 < finrank ℝ Wᗮ)
obtain ⟨v, hv⟩ := exists_ne (0 : Wᗮ)
have hφv : φ v ∈ Wᗮ := by
intro w hw
rw [← hW w hw, LinearIsometryEquiv.inner_map_map]
exact v.prop w hw
have hv' : (v : F) ∉ W := by
intro h
exact
hv
((mem_left_iff_eq_zero_of_disjoint W.orthogonal_disjoint).mp h)
-- Let `ρ` be the reflection in `v - φ v`; this is designed to swap `v` and `φ v`
let x : F := v - φ v
let ρ := (ℝ ∙ x)ᗮ.reflection
let V := ker (ContinuousLinearMap.id ℝ F - φ.trans ρ)
have hV : ∀ w, ρ (φ w) = w → w ∈ V := by
intro w hw
change w - ρ (φ w) = 0
rw [sub_eq_zero, hw]
-- Everything fixed by `φ` is fixed by `φ.trans ρ`
have H₂V : W ≤ V := by
intro w hw
apply hV
rw [hW w hw]
refine reflection_mem_subspace_eq_self ?_
rw [mem_orthogonal_singleton_iff_inner_left]
exact Submodule.sub_mem _ v.prop hφv _ hw
have H₁V : (v : F) ∈ V := by
apply hV
have : ρ v = φ v := reflection_sub (φ.norm_map v).symm
rw [← this]
exact
reflection_reflection _
_
-- By dimension-counting, the complement of the fixed subspace of `φ.trans ρ` has dimension at
-- most `n`
have : finrank ℝ Vᗮ ≤ n := by
change finrank ℝ Wᗮ ≤ n + 1 at hn
have : finrank ℝ W + 1 ≤ finrank ℝ V :=
finrank_lt_finrank_of_lt (SetLike.lt_iff_le_and_exists.2 ⟨H₂V, v, H₁V, hv'⟩)
have : finrank ℝ V + finrank ℝ Vᗮ = finrank ℝ F := V.finrank_add_finrank_orthogonal
have : finrank ℝ W + finrank ℝ Wᗮ = finrank ℝ F := W.finrank_add_finrank_orthogonal
omega
-- So apply the inductive hypothesis to `φ.trans ρ`
obtain ⟨l, hl, hφl⟩ := IH (ρ * φ) this
refine ⟨x :: l, Nat.succ_le_succ hl, ?_⟩
rw [List.map_cons, List.prod_cons]
have := congr_arg (ρ * ·) hφl
dsimp only at this
rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this
