Lifting special orthogonal matrices #
When 2 is invertible, a special orthogonal matrix lifts across a quotient by a square-zero
ideal. Starting from arbitrary lifts of its entries, let E = M Mᵀ - 1 be the error in the
orthogonality equation. Its entries lie in the ideal and E is symmetric. Multiplication by
1 - E / 2 corrects the error; all quadratic terms vanish because the ideal is square-zero.
The corrected matrix is orthogonal. Its determinant squares to one and is congruent to one
modulo the ideal. Invertibility of 2 then forces its determinant to equal one, so the lift is
special orthogonal.
Main declarations #
Matrix.SpecialOrthogonalGroup.map_quotient_mk_surjective_of_sq_eq_bot: special orthogonal matrices lift across square-zero quotients when2is invertible.
References #
- The Stacks Project, Tag 00TH, for the infinitesimal lifting criterion for formal smoothness.
- SGA 3, Exposé XXIII, for the split special orthogonal group away from characteristic two.
theorem
Matrix.SpecialOrthogonalGroup.map_quotient_mk_surjective_of_sq_eq_bot
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{R : Type u}
[CommRing R]
[Invertible 2]
(I : Ideal R)
(hI : I ^ 2 = ⊥)
:
Every special orthogonal matrix modulo a square-zero ideal lifts to a special orthogonal
matrix when 2 is invertible in the coefficient ring.