Cartier duality for finite locally free Hopf algebras

A commutative finite locally free group scheme over an affine base is represented by a finite projective Hopf algebra whose multiplication and comultiplication are both commutative. The linear dual preserves this bicommutative condition, reverses morphisms, and is involutive by evaluation.

This file packages those facts as a contravariant equivalence on finite locally free bicommutative Hopf algebras. The equivalence is built from double-dual evaluation by CategoryTheory.Functor.dualityEquivalence, so its inverse is again finite dualization and its unit and counit are inverse double-dual evaluation; nothing about it is abstract. It is the algebraic core of Cartier duality over a general affine base; its transport through Spec is provided by AlgebraicGeometry.AffineGroupScheme.CartierDuality.FiniteLocallyFree.

Main declarations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat: finite locally free commutative, cocommutative Hopf algebras over a commutative ring.
• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor: contravariant finite dualization.
• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso: the objectwise double-dual evaluation isomorphism, natural in morphisms by evalIso_hom_naturality and bundled as evalNatIso.
• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualMap_evalIso_inv: the triangle identity exhibiting finite dualization as involutive.
• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.cartierDuality: the resulting anti-equivalence, with cartierDuality_functor and cartierDuality_inverse computing its two directions. Its unit and counit are computed by the generic CategoryTheory.Functor.dualityEquivalence_unitIso_hom_app and its three companions; the specializations to evalIso hold by rfl.

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.

def TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty (k : Type u) [CommRing k] : CategoryTheory.ObjectProperty (CommHopfAlgCat k)

The object property selecting finite locally free bicommutative Hopf algebras.

The ambient CommHopfAlgCat supplies commutativity of multiplication; the final conjunct is cocommutativity of comultiplication. Finite locally free modules are expressed as finite projective modules.

Equations

• TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty k H = (Module.Finite k ↑H ∧ Module.Projective k ↑H ∧ Coalgebra.IsCocomm k ↑H)

@[simp]

theorem TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty_iff (k : Type u) [CommRing k] (H : CommHopfAlgCat k) : finiteLocallyFreeBicommutativeHopfAlgProperty k H ↔ Module.Finite k ↑H ∧ Module.Projective k ↑H ∧ Coalgebra.IsCocomm k ↑H

Membership in finiteLocallyFreeBicommutativeHopfAlgProperty is finite projectivity together with cocommutativity.

@[reducible, inline]

abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat (k : Type u) [CommRing k] : Type (u + 1)

The category of finite locally free bicommutative Hopf algebras over a commutative ring.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat k = (TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty k).FullSubcategory

@[instance_reducible]

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.instCoeSortType {k : Type u} [CommRing k] : CoeSort (FiniteLocallyFreeBicommutativeHopfAlgCat k) (Type u)

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.instCoeSortType = { coe := fun (H : TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat k) => ↑H.obj }

