Global functionals from tensor automorphisms

Let H be a 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 compatible linear functional on every finite subcomodule of the regular comodule. Since these subcomodules cover H, the local functionals glue uniquely to a linear map

g_η : H → A.

This file performs that gluing, proves that g_η preserves one, and proves that a tensor automorphism arising from an A-valued point recovers the underlying linear map of that point. Tensor compatibility will next show that g_η preserves multiplication, upgrading it to an algebra-valued point.

Main declarations

• TauCeti.Tannaka.globalFunctional: the linear map obtained by gluing the local functionals.
• TauCeti.Tannaka.globalFunctional_comp_subtype: its restriction to a finite regular subcomodule is the prescribed local functional.
• TauCeti.Tannaka.globalFunctional_unique: the restriction property uniquely characterizes the global functional.
• TauCeti.Tannaka.globalFunctional_one: the global functional preserves the unit.
• TauCeti.Tannaka.globalFunctional_fgPointTensorIso: a point-induced tensor automorphism recovers the point's underlying linear map.

References

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

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

The global linear functional obtained by gluing the functionals extracted from a tensor automorphism on all finite subcomodules of the regular comodule.

Equations

• TauCeti.Tannaka.globalFunctional k H A η = TauCeti.Subcomodule.finiteSubcomoduleLift (fun (N : ↑TauCeti.Subcomodule.finiteSubcomodules) => TauCeti.Tannaka.localFunctional k H A η N) ⋯

@[simp]

theorem TauCeti.Tannaka.globalFunctional_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)) (N : ↑Subcomodule.finiteSubcomodules) (n : ↥↑N) : (globalFunctional k H A η) ↑n = (localFunctional k H A η N) n

The global functional agrees with the extracted local functional on every finite regular subcomodule.

@[simp]

theorem TauCeti.Tannaka.globalFunctional_comp_subtype (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) : globalFunctional k H A η ∘ₗ (↑N).toSubmodule.subtype = localFunctional k H A η N

Restricting the global functional to a finite regular subcomodule gives its local functional.

theorem TauCeti.Tannaka.globalFunctional_unique (k H A : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [CommRing A] [Algebra k A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H A)) (g : H →ₗ[k] A) (hg : ∀ (N : ↑Subcomodule.finiteSubcomodules) (n : ↥↑N), g ↑n = (localFunctional k H A η N) n) : g = globalFunctional k H A η

The restrictions to finite regular subcomodules uniquely determine the global functional.

@[simp]

theorem TauCeti.Tannaka.globalFunctional_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)) : (globalFunctional k H A η) 1 = 1

The global functional extracted from a tensor automorphism sends the unit of the coordinate Hopf algebra to the unit of the value algebra.

@[simp]

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

The global functional associated to the tensor automorphism induced by an algebra-valued point is the underlying linear map of that point.