The unit law for Tannakian local functionals

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 compatible linear functionals on the finite subcomodules of the regular comodule. This file proves the tensor-unit part of the algebra-map laws for those functionals: whenever a finite regular subcomodule contains 1, its local functional sends that element to 1 : A.

The proof maps the trivial tensor-unit comodule into the chosen regular subcomodule by r ↦ r • 1. Naturality transports the tensor automorphism along this map, while its monoidal unit axiom says that its component on the tensor unit fixes the canonical generator. The resulting theorem is the unit-law prerequisite for gluing the local functionals into the algebra-valued point in Tannakian reconstruction.

Main declaration

• TauCeti.Tannaka.localFunctional_one: every local functional sends the unit of a finite regular subcomodule to one.

References

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

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_one_tmul (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (N : ↑Subcomodule.finiteSubcomodules) (hOne : 1 ∈ ↑N) : (scalarExtensionComponent k H A η (finiteRegularObject k H N)) (1 ⊗ₜ[k] ⟨1, hOne⟩) = 1 ⊗ₜ[k] ⟨1, hOne⟩

The transported component of a tensor automorphism fixes 1 ⊗ 1 in every finite regular subcomodule containing the unit.

@[simp]

theorem TauCeti.Tannaka.localFunctional_one (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (N : ↑Subcomodule.finiteSubcomodules) (hOne : 1 ∈ ↑N) : (localFunctional k H A η N) ⟨1, hOne⟩ = 1

A local functional extracted from a tensor automorphism sends the unit of every finite regular subcomodule containing it to 1. This is the tensor-unit law needed to upgrade the glued functional on H to an algebra homomorphism.