The tensor-automorphism group functor and natural Tannakian reconstruction

Let H be a bialgebra over a commutative ring R. Sending a commutative R-algebra A to the group of tensor automorphisms of scalar extension on the finite H-comodules is a functor

CommAlgCat R ⥤ GrpCat,    A ↦ Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A),

with the action on morphisms given by base change of components (TauCeti.Tannaka.tensorAutMapValue).

The functor needs no antipode: only the bialgebra structure enters. When H is moreover a Hopf algebra over a field and is commutative, the pointwise Tannakian equivalence TauCeti.Tannaka.fgPointTensorIsoEquiv is natural in A, so the functor of points of H is isomorphic to this tensor-automorphism functor. This is the group-functor form of Tannakian reconstruction: it identifies the two as functors of points, not merely group by group.

Tensor automorphisms of scalar extension live one universe above the comodules, while the points of H live in the universe of the value algebra, so the comparison is stated after the standard universe lift of the points functor.

Main declarations

• TauCeti.Tannaka.tensorAutFunctor: the tensor-automorphism group functor on commutative algebras.
• TauCeti.Tannaka.pointsFunctorIsoTensorAutFunctor: the Tannakian equivalence as a natural isomorphism of group-valued functors.

References

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

noncomputable def TauCeti.Tannaka.tensorAutFunctor (R : Type u) [CommRing R] (H : Type v) [Semiring H] [Bialgebra R H] : CategoryTheory.Functor (CommAlgCat R) GrpCat

The tensor-automorphism group functor of a bialgebra: a commutative R-algebra A is sent to the group of tensor automorphisms of scalar extension to A on the finite H-comodules, and a morphism of value algebras acts by base change of components.

Equations

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

@[simp]

theorem TauCeti.Tannaka.tensorAutFunctor_obj (R : Type u) [CommRing R] (H : Type v) [Semiring H] [Bialgebra R H] (A : CommAlgCat R) : (tensorAutFunctor R H).obj A = ↧(CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H ↑A))

The tensor-automorphism functor sends an algebra to its group of tensor automorphisms.

@[simp]

theorem TauCeti.Tannaka.tensorAutFunctor_map (R : Type u) [CommRing R] (H : Type v) [Semiring H] [Bialgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) : (tensorAutFunctor R H).map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (tensorAutMapValueHom R H (↑A) (↑B) (CommAlgCat.Hom.hom φ))) (CategoryTheory.eqToHom ⋯))

The tensor-automorphism functor acts on morphisms by base change of components. This is the morphism-level form, stated with the object transports so that it stays in simp normal form once tensorAutFunctor_obj fires; it matches TauCeti.GeneralLinear.scalarExtensionAutomorphismsFunctor_map.

theorem TauCeti.Tannaka.tensorAutFunctor_map_transport_apply (R : Type u) [CommRing R] (H : Type v) [Semiring H] [Bialgebra R H] {A B : CommAlgCat R} (φ : A ⟶ B) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H ↑A)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((tensorAutFunctor R H).map φ)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) η)) = tensorAutMapValue R H (↑A) (↑B) (CommAlgCat.Hom.hom φ) η

Applying the tensor-automorphism functor map to an explicitly transported tensor automorphism is base change of that automorphism.

noncomputable def TauCeti.Tannaka.pointsFunctorIsoTensorAutFunctor (k H : Type u) [Field k] [CommRing H] [HopfAlgebra k H] : HopfAlgebra.pointsFunctor.comp GrpCat.uliftFunctor ≅ tensorAutFunctor k H

Tannakian reconstruction as a natural isomorphism of group-valued functors on commutative k-algebras: the functor of points of H is isomorphic to its tensor-automorphism functor.

The points functor is composed with the universe lift because tensor automorphisms of scalar extension live one universe above the value algebra.

Equations

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

theorem TauCeti.Tannaka.pointsFunctorIsoTensorAutFunctor_hom_app_apply (k H : Type u) [Field k] [CommRing H] [HopfAlgebra k H] (A : CommAlgCat k) (x : ULift.{u + 1, u} (WithConv (H →ₐ[k] ↑A))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((pointsFunctorIsoTensorAutFunctor k H).hom.app A)) x) = fgPointTensorIso k H (↑A) x.down

The natural Tannakian isomorphism sends a point to its tensor action. Not a simp lemma: the argument's type is the composite functor's value, which simp rewrites, so the left-hand side is not in normal form.

theorem TauCeti.Tannaka.pointsFunctorIsoTensorAutFunctor_inv_app_apply (k H : Type u) [Field k] [CommRing H] [HopfAlgebra k H] (A : CommAlgCat k) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H ↑A)) : ((CategoryTheory.ConcreteCategory.hom ((pointsFunctorIsoTensorAutFunctor k H).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) η)).down = reconstructedPoint k H (↑A) η

The inverse of the natural Tannakian isomorphism reconstructs the point of a tensor automorphism. Not a simp lemma, for the same reason as the previous one.