@[instance_reducible]

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.commRing {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : CommRing ↑H.obj

Equations

• H.commRing = CommHopfAlgCat.instCommRingObjForgetBialgHomX

@[instance_reducible]

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.hopfAlgebra {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : HopfAlgebra k ↑H.obj

Equations

• H.hopfAlgebra = CommHopfAlgCat.instHopfAlgebraObjForgetBialgHomX

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.finite {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : Module.Finite k ↑H.obj

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.projective {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : Module.Projective k ↑H.obj

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.isCocomm {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : Coalgebra.IsCocomm k ↑H.obj

@[reducible, inline]

abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.of (k : Type u) [CommRing k] (H : Type u) [CommRing H] [HopfAlgebra k H] [Module.Finite k H] [Module.Projective k H] [Coalgebra.IsCocomm k H] : FiniteLocallyFreeBicommutativeHopfAlgCat k

Bundle a finite locally free bicommutative Hopf algebra as an object of FiniteLocallyFreeBicommutativeHopfAlgCat.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.of k H = { obj := ↧H, property := ⋯ }

@[reducible, inline]

abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.toBialgHom {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} (f : H ⟶ K) : ↑H.obj →ₐc[k] ↑K.obj

The bialgebra morphism underlying a morphism of finite locally free bicommutative Hopf algebras.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.toBialgHom f = CommHopfAlgCat.Hom.hom f.hom

@[reducible, inline]

abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.ofHom {k : Type u} [CommRing k] {H K : Type u} [CommRing H] [CommRing K] [HopfAlgebra k H] [HopfAlgebra k K] [Module.Finite k H] [Module.Finite k K] [Module.Projective k H] [Module.Projective k K] [Coalgebra.IsCocomm k H] [Coalgebra.IsCocomm k K] (f : H →ₐc[k] K) : of k H ⟶ of k K

Bundle a bialgebra morphism between finite locally free bicommutative Hopf algebras.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.ofHom f = CategoryTheory.ObjectProperty.homMk (CommHopfAlgCat.ofHom f)

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.hom_ext {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} {f g : H ⟶ K} (h : toBialgHom f = toBialgHom g) : f = g

Morphisms of finite locally free bicommutative Hopf algebras are determined by their underlying bialgebra morphisms.

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.hom_ext_iff {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} {f g : H ⟶ K} : f = g ↔ toBialgHom f = toBialgHom g

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.toBialgHom_id {k : Type u} [CommRing k] {H : FiniteLocallyFreeBicommutativeHopfAlgCat k} : toBialgHom (CategoryTheory.CategoryStruct.id H) = BialgHom.id k ↑H.obj

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.toBialgHom_comp {k : Type u} [CommRing k] {H K L : FiniteLocallyFreeBicommutativeHopfAlgCat k} (f : H ⟶ K) (g : K ⟶ L) : toBialgHom (CategoryTheory.CategoryStruct.comp f g) = (toBialgHom g).comp (toBialgHom f)

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dual {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : FiniteLocallyFreeBicommutativeHopfAlgCat k

The finite dual of a finite locally free bicommutative Hopf algebra.

Equations

• H.dual = TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.of k (TauCeti.ConvolutionDual k ↑H.obj)

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualMap {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} (f : H ⟶ K) : K.dual ⟶ H.dual

A morphism of finite locally free bicommutative Hopf algebras induces a morphism of finite duals in the opposite direction.

Equations

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

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.toBialgHom_dualMap {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} (f : H ⟶ K) : toBialgHom (dualMap f) = ConvolutionDual.map k (toBialgHom f)

The bialgebra morphism underlying dualMap is the transposed morphism.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor {k : Type u} [CommRing k] : CategoryTheory.Functor (FiniteLocallyFreeBicommutativeHopfAlgCat k)ᵒᵖ (FiniteLocallyFreeBicommutativeHopfAlgCat k)

Finite dualization as a contravariant endofunctor on finite locally free bicommutative Hopf algebras.

The body is exposed so that dualFunctor.rightOp ⋙ dualFunctor reduces to double dualization, without which evalNatIso does not typecheck.

Equations

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

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor_obj {k : Type u} [CommRing k] (H : (FiniteLocallyFreeBicommutativeHopfAlgCat k)ᵒᵖ) : dualFunctor.obj H = (Opposite.unop H).dual

The object part of dualFunctor is the finite convolution dual.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctor_map {k : Type u} [CommRing k] {H K : (FiniteLocallyFreeBicommutativeHopfAlgCat k)ᵒᵖ} (f : H ⟶ K) : dualFunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (dualMap f.unop) (CategoryTheory.eqToHom ⋯))

The morphism part of dualFunctor is precomposition on the finite dual.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : H ≅ H.dual.dual

Evaluation identifies a finite locally free bicommutative Hopf algebra with its double finite dual.

Equations

• H.evalIso = (TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty k).isoMk (CommHopfAlgCat.isoMk (TauCeti.ConvolutionDual.evalBialgEquiv k ↑H.obj))

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso_hom_apply_apply {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) (x : ↑H.obj) (phi : ConvolutionDual k ↑H.obj) : ((CategoryTheory.ConcreteCategory.hom H.evalIso.hom) x).ofConv phi = phi.ofConv x

The forward map of evalIso evaluates finite-dual functionals.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso_inv_apply_apply {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) (Phi : ConvolutionDual k (ConvolutionDual k ↑H.obj)) (phi : ConvolutionDual k ↑H.obj) : phi.ofConv ((CategoryTheory.ConcreteCategory.hom H.evalIso.inv) Phi) = Phi.ofConv phi

The inverse map of evalIso is characterized by evaluation.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso_hom_naturality {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp f K.evalIso.hom = CategoryTheory.CategoryStruct.comp H.evalIso.hom (dualMap (dualMap f))

Double-dual evaluation is natural in finite locally free bicommutative Hopf algebras.

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso_hom_naturality_assoc {k : Type u} [CommRing k] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat k} (f : H ⟶ K) {Z : FiniteLocallyFreeBicommutativeHopfAlgCat k} (h : K.dual.dual ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp K.evalIso.hom h) = CategoryTheory.CategoryStruct.comp H.evalIso.hom (CategoryTheory.CategoryStruct.comp (dualMap (dualMap f)) h)

Double-dual evaluation is natural in finite locally free bicommutative Hopf algebras.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalNatIso {k : Type u} [CommRing k] : CategoryTheory.Functor.id (FiniteLocallyFreeBicommutativeHopfAlgCat k) ≅ dualFunctor.rightOp.comp dualFunctor

Double-dual evaluation as a natural isomorphism from the identity functor to double finite dualization.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalNatIso = CategoryTheory.NatIso.ofComponents TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalIso ⋯

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalNatIso_hom_app {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : evalNatIso.hom.app H = H.evalIso.hom

The components of evalNatIso are the objectwise evaluation isomorphisms.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.evalNatIso_inv_app {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : evalNatIso.inv.app H = H.evalIso.inv

The inverse components of evalNatIso are the objectwise inverse evaluation isomorphisms.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualMap_evalIso_inv {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : dualMap H.evalIso.inv = H.dual.evalIso.hom

Dualizing the inverse evaluation isomorphism of H is the evaluation isomorphism of the finite dual of H. This is the triangle identity that makes finite dualization involutive.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualMap_evalIso_hom {k : Type u} [CommRing k] (H : FiniteLocallyFreeBicommutativeHopfAlgCat k) : dualMap H.evalIso.hom = H.dual.evalIso.inv

Dualizing the evaluation isomorphism of H is the inverse evaluation isomorphism of the finite dual of H.

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.isInvolutiveDual_dualFunctor {k : Type u} [CommRing k] : dualFunctor.IsInvolutiveDual evalNatIso

Finite dualization is involutive in the sense required to build an anti-equivalence out of it.

IsInvolutiveDual spells the triangle identity with dualFunctor and evalNatIso; those are the functor and natural isomorphism assembled from dualMap and evalIso, so the two forms of the identity are the same statement and dualMap_evalIso_inv_comp applies directly.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.cartierDuality {k : Type u} [CommRing k] : (FiniteLocallyFreeBicommutativeHopfAlgCat k)ᵒᵖ ≌ FiniteLocallyFreeBicommutativeHopfAlgCat k

Finite locally free Cartier duality. Finite dualization is an anti-equivalence of the category of finite locally free bicommutative Hopf algebras over a commutative ring. Its inverse is finite dualization again, and its unit and counit are inverse double-dual evaluation.

The body is exposed so that cartierDuality_functor and cartierDuality_inverse, and their counterparts for the transported group-scheme duality, hold definitionally.

Equations

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

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.cartierDuality_functor {k : Type u} [CommRing k] : cartierDuality.functor = dualFunctor

The forward functor of cartierDuality is finite dualization.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.cartierDuality_inverse {k : Type u} [CommRing k] : cartierDuality.inverse = dualFunctor.rightOp

The inverse functor of cartierDuality is finite dualization again.

instance TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.dualFunctorIsEquivalence {k : Type u} [CommRing k] : dualFunctor.IsEquivalence