English
For a finite-dimensional subspace K, the determinant of the reflection map on K is (-1)^{finrank K⊥}.
Русский
Для конечномерного подпространства K детерминант отображения отражения равен (-1)^{finrank(K⊥)}.
LaTeX
$$$ \det(K.\!reflection) = (-1)^{\operatorname{finrank} K^{\perp}}. $$$
Lean4
@[simp]
theorem det_reflection : LinearMap.det K.reflection.toLinearMap = (-1) ^ finrank 𝕜 Kᗮ :=
by
by_cases hK : FiniteDimensional 𝕜 Kᗮ
swap
· rw [finrank_of_infinite_dimensional hK, pow_zero, LinearMap.det_eq_one_of_finrank_eq_zero]
exact finrank_of_infinite_dimensional fun h ↦ hK (h.finiteDimensional_submodule _)
let e := K.prodEquivOfIsCompl _ K.isCompl_orthogonal_of_hasOrthogonalProjection
let b := (finBasis 𝕜 K).prod (finBasis 𝕜 Kᗮ)
have : LinearMap.toMatrix b b (e.symm ∘ₗ K.reflection.toLinearMap ∘ₗ e.symm.symm) = Matrix.fromBlocks 1 0 0 (-1) := by
ext (_ | _) (_ | _) <;>
simp [LinearMap.toMatrix_apply, b, Matrix.one_apply, Finsupp.single_apply, e, eq_comm,
reflection_mem_subspace_eq_self, reflection_mem_subspace_orthogonalComplement_eq_neg]
rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁, Matrix.det_one,
one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
