The type C carrier over a field

The full-weight type C_(n+1) Kostant carrier is constructed over ℤ as the closed subgroup of GL_(2n+2) generated by the numbered root subgroups and its weight torus. After extension to a field, its matrix points are already known to be exactly the matrices preserving the standard alternating form. This file upgrades that pointwise statement to an equality of defining Hopf ideals over every field:

  baseChangeDefiningIdeal n k = Symplectic.definingHopfIdeal k (n + 1).

The resulting quotient isomorphism identifies the base-changed explicit carrier with the coordinate Hopf algebra of Sp_(2n+2). It is also promoted to an isomorphism from the scheme-theoretic base change of the integral carrier to the symplectic group scheme. The isomorphism commutes with the closed immersions into GL_(2n+2), and its action on algebra-valued points preserves the underlying matrix. This ambient-matrix compatibility prepares the later comparison of the already constructed integral pinning with the pinned symplectic group, rather than merely matching abstract groups of field-valued points.

Only the equality of ideals needs a field: the containment of the symplectic ideal in the transported carrier ideal, equivalently the statement that every carrier point preserves the standard alternating form, holds over every commutative ring.

Main declarations

• TauCeti.SpStd.symplecticDefiningHopfIdeal_le_baseChangeDefiningIdeal: over every commutative ring, the symplectic defining ideal is contained in the transported carrier ideal.
• TauCeti.SpStd.baseChangeDefiningIdeal_eq_symplecticDefiningHopfIdeal: over every field, the transported carrier and symplectic defining ideals agree.
• TauCeti.SpStd.baseChangeCoordinateSymplecticIso: the induced coordinate Hopf-algebra isomorphism with Sp_(2n+2).
• TauCeti.SpStd.baseChangeSymplecticIso: the induced group-scheme isomorphism from the base change of the integral carrier to Sp_(2n+2).
• TauCeti.SpStd.baseChangeSymplecticSchemePointsMulEquiv: the induced equivalence on scheme-valued points of the base-changed carrier.
• TauCeti.SpStd.baseChangeSymplecticPointsMulEquiv: the corresponding equivalence on points of the transported quotient presentation.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §§3--4.

theorem TauCeti.SpStd.symplecticDefiningHopfIdeal_le_baseChangeDefiningIdeal (n : ℕ) (A : Type u) [CommRing A] : Symplectic.definingHopfIdeal A (n + 1) ≤ baseChangeDefiningIdeal n A

The symplectic ideal is contained in the transported defining ideal of the full-weight type C_(n+1) carrier over every commutative ring. Equivalently, every point of the transported carrier preserves the standard alternating form.

theorem TauCeti.SpStd.baseChangeDefiningIdeal_eq_symplecticDefiningHopfIdeal (n : ℕ) (k : Type u) [Field k] : baseChangeDefiningIdeal n k = Symplectic.definingHopfIdeal k (n + 1)

Over a field, the transported defining ideal of the full-weight type C_(n+1) carrier is the symplectic ideal. Thus the explicit carrier obtained from the Kostant construction is scheme-theoretically Sp_(2n+2), not merely equal to it on field-valued points.

noncomputable def TauCeti.SpStd.baseChangeCoordinateSymplecticIso (n : ℕ) (k : Type u) [Field k] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k (n + 1 + (n + 1))) (baseChangeDefiningIdeal n k) ≅ Symplectic.coordinateHopfAlgebra k (n + 1)

Over a field, the coordinate Hopf algebra of the base-changed full-weight type C_(n+1) carrier is canonically the coordinate Hopf algebra of Sp_(2n+2).

Equations

• TauCeti.SpStd.baseChangeCoordinateSymplecticIso n k = CategoryTheory.eqToIso ⋯

@[simp]

theorem TauCeti.SpStd.mkQuotient_comp_baseChangeCoordinateSymplecticIso_hom (n : ℕ) (k : Type u) [Field k] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra k (n + 1 + (n + 1))) (baseChangeDefiningIdeal n k)) (baseChangeCoordinateSymplecticIso n k).hom = Symplectic.coordinateMap k (n + 1)

The carrier--symplectic coordinate isomorphism is compatible with their quotient maps from O(GL_(2n+2)/k).

@[simp]

theorem TauCeti.SpStd.mkQuotient_comp_baseChangeCoordinateSymplecticIso_inv (n : ℕ) (k : Type u) [Field k] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra k (n + 1 + (n + 1))) (Symplectic.definingHopfIdeal k (n + 1))) (baseChangeCoordinateSymplecticIso n k).inv = CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra k (n + 1 + (n + 1))) (baseChangeDefiningIdeal n k)

The inverse carrier--symplectic coordinate isomorphism carries the symplectic quotient map to the transported carrier quotient map.

The pinned carrier after base change

noncomputable def TauCeti.SpStd.baseChangeSymplecticIso (n : ℕ) (k : Type) [Field k] : baseChangeGroupScheme n k ≅ Symplectic.groupScheme k (n + 1)

The base-changed full-weight type-C_(n+1) Chevalley carrier is the symplectic group scheme.

It canonically identifies the scheme-theoretic base change of the integral Kostant carrier with Sp_(2n+2)/k. The following theorem records compatibility with their ambient closed immersions.

