The finite dual of a Hopf algebra

For a finite projective bialgebra H over a commutative ring k, the linear dual carries the transposed bialgebra structure. Its multiplication is convolution, while its comultiplication and counit are characterized by

Delta(phi)(x tensor y) = phi (x * y),        epsilon(phi) = phi(1).

If H is a Hopf algebra, precomposition with its antipode is the antipode of the dual. This is the algebraic construction underlying Cartier duality for finite locally free commutative group schemes. The present file builds the finite locally free Hopf dual over a general affine base; the scheme-level duality remains a separate step.

Main declarations

• TauCeti.ConvolutionDual: the convolution algebra on the linear dual.
• TauCeti.ConvolutionDual.instBialgebra: the bialgebra obtained by transposing multiplication and unit.
• TauCeti.ConvolutionDual.instHopfAlgebra: the Hopf structure obtained by transposing the antipode.

References

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

@[reducible, inline]

abbrev TauCeti.ConvolutionDual (k : Type u) (H : Type v) [CommSemiring k] [AddCommMonoid H] [Module k H] : Type (max u v)

The linear dual, wrapped to select convolution multiplication when a coalgebra structure is available.

The WithConv wrapper selects Mathlib's convolution multiplication on linear maps.

Equations

• TauCeti.ConvolutionDual k H = WithConv (Module.Dual k H)

instance TauCeti.ConvolutionDual.instFinite (k : Type u) (H : Type v) [CommSemiring k] [AddCommMonoid H] [Module k H] [Module.Finite k H] [Module.Projective k H] : Module.Finite k (ConvolutionDual k H)

The convolution dual of a finite projective module is finite.

instance TauCeti.ConvolutionDual.instProjective (k : Type u) (H : Type v) [CommSemiring k] [AddCommMonoid H] [Module k H] [Module.Finite k H] [Module.Projective k H] : Module.Projective k (ConvolutionDual k H)

The convolution dual of a finite projective module is projective.

noncomputable def TauCeti.ConvolutionDual.dualDistribEquiv (k : Type u) (H : Type v) [CommRing k] [AddCommMonoid H] [Module k H] [Module.Finite k H] [Module.Projective k H] : TensorProduct k (ConvolutionDual k H) (ConvolutionDual k H) ≃ₗ[k] Module.Dual k (TensorProduct k H H)

A tensor of finite-dual functionals is equivalently a functional on the tensor square.

Equations

• TauCeti.ConvolutionDual.dualDistribEquiv k H = (TauCeti.ConvolutionDual.tensorUnwrap✝ k H).trans (TauCeti.ConvolutionDual.projectiveDualDistribEquiv✝ k H H)

@[instance_reducible]

noncomputable instance TauCeti.ConvolutionDual.instCoalgebraStruct (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] : CoalgebraStruct k (ConvolutionDual k H)

The comultiplication and counit on the finite dual, obtained by transposing multiplication and unit on the original algebra.

Equations

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

@[simp]

theorem TauCeti.ConvolutionDual.dualDistribEquiv_tmul_apply (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] (phi psi : ConvolutionDual k H) (x y : H) : ((dualDistribEquiv k H) (phi ⊗ₜ[k] psi)) (x ⊗ₜ[k] y) = phi.ofConv x * psi.ofConv y

A pure tensor of finite-dual functionals evaluates componentwise.

@[instance_reducible]

noncomputable instance TauCeti.ConvolutionDual.instCoalgebra (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] : Coalgebra k (ConvolutionDual k H)

The coalgebra structure on the finite dual, obtained by transposing multiplication and unit on the original bialgebra.

Equations

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

@[simp]

theorem TauCeti.ConvolutionDual.dualDistribEquiv_comul (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] (phi : ConvolutionDual k H) : (dualDistribEquiv k H) (CoalgebraStruct.comul phi) = phi.ofConv ∘ₗ LinearMap.mul' k H

Evaluating the finite-dual comultiplication gives the transpose of multiplication on H.

theorem TauCeti.ConvolutionDual.dualDistribEquiv_comul_apply (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] (phi : ConvolutionDual k H) (x y : H) : ((dualDistribEquiv k H) (CoalgebraStruct.comul phi)) (x ⊗ₜ[k] y) = phi.ofConv (x * y)

Pointwise form of the characteristic equation for the finite-dual comultiplication.

@[simp]

theorem TauCeti.ConvolutionDual.counit_apply (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] (phi : ConvolutionDual k H) : CoalgebraStruct.counit phi = phi.ofConv 1

The finite-dual counit is evaluation at one.

@[instance_reducible]

noncomputable instance TauCeti.ConvolutionDual.instBialgebra (k : Type u) (H : Type v) [CommRing k] [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] : Bialgebra k (ConvolutionDual k H)

The bialgebra structure on the finite dual. Multiplication is convolution and the coalgebra operations are transposes of multiplication and unit on the original bialgebra.

Equations

• TauCeti.ConvolutionDual.instBialgebra k H = Bialgebra.mk' k (TauCeti.ConvolutionDual k H) ⋯ ⋯ ⋯ ⋯

instance TauCeti.ConvolutionDual.instIsCocomm (k : Type u) (H : Type v) [CommRing k] [CommSemiring H] [Algebra k H] [Module.Finite k H] [Module.Projective k H] : Coalgebra.IsCocomm k (ConvolutionDual k H)

The coalgebra underlying the finite dual is cocommutative.

@[instance_reducible]

noncomputable instance TauCeti.ConvolutionDual.instHopfAlgebraStruct (k : Type u) (H : Type v) [CommRing k] [Semiring H] [HopfAlgebra k H] [Module.Finite k H] [Module.Projective k H] : HopfAlgebraStruct k (ConvolutionDual k H)

The antipode operation on the finite dual, obtained by transposing the antipode of the original Hopf algebra.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.ConvolutionDual.instHopfAlgebra (k : Type u) (H : Type v) [CommRing k] [Semiring H] [HopfAlgebra k H] [Module.Finite k H] [Module.Projective k H] : HopfAlgebra k (ConvolutionDual k H)

The Hopf algebra structure on the finite dual. Its antipode is precomposition with the antipode of the original finite projective Hopf algebra.

Equations

• TauCeti.ConvolutionDual.instHopfAlgebra k H = HopfAlgebra.ofConvInverse (HopfAlgebraStruct.antipode k) ⋯ ⋯

@[simp]

theorem TauCeti.ConvolutionDual.antipode_apply (k : Type u) (H : Type v) [CommRing k] [Semiring H] [HopfAlgebra k H] [Module.Finite k H] [Module.Projective k H] (phi : ConvolutionDual k H) (x : H) : ((HopfAlgebraStruct.antipode k) phi).ofConv x = phi.ofConv ((HopfAlgebraStruct.antipode k) x)

The finite-dual antipode acts by precomposition with the original antipode.