Cartier duality commutes with base change

Pullback along Spec S ⟶ Spec R preserves finite local freeness and commutativity, so it acts on the category where Cartier duality lives, and it commutes with Cartier duality: the Cartier dual of a base-changed group scheme is the base change of the Cartier dual.

Everything is transported from the coordinate Hopf algebras, where the corresponding statement is TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso, itself a repackaging of TauCeti.ConvolutionDual.baseChangeBialgEquiv.

Main declarations

• TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty_baseChange: pullback preserves finite local freeness and commutativity.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.baseChangeFunctor: pullback of finite locally free commutative affine group schemes along Spec S ⟶ Spec R.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.hopfSpecBaseChangeNatIso: base change of a Hopf spectrum is the Hopf spectrum of the scalar-extended coordinate Hopf algebra.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraBaseChangeNatIso: the coordinate Hopf algebra of a base change is the scalar extension of the coordinate Hopf algebra.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualBaseChangeNatIso and its objectwise form cartierDualBaseChangeIso: Cartier duality commutes with base change, identified with the Hopf-level baseChangeDualIso by cartierDualBaseChangeIso_hom.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.
• J. S. Milne, Algebraic Groups (2017), Section 12.e.

This advances Layer 4, "Cartier duality", of the ReductiveGroups roadmap.

theorem TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty_baseChange (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : finiteLocallyFreeCommAffineGroupSchemeProperty (↧S) ((AffineGroupSchemeCat.baseChangeFunctor (CommRingCat.ofHom (algebraMap R S))).obj ((finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι.obj G))

Pullback along Spec S ⟶ Spec R preserves finite local freeness and commutativity, so it restricts to the category where Cartier duality lives. No hypothesis beyond commutativity of the two rings is needed: finiteness, flatness and local finite presentation are all stable under base change.

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.baseChangeFunctor (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Functor (FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) (FiniteLocallyFreeCommAffineGroupSchemeCat ↧S)

Pullback of finite locally free commutative affine group schemes along Spec S ⟶ Spec R.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.baseChangeFunctorCompιIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : (baseChangeFunctor R S).comp (finiteLocallyFreeCommAffineGroupSchemeProperty ↧S).ι ≅ (finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι.comp (AffineGroupSchemeCat.baseChangeFunctor (CommRingCat.ofHom (algebraMap R S)))

Forgetting finite local freeness and commutativity turns the restricted base change into scheme-theoretic pullback.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.hopfSpecBaseChangeNatIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.comp (baseChangeFunctor R S) ≅ (FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctor R S).op.comp (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat S).functor

Base change of a Hopf spectrum is the Hopf spectrum of the scalar-extended coordinate Hopf algebra, restricted to finite locally free commutative objects.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraBaseChangeNatIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : (baseChangeFunctor R S).op.comp (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat S).rightOp.inverse ≅ (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).rightOp.inverse.comp (FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctor R S)

The coordinate Hopf algebra of a base-changed group scheme is the scalar extension of its coordinate Hopf algebra, naturally in the group scheme.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualBaseChangeNatIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : (baseChangeFunctor R S).op.comp (cartierDualFunctor S) ≅ (cartierDualFunctor R).comp (baseChangeFunctor R S)

Cartier duality commutes with base change, naturally in the group scheme.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraBaseChangeIso {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : coordinateHopfAlgebra S ((baseChangeFunctor R S).obj G) ≅ FiniteLocallyFreeBicommutativeHopfAlgCat.baseChange S (coordinateHopfAlgebra R G)

The coordinate Hopf algebra of a base-changed group scheme is the scalar extension of its coordinate Hopf algebra.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualBaseChangeIso {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : cartierDual S ((baseChangeFunctor R S).obj G) ≅ (baseChangeFunctor R S).obj (cartierDual R G)

Cartier duality commutes with base change: the Cartier dual of a base-changed finite locally free commutative affine group scheme is the base change of its Cartier dual.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualBaseChangeIso S G = (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualBaseChangeNatIso R S).app (Opposite.op G)

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualBaseChangeIso_hom {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : (cartierDualBaseChangeIso S G).hom = CategoryTheory.CategoryStruct.comp ((finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat S).functor.map (FiniteLocallyFreeBicommutativeHopfAlgCat.dualMap (coordinateHopfAlgebraBaseChangeIso S G).hom).op) (CategoryTheory.CategoryStruct.comp ((finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat S).functor.map (FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso S (coordinateHopfAlgebra R G)).hom.op) ((hopfSpecBaseChangeNatIso R S).app (Opposite.op (coordinateHopfAlgebra R G).dual)).inv)

cartierDualBaseChangeIso is the Hopf-level comparison baseChangeDualIso transported by Spec. Reading the Cartier dual through its coordinate Hopf algebra, the comparison is finite dualization of coordinateHopfAlgebraBaseChangeIso followed by baseChangeDualIso, and then the Hopf-spectrum base-change comparison. This is the identification that lets coherences be proved without unfolding the whiskered definition.