Local functionals from tensor automorphisms

Let H be a bialgebra over a commutative semiring k, and let A be a commutative k-algebra. A tensor automorphism η of scalar extension on the finitely generated H-comodules acts, in particular, on every finite subcomodule N of the regular comodule H. Applying that component to 1 ⊗ n and then applying the counit to the N-factor gives a linear functional

g_{η,N} : N → A.

Naturality of η under inclusions of finite subcomodules makes these functionals compatible. They therefore form exactly the local data needed to reconstruct one linear map H → A from the directed union of the finite subcomodules. The separate directed-union construction can then glue them; tensor and unit compatibility will supply the algebra-map laws.

Main declarations

• TauCeti.Tannaka.counitEvaluation: counit evaluation after scalar extension on a regular subcomodule.
• TauCeti.Tannaka.localFunctional: the functional extracted from one finite subcomodule.
• TauCeti.Tannaka.localFunctional_eq_comp_inclusion: compatibility under inclusion.
• TauCeti.Tannaka.localFunctional_fgPointTensorIso: a point recovers its restriction to every finite subcomodule.

References

• J. S. Milne, Algebraic Groups (2017), §9.4.
• Mathlib/RepresentationTheory/Tannaka.lean: the naturality and monoidal-transport pattern is adapted here from the proof of map_mul_toRightFDRepComp.

@[reducible, inline]

noncomputable abbrev TauCeti.Tannaka.finiteRegularObject (k H : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] (N : ↑Subcomodule.finiteSubcomodules) : FGComoduleCat k H

A finite subcomodule of the regular comodule, bundled as an object of the finite comodule category.

Equations

• TauCeti.Tannaka.finiteRegularObject k H N = { obj := TauCeti.ComoduleCat.of k H ↥↑N, property := ⋯ }

noncomputable def TauCeti.Tannaka.counitEvaluation (k : Type u) [CommSemiring k] (H : Type v) [AddCommMonoid H] [Module k H] [Coalgebra k H] (A : Type w) [CommSemiring A] [Algebra k A] (N : Subcomodule k H H) : TensorProduct k A ↥N →ₗ[A] A

Evaluation after scalar extension by applying the counit on a regular subcomodule.

Equations

• TauCeti.Tannaka.counitEvaluation k H A N = TauCeti.Module.Dual.baseChangeEvaluation (1 ⊗ₜ[k] (CoalgebraStruct.counit ∘ₗ SMulMemClass.subtype N))

@[simp]

theorem TauCeti.Tannaka.counitEvaluation_tmul (k : Type u) [CommSemiring k] (H : Type v) [AddCommMonoid H] [Module k H] [Coalgebra k H] (A : Type w) [CommSemiring A] [Algebra k A] (N : Subcomodule k H H) (a : A) (n : ↥N) : (counitEvaluation k H A N) (a ⊗ₜ[k] n) = a * (algebraMap k A) (CoalgebraStruct.counit ↑n)

Counit evaluation on a pure scalar-extension tensor.

theorem TauCeti.Tannaka.counitEvaluation_apply (k : Type u) [CommSemiring k] (H : Type v) [AddCommMonoid H] [Module k H] [Coalgebra k H] (A : Type w) [CommSemiring A] [Algebra k A] (N : Subcomodule k H H) (z : TensorProduct k A ↥N) : (counitEvaluation k H A N) z = (TensorProduct.AlgebraTensorModule.rid k A A) ((LinearMap.baseChange A (CoalgebraStruct.counit ∘ₗ SMulMemClass.subtype N)) z)

Counit evaluation is the base change of the counit restricted to the regular subcomodule.

noncomputable def TauCeti.Tannaka.regularInclusion (k H : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] {N Q : ↑Subcomodule.finiteSubcomodules} (hNQ : ↑N ≤ ↑Q) : finiteRegularObject k H N ⟶ finiteRegularObject k H Q

Inclusion of finite regular subcomodules as a morphism in the finite comodule category.

Equations

• TauCeti.Tannaka.regularInclusion k H hNQ = TauCeti.FGComoduleCat.ofHom (let __LinearMap := Submodule.inclusion hNQ; { toLinearMap := __LinearMap, map_coact := ⋯ })

@[simp]

theorem TauCeti.Tannaka.regularInclusion_apply (k H : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] {N Q : ↑Subcomodule.finiteSubcomodules} (hNQ : ↑N ≤ ↑Q) (n : ↥↑N) : (CategoryTheory.ConcreteCategory.hom (regularInclusion k H hNQ)) n = ⟨↑n, ⋯⟩

The inclusion of finite regular subcomodules is the ordinary subtype inclusion.

@[simp]

theorem TauCeti.Tannaka.regularInclusion_toLinearMap (k H : Type u) [CommSemiring k] [Semiring H] [Bialgebra k H] [Module.Flat k H] {N Q : ↑Subcomodule.finiteSubcomodules} (hNQ : ↑N ≤ ↑Q) : (regularInclusion k H hNQ).hom.toLinearMap = Submodule.inclusion hNQ

The linear map underlying inclusion of finite regular subcomodules is the ordinary submodule inclusion.

noncomputable def TauCeti.Tannaka.localFunctional (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 : ↑Subcomodule.finiteSubcomodules) : ↥↑N →ₗ[k] A

The linear functional on a finite subcomodule of the regular comodule extracted from a tensor automorphism. It applies the automorphism to 1 ⊗ n and then evaluates the regular coordinate by the counit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Tannaka.localFunctional_apply (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 : ↑Subcomodule.finiteSubcomodules) (n : ↥↑N) : (localFunctional k H A η N) n = (counitEvaluation k H A ↑N) ((scalarExtensionComponent k H A η (finiteRegularObject k H N)) (1 ⊗ₜ[k] n))

Evaluation formula for the functional extracted from a finite regular subcomodule.

theorem TauCeti.Tannaka.localFunctional_eq_comp_inclusion (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 Q : ↑Subcomodule.finiteSubcomodules) (hNQ : ↑N ≤ ↑Q) : localFunctional k H A η N = localFunctional k H A η Q ∘ₗ Submodule.inclusion hNQ

The local functionals extracted from a tensor automorphism agree under inclusion of finite subcomodules.

@[simp]

theorem TauCeti.Tannaka.localFunctional_fgPointTensorIso (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) (N : ↑Subcomodule.finiteSubcomodules) (n : ↥↑N) : (localFunctional k H A (fgPointTensorIso k H A g) N) n = g.ofConv ↑n

For a tensor automorphism induced by an algebra-valued point g, the local functional is the restriction of g to the chosen finite subcomodule of the regular comodule.