Faithfulness of point automorphisms

An algebra-valued point of a Hopf algebra acts naturally on the scalar extension of every comodule. This file proves that the resulting natural automorphism determines the point.

For all comodules, it is enough to inspect the regular comodule: its matrix coefficients generate the whole Hopf algebra. For finitely generated comodules over a principal ideal domain, the fundamental theorem of coalgebras replaces the generally infinite regular comodule by its finite restricted subcomodules. Consequently, the point action on the finite scalar-extension functor is faithful. Over a field this is the injectivity half of Tannakian reconstruction for affine group schemes.

Main declarations

• TauCeti.Tannaka.pointNatIsoHom_injective: point automorphisms on all comodules determine the point.
• TauCeti.Tannaka.fgPointNatIsoHom_injective: point automorphisms on finitely generated comodules determine the point over a principal ideal domain.
• TauCeti.Tannaka.fgPoint_ext_of_forall_ofLinearEquiv_pointsAction: over a principal ideal domain, points are equal when their general-linear actions agree on every finitely generated comodule.
• TauCeti.Tannaka.commute_iff_forall_ofLinearEquiv_pointsAction: over a principal ideal domain, points commute exactly when their general-linear actions commute on every finitely generated comodule.

References

• J. S. Milne, Algebraic Groups (2017), Sections 4.5 and 9.4.
• M. Sweedler, Hopf Algebras, Chapter 2.

theorem TauCeti.Tannaka.pointNatIsoHom_injective (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] : Function.Injective ⇑(pointNatIsoHom R H A)

The action of algebra-valued points on the scalar-extension functor of all comodules is faithful. Equality of natural automorphisms on the regular comodule forces equality of the points on its matrix coefficients, which generate H.

theorem TauCeti.Tannaka.fgPointNatIsoHom_injective (R : Type u) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] [Module.Free R H] (A : Type x) [CommSemiring A] [Algebra R A] : Function.Injective ⇑(fgPointNatIsoHom R H A)

The action of algebra-valued points on the scalar-extension functor of finitely generated comodules is faithful over a principal ideal domain when the Hopf algebra is free as a module.

In particular this applies over a field. The finite restricted regular comodules jointly separate points, so equality of the natural automorphisms implies equality of the original algebra maps.

theorem TauCeti.Tannaka.fgPoint_ext_of_forall_ofLinearEquiv_pointsAction (R : Type u) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] [Module.Free R H] (A : Type x) [CommSemiring A] [Algebra R A] {g h : WithConv (H →ₐ[R] A)} (heq : ∀ (M : FGComoduleCat R H), LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g) = LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) h)) : g = h

Over a principal ideal domain, when H is free as a module, algebra-valued points are equal when their actions, viewed in the general linear group, agree on every finitely generated comodule. In particular, this applies over a field.

theorem TauCeti.Tannaka.commute_iff_forall_ofLinearEquiv_pointsAction (R : Type u) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (H : Type v) [Semiring H] [HopfAlgebra R H] [Module.Free R H] (A : Type x) [CommSemiring A] [Algebra R A] {g h : WithConv (H →ₐ[R] A)} : Commute g h ↔ ∀ (M : FGComoduleCat R H), Commute (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)) (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) h))

Over a principal ideal domain, when H is free as a module, two algebra-valued points commute if and only if their actions, viewed in the general linear group, commute on every finitely generated comodule. In particular, this applies over a field.