Reconstructing algebra-valued points from tensor automorphisms

Let H be a commutative Hopf algebra over a field k, and let A be a commutative k-algebra. A tensor automorphism of scalar extension on the finite-dimensional H-comodules determines a linear functional H → A. Tensor compatibility makes this functional multiplicative, while compatibility with the tensor unit makes it preserve one. It therefore defines an A-valued point of the affine group represented by H.

This file packages that reconstructed point and proves that reconstructing the tensor automorphism induced by a point returns the original point. The converse equality, that the reconstructed point induces the original component on every finite comodule, requires the matrix-coefficient separation argument developed separately.

Main declarations

• TauCeti.Tannaka.globalFunctional_mul: the glued functional preserves multiplication.
• TauCeti.Tannaka.reconstructedPoint: the algebra-valued point reconstructed from a tensor automorphism.
• TauCeti.Tannaka.reconstructedPoint_fgPointTensorIso: reconstruction recovers every algebra-valued point.

References

• J. S. Milne, Algebraic Groups (2017), §9.4.

@[simp]

theorem TauCeti.Tannaka.globalFunctional_mul (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (x y : H) : (globalFunctional k H A η) (x * y) = (globalFunctional k H A η) x * (globalFunctional k H A η) y

The global functional reconstructed from a tensor automorphism preserves multiplication.

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

The algebra-valued point reconstructed from a tensor automorphism of finite-comodule scalar extension. Its underlying map is the global functional extracted from the automorphism.

Equations

• TauCeti.Tannaka.reconstructedPoint k H A η = WithConv.toConv (AlgHom.ofLinearMap (TauCeti.Tannaka.globalFunctional k H A η) ⋯ ⋯)

@[simp]

theorem TauCeti.Tannaka.reconstructedPoint_apply (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (x : H) : (reconstructedPoint k H A η).ofConv x = (globalFunctional k H A η) x

The reconstructed point evaluates as its defining global functional.

@[simp]

theorem TauCeti.Tannaka.reconstructedPoint_toLinearMap (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) : (reconstructedPoint k H A η).ofConv.toLinearMap = globalFunctional k H A η

The underlying linear map of the reconstructed point is the global functional.

@[simp]

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

Reconstructing the tensor automorphism induced by an algebra-valued point returns that point. Thus reconstruction is a left inverse to the tensor action of points.