Cartier duality over an affine base

This file transports finite locally free Cartier duality from coordinate Hopf algebras to commutative affine group schemes over an arbitrary commutative ring. A morphism to an affine base is finite locally free when it is finite, flat, and locally of finite presentation. For a Hopf spectrum these three conditions say exactly that its coordinate algebra is finite projective over the base. Commutativity of the group object is, as before, cocommutativity of the coordinate Hopf algebra.

The resulting anti-equivalence is Cartier duality over an arbitrary affine base. Its objects explicitly include flatness and finite presentation; these hypotheses cannot be omitted over a general ring. Because the Hopf-algebra equivalence being transported already knows its own inverse, so does this one: the inverse is Cartier dualization again, and the counit is the inverse of the double-dual isomorphism cartierDualDualIso.

Main declarations

• TauCeti.moduleProjective_iff_flat_and_locallyOfFinitePresentation_hopfSpec: finite projectivity of a coordinate algebra is the flat, finitely presented condition on its Hopf spectrum.
• TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty: the object property selecting finite locally free commutative affine group schemes over an affine base.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat: the category selected by that property.
• finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat: the restricted anti-equivalence over a commutative ring. Its functorCompFullSubcategoryιIso, functorCompιIso, inverseCompιIso, and rightOpInverseCompιIso describe the two functors after forgetting the property proofs.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality: Cartier duality over an arbitrary affine base, with cartierDuality_functor and cartierDuality_inverse computing both of its directions as transported finite dualization.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDual and TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebra: the Cartier dual of a group scheme and its coordinate Hopf algebra, related by cartierDual_eq and coordinateHopfAlgebraCartierDualIso.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.hopfSpecCoordinateHopfAlgebraIso: the comparison with the Hopf spectrum of the coordinate algebra in the ambient affine category.
• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualIso: the double-dual isomorphism G ≅ D(D(G)), natural by cartierDualDualIso_hom_naturality.

References

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

This completes the affine-base case of the Cartier-duality target in Layer 4 of the ReductiveGroups roadmap.

def TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty (S : CommRingCat) : CategoryTheory.ObjectProperty (AffineGroupSchemeCat S)

The object property selecting finite locally free commutative affine group schemes over an affine base. Finite local freeness is expressed by the standard scheme-theoretic conjunction of finiteness, flatness, and local finite presentation.

Equations

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

@[simp]

theorem TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty_iff (S : CommRingCat) (G : AffineGroupSchemeCat S) : finiteLocallyFreeCommAffineGroupSchemeProperty S G ↔ AlgebraicGeometry.IsFinite G.obj.X.hom ∧ AlgebraicGeometry.Flat G.obj.X.hom ∧ AlgebraicGeometry.LocallyOfFinitePresentation G.obj.X.hom ∧ CategoryTheory.IsCommMonObj G.obj.X

Membership in the finite-locally-free commutative affine-group-scheme property.

instance TauCeti.instIsClosedUnderIsomorphismsAffineGroupSchemeCatFiniteLocallyFreeCommAffineGroupSchemeProperty (S : CommRingCat) : (finiteLocallyFreeCommAffineGroupSchemeProperty S).IsClosedUnderIsomorphisms

