Base change of the finite dual

The finite dual of a finite projective bialgebra commutes with extension of scalars. More precisely, for a map of commutative rings k → K and a finite projective k-bialgebra H, there is a canonical K-bialgebra equivalence

K ⊗[k] ConvolutionDual k H ≃ₐc[K] ConvolutionDual K (K ⊗[k] H).

On pure tensors this sends a ⊗ φ to the functional taking b ⊗ x to a * b * algebraMap k K (φ x). This is the affine algebraic base-change square needed to transport Cartier duality for finite locally free commutative group schemes over a general base.

Main declarations

• TauCeti.ConvolutionDual.baseChangeBialgEquiv: finite dualization commutes with extension of scalars.
• TauCeti.ConvolutionDual.baseChangeBialgEquiv_tmul_apply_tmul: the equivalence's value on pure tensors.
• TauCeti.ConvolutionDual.baseChangeBialgEquiv_naturality: compatibility with finite-dual maps.

References

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

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

Finite dualization commutes with extension of scalars for finite projective bialgebras.

Equations

• TauCeti.ConvolutionDual.baseChangeBialgEquiv k K H = BialgEquiv.ofAlgEquiv TauCeti.ConvolutionDual.baseChangeAlgEquiv✝ ⋯ ⋯

@[simp]

theorem TauCeti.ConvolutionDual.baseChangeBialgEquiv_tmul_apply_tmul {k : Type u} {K : Type v} {H : Type w} [CommRing k] [CommRing K] [Algebra k K] [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] (a b : K) (φ : ConvolutionDual k H) (x : H) : ((baseChangeBialgEquiv k K H) (a ⊗ₜ[k] φ)).ofConv (b ⊗ₜ[k] x) = a * b * (algebraMap k K) (φ.ofConv x)

The base-change equivalence evaluates pure tensors by scalar-extended evaluation.

theorem TauCeti.ConvolutionDual.baseChangeBialgEquiv_naturality {k : Type u} {K : Type v} {H : Type w} [CommRing k] [CommRing K] [Algebra k K] [Semiring H] [Bialgebra k H] [Module.Finite k H] [Module.Projective k H] {H' : Type x} [Semiring H'] [Bialgebra k H'] [Module.Finite k H'] [Module.Projective k H'] (f : H →ₐc[k] H') : (map K (Bialgebra.TensorProduct.map (BialgHom.id K K) f)).comp ↑(baseChangeBialgEquiv k K H') = (↑(baseChangeBialgEquiv k K H)).comp (Bialgebra.TensorProduct.map (BialgHom.id K K) (map k f))

The finite-dual base-change equivalence is natural in finite projective bialgebras.