Equations

• TauCeti.SpStd.baseChangeSymplecticIso n k = TauCeti.SpStd.baseChangePresentationIso n k ≪≫ TauCeti.SpStd.baseChangePresentationSymplecticIso✝ n k

theorem TauCeti.SpStd.baseChangeSymplecticIso_hom_comp_inclusion (n : ℕ) (k : Type) [Field k] : CategoryTheory.CategoryStruct.comp (baseChangeSymplecticIso n k).hom (Symplectic.inclusion k (n + 1)) = baseChangeι n k

The carrier--symplectic group-scheme isomorphism preserves the ambient matrix.

In particular, every transported root subgroup and torus map can be compared after composing with the same closed immersion into GL_(2n+2).

theorem TauCeti.SpStd.baseChangeSymplecticIso_hom_comp_inclusion_assoc (n : ℕ) (k : Type) [Field k] {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))} (h : GeneralLinear.groupScheme k (n + 1 + (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeSymplecticIso n k).hom (CategoryTheory.CategoryStruct.comp (Symplectic.inclusion k (n + 1)) h) = CategoryTheory.CategoryStruct.comp (baseChangeι n k) h

The carrier--symplectic group-scheme isomorphism preserves the ambient matrix.

In particular, every transported root subgroup and torus map can be compared after composing with the same closed immersion into GL_(2n+2).

Scheme-valued points

noncomputable def TauCeti.SpStd.baseChangeSymplecticSchemePointsMulEquiv (n : ℕ) (k : Type) [Field k] (A : Type) [CommRing A] [Algebra k A] : ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧k) ⟶ (baseChangeGroupScheme n k).X) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧k) ⟶ (Symplectic.groupScheme k (n + 1)).X)

The group-scheme isomorphism identifies scheme-valued points of the base-changed integral carrier with symplectic scheme-valued points.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.SpStd.baseChangeSymplecticSchemePointsMulEquiv_apply (n : ℕ) (k : Type) [Field k] (A : Type) [CommRing A] [Algebra k A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧k) ⟶ (baseChangeGroupScheme n k).X) : (baseChangeSymplecticSchemePointsMulEquiv n k A) p = CategoryTheory.CategoryStruct.comp p (baseChangeSymplecticIso n k).hom.hom.hom

The scheme-point equivalence is postcomposition with the carrier--symplectic isomorphism.

theorem TauCeti.SpStd.baseChangeSymplecticSchemePointsMulEquiv_comp_inclusion (n : ℕ) (k : Type) [Field k] (A : Type) [CommRing A] [Algebra k A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧k) ⟶ (baseChangeGroupScheme n k).X) : CategoryTheory.CategoryStruct.comp ((baseChangeSymplecticSchemePointsMulEquiv n k A) p) (Symplectic.inclusion k (n + 1)).hom.hom = CategoryTheory.CategoryStruct.comp p (baseChangeι n k).hom.hom

On scheme-valued points, the carrier--symplectic equivalence commutes with the ambient closed immersions into GL_(2n+2).

@[simp]

theorem TauCeti.SpStd.baseChangeSymplecticSchemePointsMulEquiv_coe (n : ℕ) (k : Type) [Field k] (A : Type) [CommRing A] [Algebra k A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧k) ⟶ (baseChangeGroupScheme n k).X) : (GeneralLinear.schemePointsMulEquiv (n + 1 + (n + 1)) A) (CategoryTheory.CategoryStruct.comp p (baseChangeι n k).hom.hom) = ↑((Symplectic.schemePointsMulEquiv (n + 1) A) ((baseChangeSymplecticSchemePointsMulEquiv n k A) p))

The scheme-point equivalence preserves the underlying invertible matrix.

Algebra-valued points

noncomputable def TauCeti.SpStd.baseChangeSymplecticPointsMulEquiv (n : ℕ) (k : Type u) [Field k] (A : Type v) [CommRing A] [Algebra k A] : ↑(HopfAlgebra.points ↧A) ≃* ↑(HopfAlgebra.points ↧A)

The coordinate isomorphism identifies points of the transported type-C carrier with points of the symplectic coordinate Hopf algebra, naturally in the value algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.SpStd.baseChangeSymplecticPointsMulEquiv_apply (n : ℕ) (k : Type u) [Field k] (A : Type v) [CommRing A] [Algebra k A] (q : ↑(HopfAlgebra.points ↧A)) : (baseChangeSymplecticPointsMulEquiv n k A) q = (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (baseChangeCoordinateSymplecticIso n k).inv).app ↧A)) q

The point equivalence is precomposition with the inverse coordinate isomorphism.

theorem TauCeti.SpStd.baseChangeSymplecticPointsMulEquiv_coe (n : ℕ) (k : Type u) [Field k] (A : Type v) [CommRing A] [Algebra k A] (q : ↑(HopfAlgebra.points ↧A)) : (GeneralLinear.pointsMulEquiv (n + 1 + (n + 1))) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra k (n + 1 + (n + 1))) (baseChangeDefiningIdeal n k) ↧A)) q) = ↑((Symplectic.pointsMulEquiv k (n + 1)) ((baseChangeSymplecticPointsMulEquiv n k A) q))

The carrier--symplectic point equivalence preserves the underlying invertible matrix.