Point automorphisms of scalar extension

Let H be a Hopf algebra over a commutative semiring R, and let A be a commutative R-algebra. Scalar extension of the underlying-module functor is constructed for all comodules in TauCeti.Algebra.Coalgebra.Comodule.ScalarExtension and restricted to finitely generated comodules in TauCeti.Algebra.Coalgebra.Comodule.Finite.ScalarExtension.Basic:

FGComoduleCat R H ⥤ SemimoduleCat A,    M ↦ A ⊗[R] M.

Every A-valued point of H acts naturally and invertibly on the all-comodule functor: its component at M is the usual point action on A ⊗[R] M. These automorphisms form a group homomorphism, which restricts by precomposition to the finite-comodule functor.

This is the base change of the neutral underlying-module functor, without a faithfulness claim: scalar extension along an arbitrary R → A need not be faithful. Equipping this functor and these natural automorphisms with their tensor compatibilities is a separate step; together, the constructions supply categorical infrastructure for Tannakian reconstruction in Layer 1 of the reductive-groups roadmap.

Main declarations

• TauCeti.Tannaka.pointNatIso: the point action as a natural automorphism of the functor.
• TauCeti.Tannaka.pointNatIsoHom: points acting on all comodules, as a group homomorphism.
• TauCeti.Tannaka.fgPointNatIsoHom: the induced action on finitely generated comodules.

References

This is the scalar-extended underlying-module functor and point action used in Tannakian reconstruction; see J. S. Milne, Algebraic Groups (2017), §§4.5 and 9.4. The construction reuses Mathlib's linear-map base change and Tau Ceti's finite-comodule category and point action.

noncomputable def TauCeti.Tannaka.pointNatIso (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : ComoduleCat.scalarExtensionFunctor R H A ≅ ComoduleCat.scalarExtensionFunctor R H A

Every algebra-valued point acts as a natural automorphism of the scalar-extension functor. Naturality is precisely the fact that scalar extension of a comodule morphism intertwines point actions.

Equations

• TauCeti.Tannaka.pointNatIso R H A g = CategoryTheory.NatIso.ofComponents (TauCeti.Tannaka.pointIso✝ R H A g) ⋯

@[simp]

theorem TauCeti.Tannaka.pointNatIso_hom_app (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (M : ComoduleCat R H) : (pointNatIso R H A g).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((Comodule.pointsAction ↑M.toSemimoduleCat) g).toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))

The component of the point natural automorphism is the transported point action.

@[simp]

theorem TauCeti.Tannaka.pointNatIso_inv_app (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (M : ComoduleCat R H) : (pointNatIso R H A g).inv.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((Comodule.pointsAction ↑M.toSemimoduleCat) g).toModuleIsoₛ.inv (CategoryTheory.eqToHom ⋯))

The inverse component of the point natural automorphism is the transported inverse point action.

noncomputable def TauCeti.Tannaka.pointNatIsoHom (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] : WithConv (H →ₐ[R] A) →* CategoryTheory.Aut (ComoduleCat.scalarExtensionFunctor R H A)

Algebra-valued points act on the scalar-extension functor by natural automorphisms.

Equations

• TauCeti.Tannaka.pointNatIsoHom R H A = { toFun := TauCeti.Tannaka.pointNatIso R H A, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.Tannaka.pointNatIsoHom_apply (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : (pointNatIsoHom R H A) g = pointNatIso R H A g

Evaluating the points action homomorphism gives the corresponding natural automorphism.

noncomputable def TauCeti.Tannaka.fgPointNatIsoHom (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] : WithConv (H →ₐ[R] A) →* CategoryTheory.Aut (FGComoduleCat.scalarExtensionFunctor R H A)

Restricting the point action to finitely generated comodules gives automorphisms of the finite scalar-extension functor used in Tannakian reconstruction.

Equations

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

@[simp]

theorem TauCeti.Tannaka.fgPointNatIsoHom_hom_app (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (M : FGComoduleCat R H) : ((fgPointNatIsoHom R H A) g).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((Comodule.pointsAction ↑M) g).toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))

The component of the finite-comodule point automorphism is the transported point action.

@[simp]

theorem TauCeti.Tannaka.fgPointNatIsoHom_inv_app (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type x) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (M : FGComoduleCat R H) : ((fgPointNatIsoHom R H A) g).inv.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((Comodule.pointsAction ↑M) g).toModuleIsoₛ.inv (CategoryTheory.eqToHom ⋯))

The inverse component of the finite-comodule point automorphism is the transported inverse point action.