Base change of the standard symplectic isotropic flag subgroup

For any homomorphism of commutative rings R → K, the scalar extension of the coordinate Hopf algebra of the standard complete isotropic flag stabilizer in Sp₂ₘ is canonically the coordinate Hopf algebra of that stabilizer over K. The comparison commutes with coordinate restriction from the symplectic group. Thus geometric fibers of the flag subgroup can be studied using its explicit matrix presentation over the residue field. The induced point equivalence preserves the flag-preserving symplectic matrix over every commutative value algebra.

The defining equations are the matrix entries below the diagonal in the self-dual flag order. Transporting these equations uses the general-linear and symplectic base-change comparisons; the quotient construction uses CommHopfAlgCat.quotientBaseChangeIsoOfMapEq. The defining-ideal proof follows TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.Borel; the matrix-point interface follows TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.BaseChange.

References

• J. S. Milne, Algebraic Groups (2017), §24.6 (symplectic groups and isotropic flags).
• B. Conrad, Reductive Group Schemes (2014), §5.1 (Borel subgroups over a base).

theorem TauCeti.Symplectic.IsotropicFlag.map_baseChangeHopfIdeal_definingHopfIdeal (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : (CommHopfAlgCat.baseChangeHopfIdeal (definingHopfIdeal R m)).map (CommHopfAlgCat.Hom.hom (Symplectic.coordinateHopfAlgebraBaseChangeIso R K m).hom) = definingHopfIdeal K m

The symplectic base-change comparison carries the scalar-extended flag ideal onto the flag ideal over the new base, including nonflat changes of base.

noncomputable def TauCeti.Symplectic.IsotropicFlag.coordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : CommHopfAlgCat.baseChange (coordinateHopfAlgebra R m) ≅ coordinateHopfAlgebra K m

Scalar extension of the flag subgroup's coordinate Hopf algebra is the flag coordinate Hopf algebra over the new base. No flatness, field, or characteristic hypothesis is needed.

@[simp]

theorem TauCeti.Symplectic.IsotropicFlag.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R m)) (coordinateHopfAlgebraBaseChangeIso R K m).hom = CategoryTheory.CategoryStruct.comp (Symplectic.coordinateHopfAlgebraBaseChangeIso R K m).hom (coordinateMap K m)

Base change of the flag restriction agrees with restriction over the new base under the canonical symplectic and flag comparisons.

@[simp]

theorem TauCeti.Symplectic.IsotropicFlag.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom_assoc (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) {Z : CommHopfAlgCat K} (h : coordinateHopfAlgebra K m ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R m)) (CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K m).hom h) = CategoryTheory.CategoryStruct.comp (Symplectic.coordinateHopfAlgebraBaseChangeIso R K m).hom (CategoryTheory.CategoryStruct.comp (coordinateMap K m) h)

Base change of the flag restriction agrees with restriction over the new base under the canonical symplectic and flag comparisons.

theorem TauCeti.Symplectic.IsotropicFlag.coordinateHopfAlgebraBaseChangeIso_hom_tmul_coordinateMap (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) (s : K) (x : ↑(Symplectic.coordinateHopfAlgebra R m)) : (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K m).hom) (s ⊗ₜ[R] (CommHopfAlgCat.Hom.hom (coordinateMap R m)) x) = (CommHopfAlgCat.Hom.hom (coordinateMap K m)) ((CommHopfAlgCat.Hom.hom (Symplectic.coordinateHopfAlgebraBaseChangeIso R K m).hom) (s ⊗ₜ[R] x))

On a pure tensor of a restricted symplectic function, the flag comparison is the ambient symplectic comparison followed by restriction.

theorem TauCeti.Symplectic.IsotropicFlag.pointsMulEquiv_baseChangeIsoPointsMulEquiv (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) (A : CommAlgCat K) (q : ↑(HopfAlgebra.points A)) : (pointsMulEquiv R m) ((CommHopfAlgCat.baseChangeIsoPointsMulEquiv (coordinateHopfAlgebraBaseChangeIso R K m).symm A) q) = (pointsMulEquiv K m) q

The flag base-change point equivalence preserves the flag-preserving symplectic matrix over every commutative value algebra.