Determinants along a double coset of GL ι R #
The determinant is constant on a double coset H₁ g H₂ as soon as every coefficient has
determinant one. Nothing here is arithmetic: the argument is multiplicativity of Matrix.det,
so it holds over any commutative ring and any finite index type.
The arithmetic consumers — SL_n(ℤ) and the congruence subgroups inside it — specialise this
in TauCeti.NumberTheory.HeckeRing.GLn.Basic.
Main results #
DoubleCoset.det_eq_of_mem_doubleCoset_of_det_eq_one: the determinant is constant on a double coset with determinant-one coefficients.
theorem
DoubleCoset.det_eq_of_mem_doubleCoset_of_det_eq_one
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{R : Type u_2}
[CommRing R]
{H₁ H₂ : Subgroup (GL ι R)}
(h₁ : ∀ γ ∈ H₁, (↑γ).det = 1)
(h₂ : ∀ γ ∈ H₂, (↑γ).det = 1)
{a b : GL ι R}
(hb : b ∈ doubleCoset a ↑H₁ ↑H₂)
:
The determinant is constant on a double coset whose coefficients all have determinant one — the only property of the coefficient subgroups the argument uses.