theorem TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty_inverseImage (R : Type u) [CommRing R] : (finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor = (finiteLocallyFreeBicommutativeHopfAlgProperty R).op

Under the affine Hopf/group-scheme anti-equivalence over a commutative ring, finite projectivity and cocommutativity of the coordinate Hopf algebra correspond to finite local freeness and commutativity of the affine group scheme.

@[reducible, inline]

abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat (S : CommRingCat) : Type (u + 1)

The category of finite locally free commutative affine group schemes over an affine base.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat S = (TauCeti.finiteLocallyFreeCommAffineGroupSchemeProperty S).FullSubcategory

instance TauCeti.instIsFiniteHomSchemeXOverSpecObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteLocallyFreeCommAffineGroupSchemeProperty {S : CommRingCat} (G : FiniteLocallyFreeCommAffineGroupSchemeCat S) : AlgebraicGeometry.IsFinite G.obj.obj.X.hom

instance TauCeti.instFlatHomSchemeXOverSpecObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteLocallyFreeCommAffineGroupSchemeProperty {S : CommRingCat} (G : FiniteLocallyFreeCommAffineGroupSchemeCat S) : AlgebraicGeometry.Flat G.obj.obj.X.hom

instance TauCeti.instLocallyOfFinitePresentationHomSchemeXOverSpecObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteLocallyFreeCommAffineGroupSchemeProperty {S : CommRingCat} (G : FiniteLocallyFreeCommAffineGroupSchemeCat S) : AlgebraicGeometry.LocallyOfFinitePresentation G.obj.obj.X.hom

instance TauCeti.instIsCommMonObjOverSchemeSpecXObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteLocallyFreeCommAffineGroupSchemeProperty {S : CommRingCat} (G : FiniteLocallyFreeCommAffineGroupSchemeCat S) : CategoryTheory.IsCommMonObj G.obj.obj.X

noncomputable def TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat (R : Type u) [CommRing R] : (FiniteLocallyFreeBicommutativeHopfAlgCat R)ᵒᵖ ≌ FiniteLocallyFreeCommAffineGroupSchemeCat ↧R

Spec as an anti-equivalence from finite locally free bicommutative Hopf algebras to finite locally free commutative affine group schemes over an arbitrary commutative ring.

Equations

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

noncomputable def TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat.functorCompFullSubcategoryιIso (R : Type u) [CommRing R] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.comp (finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι ≅ (CategoryTheory.forget₂ (FiniteLocallyFreeBicommutativeHopfAlgCat R) (CommHopfAlgCat R)).op.comp (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor

The restricted equivalence followed by the finite-locally-free inclusion is the unrestricted equivalence applied after forgetting the property proofs. This isomorphism isolates the implementation of the object-property restrictions, so that downstream files never have to unfold them.

Equations

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

noncomputable def TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat.functorCompιIso (R : Type u) [CommRing R] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.comp ((finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι.comp (affineGroupSchemeProperty ↧R).ι) ≅ (CategoryTheory.forget₂ (FiniteLocallyFreeBicommutativeHopfAlgCat R) (CommHopfAlgCat R)).op.comp (AlgebraicGeometry.hopfSpec ↧R)

The restricted anti-equivalence followed by the inclusions into affine group schemes and all group schemes is Mathlib's hopfSpec after forgetting the finiteness, projectivity, and cocommutativity proofs.

Equations

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

noncomputable def TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat.functorObjIso (R : Type u) [CommRing R] (H : (FiniteLocallyFreeBicommutativeHopfAlgCat R)ᵒᵖ) : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.obj H ≅ { obj := { obj := (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (Opposite.unop H).obj), property := ⋯ }, property := ⋯ }

The object produced by the finite-locally-free Hopf/group-scheme anti-equivalence is its bundled Hopf spectrum.

Equations

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

theorem TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat.functorObjIso_hom_hom_hom (R : Type u) [CommRing R] (H : (FiniteLocallyFreeBicommutativeHopfAlgCat R)ᵒᵖ) : (functorObjIso R H).hom.hom.hom = (functorCompιIso R).hom.app H

After forgetting the property proofs, the object comparison is the Hopf--spectrum functor comparison.

noncomputable def TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat.inverseCompιIso (R : Type u) [CommRing R] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).inverse.comp (CategoryTheory.forget₂ (FiniteLocallyFreeBicommutativeHopfAlgCat R) (CommHopfAlgCat R)).op ≅ (finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι.comp (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).inverse

The inverse restricted anti-equivalence computes as the unrestricted coordinate-Hopf-algebra functor after forgetting finite local freeness and commutativity.

Equations

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

noncomputable def TauCeti.finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat.rightOpInverseCompιIso (R : Type u) [CommRing R] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).rightOp.inverse.comp (CategoryTheory.forget₂ (FiniteLocallyFreeBicommutativeHopfAlgCat R) (CommHopfAlgCat R)) ≅ ((finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι.comp (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).inverse).leftOp

The rightOp inverse used in scheme-level Cartier duality computes, after forgetting module-finiteness and cocommutativity, as the opposite of the unrestricted coordinate Hopf-algebra functor.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality (R : Type u) [CommRing R] : (FiniteLocallyFreeCommAffineGroupSchemeCat ↧R)ᵒᵖ ≌ FiniteLocallyFreeCommAffineGroupSchemeCat ↧R

Cartier duality for finite locally free commutative affine group schemes over an arbitrary commutative base ring.

Transporting FiniteLocallyFreeBicommutativeHopfAlgCat.cartierDuality rather than the bare dualization functor keeps the inverse computable: it is again Cartier dualization, and the counit is the inverse of the double-dual evaluation isomorphism cartierDualDualIso.

The body is exposed so that cartierDuality_inverse holds definitionally, without which cartierDualDualNatIso does not typecheck.

Equations

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

@[simp]

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality_functor (R : Type u) [CommRing R] : (cartierDuality R).functor = (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).rightOp.inverse.comp (FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor.rightOp.comp (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor)

The forward functor of Cartier duality over an arbitrary affine base is finite dualization transported through the finite-locally-free Hopf--spectrum anti-equivalence.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (FiniteLocallyFreeCommAffineGroupSchemeCat ↧R)ᵒᵖ (FiniteLocallyFreeCommAffineGroupSchemeCat ↧R)

Cartier dualization as a contravariant endofunctor on finite locally free commutative affine group schemes.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualFunctor R = (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality R).functor

@[simp]

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality_inverse (R : Type u) [CommRing R] : (cartierDuality R).inverse = (cartierDualFunctor R).rightOp

The inverse of Cartier duality is Cartier dualization again. This is the identification that CategoryTheory.Functor.asEquivalence cannot provide.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebra (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : FiniteLocallyFreeBicommutativeHopfAlgCat R

The coordinate Hopf algebra of a finite locally free commutative affine group scheme.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.hopfSpecCoordinateHopfAlgebraIso (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧R).functor.obj (Opposite.op (coordinateHopfAlgebra R G).obj) ≅ (finiteLocallyFreeCommAffineGroupSchemeProperty ↧R).ι.obj G

The Hopf spectrum of the coordinate Hopf algebra recovers the original affine group scheme, after forgetting finite local freeness and commutativity.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDual (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R

The Cartier dual of a finite locally free commutative affine group scheme.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDual R G = (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualFunctor R).obj (Opposite.op G)

@[simp]

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDual_eq (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : cartierDual R G = (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.obj (Opposite.op (coordinateHopfAlgebra R G).dual)

The Cartier dual is represented by the finite dual of the coordinate Hopf algebra.

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualHopfSpecIso (R : Type u) [CommRing R] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : cartierDual R ((finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.obj (Opposite.op H)) ≅ (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.obj (Opposite.op H.dual)

Cartier dualization of a Hopf spectrum is the Hopf spectrum of the finite dual.

Equations

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

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualHopfSpecIso_hom (R : Type u) [CommRing R] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : let E := finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R; (cartierDualHopfSpecIso R H).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (E.functor.map (FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor.mapIso (E.unitIso.app (Opposite.op H)).unop.op).op.hom)

On morphisms, the Hopf--spectrum duality comparison is induced by the equivalence unit and finite dualization.

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraCartierDualNatIso (R : Type u) [CommRing R] : (cartierDualFunctor R).rightOp.comp (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).rightOp.inverse ≅ (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).rightOp.inverse.rightOp.comp FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor

The coordinate Hopf algebra of a Cartier dual is the finite dual of the coordinate Hopf algebra, naturally in the group scheme.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraCartierDualIso (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : coordinateHopfAlgebra R (cartierDual R G) ≅ (coordinateHopfAlgebra R G).dual

The coordinate Hopf algebra of the Cartier dual of a single group scheme.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraCartierDualIso R G = (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.coordinateHopfAlgebraCartierDualNatIso R).app G

noncomputable def TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualNatIso (R : Type u) [CommRing R] : CategoryTheory.Functor.id (FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) ≅ (cartierDualFunctor R).rightOp.comp (cartierDualFunctor R)

Cartier duality is involutive. Every finite locally free commutative affine group scheme is naturally isomorphic to its Cartier double dual.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualNatIso R = (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality R).counitIso.symm

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualIso (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : G ≅ cartierDual R (cartierDual R G)

The double-dual isomorphism of a single finite locally free commutative affine group scheme.

Equations

• TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualIso R G = (TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualNatIso R).app G

@[simp]

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualNatIso_hom_app (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : (cartierDualDualNatIso R).hom.app G = (cartierDuality R).counitIso.inv.app G

The double-dual isomorphism is the inverse counit of cartierDuality.

@[simp]

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualNatIso_inv_app (R : Type u) [CommRing R] (G : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R) : (cartierDualDualNatIso R).inv.app G = (cartierDuality R).counitIso.hom.app G

The inverse double-dual isomorphism is the counit of cartierDuality.

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualIso_hom_naturality (R : Type u) [CommRing R] {G H : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp f (cartierDualDualIso R H).hom = CategoryTheory.CategoryStruct.comp (cartierDualDualIso R G).hom ((cartierDualFunctor R).map ((cartierDualFunctor R).map f.op).op)

The double-dual isomorphism is natural in the group scheme.

theorem TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualDualIso_hom_naturality_assoc (R : Type u) [CommRing R] {G H : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R} (f : G ⟶ H) {Z : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R} (h : cartierDual R (cartierDual R H) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (cartierDualDualIso R H).hom h) = CategoryTheory.CategoryStruct.comp (cartierDualDualIso R G).hom (CategoryTheory.CategoryStruct.comp ((cartierDualFunctor R).map ((cartierDualFunctor R).map f.op).op) h)

The double-dual isomorphism is natural in the group scheme.