Pointwise Tannakian reconstruction for commutative Hopf algebras

Let H be a commutative Hopf algebra over a field k, and let A be a commutative k-algebra. This file identifies the A-valued points of H with the tensor automorphisms of scalar extension on finite-dimensional H-comodules.

The identification here is for one fixed value algebra A; naturality in A, and hence the statement identifying the two functors of points, is in TauCeti.Algebra.AlgebraicGroup.Representation.Tannaka.GroupFunctor. Nothing in this file is stated in terms of affine group schemes: the reconstruction is at the level of the coordinate Hopf algebra, and passing to TauCeti.AffineGroupSchemeCat goes through the anti-equivalence in TauCeti.AlgebraicGeometry.AffineGroupScheme.Equivalence.

The remaining inverse direction in the reconstruction theorem is detected by matrix coefficients. For a finite comodule M, every coefficient map is a comodule morphism from M to a finite subcomodule of the regular comodule. Naturality compares an arbitrary tensor automorphism on these two objects. Applying the counit then reads the comparison as the global functional used to reconstruct the point, and the scalar-extended dual separates elements of A ⊗[k] M.

Main declarations

• TauCeti.Tannaka.fgPointTensorIso_reconstructedPoint: reconstruction is a right inverse to the point action.
• TauCeti.Tannaka.endOfPoint_reconstructedPoint: a reconstructed point acts through the corresponding tensor-automorphism component.
• TauCeti.Tannaka.fgPointTensorIsoEquiv: the Tannakian equivalence, for a fixed value algebra, between algebra-valued points and tensor automorphisms of finite-comodule scalar extension.

References

• J. S. Milne, Algebraic Groups (2017), §9.4.
• Mathlib/RepresentationTheory/Tannaka.lean: the final MulEquiv.ofBijective packaging follows the finite-group Tannaka theorem there.

@[simp]

theorem TauCeti.Tannaka.fgPointTensorIso_reconstructedPoint (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (eta : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) : fgPointTensorIso k H A (reconstructedPoint k H A eta) = eta

The tensor automorphism induced by a reconstructed point is the original tensor automorphism. Thus reconstruction is a right inverse to the tensor action of points.

@[simp]

theorem TauCeti.Tannaka.endOfPoint_reconstructedPoint (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (eta : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (M : FGComoduleCat k H) : Comodule.endOfPoint (↑M) (reconstructedPoint k H A eta).ofConv = scalarExtensionComponent k H A eta M

The action of a point reconstructed from a tensor automorphism is that automorphism's component on every finite-dimensional comodule.

noncomputable def TauCeti.Tannaka.fgPointTensorIsoEquiv (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] : WithConv (H →ₐ[k] A) ≃* CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)

Algebra-valued points of a commutative Hopf algebra over a field are equivalent to tensor automorphisms of scalar extension on its finite-dimensional comodules.

Equations

• TauCeti.Tannaka.fgPointTensorIsoEquiv k H A = MulEquiv.ofBijective (TauCeti.Tannaka.fgPointTensorIsoHom k H A) ⋯

@[simp]

theorem TauCeti.Tannaka.fgPointTensorIsoEquiv_apply (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : (fgPointTensorIsoEquiv k H A) g = fgPointTensorIso k H A g

The Tannakian equivalence sends a point to its tensor action.

@[simp]

theorem TauCeti.Tannaka.fgPointTensorIsoEquiv_symm_apply (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (eta : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) : (fgPointTensorIsoEquiv k H A).symm eta = reconstructedPoint k H A eta

The inverse Tannakian equivalence reconstructs the point of a tensor automorphism.