Lifting symplectic isotropic flag matrices

A symplectic matrix preserving the standard complete isotropic flag factors as diag(P, P⁻ᵀ) [1 T; 0 1], with P upper triangular and invertible and T symmetric. Both parameters lift along surjective ring homomorphisms that reflect units, including quotients by nilpotent ideals, so the flag subgroup has the infinitesimal lifting property over every commutative ring, including characteristic two.

The factorization reuses GLSymplecticFin.exists_gaussian_decomposition_of_isUnit_toBlocks₁₁.

References

• J. S. Milne, Algebraic Groups (2017), §24.6.
• SGA 3, Exposé XXII, for the split symplectic group and its flag stabilizers.

@[simp]

theorem TauCeti.GLSymplecticFin.IsotropicFlag.leviHom_mem_matrixSubgroup {m : ℕ} {R : Type u_1} [CommRing R] (P : ↥(upperTriangularGroup (Fin m) R)) : leviHom ↑P ∈ matrixSubgroup m

An upper-triangular general-linear Levi element preserves the isotropic flag.

@[simp]

theorem TauCeti.GLSymplecticFin.IsotropicFlag.upperUnipotent_mem_matrixSubgroup {m : ℕ} {R : Type u_1} [CommRing R] (T : Matrix (Fin m) (Fin m) R) (hT : T.IsSymm) : upperUnipotent T hT ∈ matrixSubgroup m

Every symmetric upper unipotent block preserves the isotropic flag.

theorem TauCeti.GLSymplecticFin.IsotropicFlag.exists_leviHom_mul_upperUnipotent {m : ℕ} {R : Type u_1} [CommRing R] (g : ↥(matrixSubgroup m)) : ∃ (P : ↥(upperTriangularGroup (Fin m) R)) (T : Matrix (Fin m) (Fin m) R) (hT : T.IsSymm), ↑g = leviHom ↑P * upperUnipotent T hT

Every flag-preserving symplectic matrix is the product of an upper-triangular Levi element and an upper unipotent with symmetric block.

theorem TauCeti.GLSymplecticFin.IsotropicFlag.map_surjective {m : ℕ} {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) [IsLocalHom φ] (hφ : Function.Surjective ⇑φ) : Function.Surjective ⇑(map m φ)

A surjective ring homomorphism that reflects units induces a surjection on the symplectic isotropic flag subgroup. No invertibility of two is required.