Multiplicativity of Tannakian local functionals

Let H be a bialgebra over a commutative semiring k, let A be a commutative k-algebra, and let η be a tensor automorphism of scalar extension on finitely generated H-comodules. The functional extracted from η on a finite subcomodule of the regular comodule is compatible with multiplication.

More precisely, if finite regular subcomodules N and P have all their pairwise products in a third finite regular subcomodule Q, then

g_{η,Q}(n * p) = g_{η,N}(n) * g_{η,P}(p).

The proof applies naturality to the corestricted regular-comodule multiplication Subcomodule.mulHom and applies the tensor law for η to 1 ⊗ n and 1 ⊗ p. Evaluation by the counit turns multiplication in the regular comodule into multiplication in A. Together with the gluing construction and a unit law still to be developed, this supplies the algebra-map law needed to reconstruct an A-valued point from a tensor automorphism.

Main declarations

• TauCeti.Tannaka.regularMulHom: multiplication of two finite regular subcomodules, corestricted to a finite regular subcomodule containing their products and packaged in FGComoduleCat.
• TauCeti.Tannaka.localFunctional_mul: the extracted local functionals preserve these products.

References

• J. S. Milne, Algebraic Groups (2017), section 9.4.
• Mathlib/RepresentationTheory/Tannaka.lean: mulRepHom and map_mul_toRightFDRepComp supply the formal pattern of a categorical multiplication morphism followed by naturality and the monoidal tensor law, adapted here to comodules.

noncomputable def TauCeti.Tannaka.regularMulHom (k H : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] (N P Q : ↑Subcomodule.finiteSubcomodules) (h : ∀ (n : ↥↑N) (p : ↥↑P), ↑n * ↑p ∈ ↑Q) : CategoryTheory.MonoidalCategoryStruct.tensorObj (finiteRegularObject k H N) (finiteRegularObject k H P) ⟶ finiteRegularObject k H Q

Multiplication of two finite regular subcomodules, corestricted to a finite regular subcomodule containing all their pairwise products.

Equations

• TauCeti.Tannaka.regularMulHom k H N P Q h = TauCeti.FGComoduleCat.ofHom ((↑N).mulHom (↑P) (↑Q) h)

@[simp]

theorem TauCeti.Tannaka.regularMulHom_toLinearMap (k H : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] (N P Q : ↑Subcomodule.finiteSubcomodules) (h : ∀ (n : ↥↑N) (p : ↥↑P), ↑n * ↑p ∈ ↑Q) : (regularMulHom k H N P Q h).hom.toLinearMap = ((↑N).mulHom (↑P) (↑Q) h).toLinearMap

The linear map underlying corestricted multiplication of finite regular subcomodules is the one underlying Subcomodule.mulHom.

@[simp]

theorem TauCeti.Tannaka.localFunctional_mul (k H A : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] [CommSemiring A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (N P Q : ↑Subcomodule.finiteSubcomodules) (h : ∀ (n : ↥↑N) (p : ↥↑P), ↑n * ↑p ∈ ↑Q) (n : ↥↑N) (p : ↥↑P) : (localFunctional k H A η Q) ⟨↑n * ↑p, ⋯⟩ = (localFunctional k H A η N) n * (localFunctional k H A η P) p

Local functionals extracted from a tensor automorphism preserve products whenever the products of the two source subcomodules lie in the chosen target subcomodule.