A Laurent-polynomial path in the special linear group #
Specializing the generic Laurent unit in the two-coordinate unit diagonal family recovers
Mathlib's Matrix.SpecialLinearGroup.diag2n matrix. This supplies the diagonal one-parameter
family used to prove connectedness of SLₙ.
Main declarations #
TauCeti.SpecialLinear.map_diag2nUnit_genericUnit: specialization of the generic Laurent matrix.
theorem
TauCeti.SpecialLinear.map_diag2nUnit_genericUnit
{K : Type u}
[Field K]
{m : Type v}
[Fintype m]
[DecidableEq m]
{i j : m}
(hij : i ≠ j)
(b : Kˣ)
:
Evaluating the generic Laurent diagonal matrix at a unit b gives the ordinary
two-coordinate diagonal matrix with entries b and b⁻¹.