Functoriality and reflexivity of the finite Hopf dual

Dualizing a bialgebra morphism between finite projective bialgebras gives a morphism in the opposite direction between their convolution duals. Evaluation identifies a finite projective bialgebra with its double convolution dual, compatibly with multiplication, comultiplication, unit, and counit.

These are the algebraic functoriality and involutivity statements needed to promote the finite Hopf dual constructed in TauCeti.Algebra.HopfAlgebra.FiniteDual.Basic to Cartier duality. The scheme-level duality remains a separate step.

Main declarations

• TauCeti.ConvolutionDual.map: the contravariant map on finite projective bialgebras.
• TauCeti.ConvolutionDual.map_id and TauCeti.ConvolutionDual.map_comp: its functoriality laws.
• TauCeti.ConvolutionDual.mapEquiv: the contravariant equivalence induced by a bialgebra equivalence.
• TauCeti.ConvolutionDual.evalBialgEquiv: evaluation as a bialgebra equivalence with the double convolution dual.
• TauCeti.ConvolutionDual.evalBialgEquiv_naturality: naturality of evaluation.

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.

noncomputable def TauCeti.ConvolutionDual.map (k : Type u) [CommRing k] {H : Type v} {K : Type w} [Semiring H] [Bialgebra k H] [Semiring K] [Bialgebra k K] [Module.Finite k H] [Module.Projective k H] [Module.Finite k K] [Module.Projective k K] (f : H →ₐc[k] K) : ConvolutionDual k K →ₐc[k] ConvolutionDual k H

The finite dual is contravariantly functorial. A bialgebra morphism H → K induces the bialgebra morphism K* → H* given by precomposition.

Equations

• TauCeti.ConvolutionDual.map k f = BialgHom.ofAlgHom (TauCeti.ConvolutionDual.mapAlgHom✝ k f) ⋯ ⋯

@[simp]

theorem TauCeti.ConvolutionDual.map_apply_apply (k : Type u) [CommRing k] {H : Type v} {K : Type w} [Semiring H] [Bialgebra k H] [Semiring K] [Bialgebra k K] [Module.Finite k H] [Module.Projective k H] [Module.Finite k K] [Module.Projective k K] (f : H →ₐc[k] K) (phi : ConvolutionDual k K) (x : H) : ((map k f) phi).ofConv x = phi.ofConv (f x)

The dual morphism evaluates by precomposition.

@[simp]

theorem TauCeti.ConvolutionDual.map_id (k : Type u) [CommRing k] {H : Type v} [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] : map k (BialgHom.id k H) = BialgHom.id k (ConvolutionDual k H)

Dualizing the identity bialgebra morphism gives the identity.

@[simp]

theorem TauCeti.ConvolutionDual.map_comp (k : Type u) [CommRing k] {H : Type v} {K : Type w} [Semiring H] [Bialgebra k H] [Semiring K] [Bialgebra k K] [Module.Finite k H] [Module.Projective k H] [Module.Finite k K] [Module.Projective k K] {L : Type u_1} [Semiring L] [Bialgebra k L] [Module.Finite k L] [Module.Projective k L] (g : K →ₐc[k] L) (f : H →ₐc[k] K) : map k (g.comp f) = (map k f).comp (map k g)

Dualizing a composite reverses the order of the dual morphisms.

noncomputable def TauCeti.ConvolutionDual.mapEquiv (k : Type u) [CommRing k] {H : Type v} {K : Type w} [Semiring H] [Bialgebra k H] [Semiring K] [Bialgebra k K] [Module.Finite k H] [Module.Projective k H] [Module.Finite k K] [Module.Projective k K] (e : H ≃ₐc[k] K) : ConvolutionDual k K ≃ₐc[k] ConvolutionDual k H

A bialgebra equivalence induces a bialgebra equivalence of finite duals in the opposite direction.

Equations

• TauCeti.ConvolutionDual.mapEquiv k e = BialgEquiv.ofBialgHom (TauCeti.ConvolutionDual.map k ↑e) (TauCeti.ConvolutionDual.map k ↑e.symm) ⋯ ⋯

@[simp]

theorem TauCeti.ConvolutionDual.mapEquiv_apply (k : Type u) [CommRing k] {H : Type v} {K : Type w} [Semiring H] [Bialgebra k H] [Semiring K] [Bialgebra k K] [Module.Finite k H] [Module.Projective k H] [Module.Finite k K] [Module.Projective k K] (e : H ≃ₐc[k] K) (phi : ConvolutionDual k K) : (mapEquiv k e) phi = (map k ↑e) phi

The forward map of the dual equivalence is the dual morphism.

@[simp]

theorem TauCeti.ConvolutionDual.mapEquiv_symm (k : Type u) [CommRing k] {H : Type v} {K : Type w} [Semiring H] [Bialgebra k H] [Semiring K] [Bialgebra k K] [Module.Finite k H] [Module.Projective k H] [Module.Finite k K] [Module.Projective k K] (e : H ≃ₐc[k] K) : (mapEquiv k e).symm = mapEquiv k e.symm

The inverse of the dual equivalence is induced by the inverse bialgebra equivalence.

noncomputable def TauCeti.ConvolutionDual.evalBialgEquiv (k : Type u) [CommRing k] (H : Type v) [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] : H ≃ₐc[k] ConvolutionDual k (ConvolutionDual k H)

A finite projective bialgebra is canonically isomorphic to its double finite dual.

The equivalence sends x to evaluation at x.

Equations

• TauCeti.ConvolutionDual.evalBialgEquiv k H = id (have hbij := ⋯; BialgEquiv.ofBijective (TauCeti.ConvolutionDual.evalBialgHom✝ k H) hbij)

@[simp]

theorem TauCeti.ConvolutionDual.evalBialgEquiv_apply_apply (k : Type u) [CommRing k] (H : Type v) [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] (x : H) (phi : ConvolutionDual k H) : ((evalBialgEquiv k H) x).ofConv phi = phi.ofConv x

The double-dual equivalence evaluates a functional at the original element.

@[simp]

theorem TauCeti.ConvolutionDual.evalBialgEquiv_symm_apply_apply (k : Type u) [CommRing k] (H : Type v) [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] (Phi : ConvolutionDual k (ConvolutionDual k H)) (phi : ConvolutionDual k H) : phi.ofConv ((evalBialgEquiv k H).symm Phi) = Phi.ofConv phi

The inverse double-dual equivalence is characterized by evaluation.

theorem TauCeti.ConvolutionDual.evalBialgEquiv_naturality (k : Type u) [CommRing k] (H : Type v) [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] {K : Type w} [Semiring K] [Bialgebra k K] [Module.Finite k K] [Module.Projective k K] (f : H →ₐc[k] K) : (↑(evalBialgEquiv k K)).comp f = (map k (map k f)).comp ↑(evalBialgEquiv k H)

Evaluation into the double dual is natural in finite projective bialgebras.