Tensor automorphisms from algebraic-group points

Let H be a Hopf algebra over a commutative semiring R, and let A be a commutative R-algebra. Scalar extension of finite H-comodules is a strong monoidal functor

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

Every A-valued point of H already acts naturally on this functor. This file proves that the action preserves the tensor product and tensor unit, and therefore packages it as an automorphism of the corresponding bundled lax monoidal functor. Over a principal ideal domain, when H is free as an R-module, this map from points to tensor automorphisms is injective.

Assembling an automorphism of scalar extension from a natural family of linear automorphisms is TauCeti.FGComoduleCat.autOfComponents, which needs only the coalgebra structure; adding the tensor-unit and tensor comparisons upgrades it to a tensor automorphism here.

This is the faithful direction of the tensor-automorphism formulation of Tannakian reconstruction. The converse, recovering a point from every tensor automorphism, remains a separate theorem.

Main declarations

• TauCeti.Tannaka.monoidalAutOfComponents: the same, with the unit and tensor conditions, as a tensor automorphism.
• TauCeti.Tannaka.scalarExtensionComponent: a tensor-automorphism component transported to an explicit scalar-extension tensor product.
• TauCeti.Tannaka.scalarExtensionComponent_tensor: the elementwise tensor law for transported components.
• TauCeti.Tannaka.scalarExtensionComponent_one and TauCeti.Tannaka.scalarExtensionComponent_mul: transported components are multiplicative in the tensor automorphism.
• TauCeti.Tannaka.scalarExtensionComponentGL: a transported component as an element of the general linear group of the scalar extension.
• TauCeti.Tannaka.scalarExtensionComponent_tensorUnit and TauCeti.Tannaka.distribBaseChange_comp_scalarExtensionComponent: the unit and tensor halves of the monoidal condition, read off the transported components.
• TauCeti.Tannaka.isMonoidal_fgPointNatIsoHom_hom: point actions on finite comodules preserve the tensor unit and tensor product.
• TauCeti.Tannaka.fgPointTensorIsoHom: points act on finite-comodule scalar extension by tensor automorphisms.
• TauCeti.Tannaka.fgPointTensorIsoHom_injective: this action is faithful over a principal ideal domain when the Hopf algebra is free.

References

• J. S. Milne, Algebraic Groups (2017), §§4.5 and 9.4.
• Mathlib/RepresentationTheory/Tannaka.lean: the bundled monoidal forgetful functor forget, point homomorphism equivHom, and tensor step in map_mul_toRightFDRepComp provide the formal pattern adapted here to comodules and scalar extension.

noncomputable def TauCeti.Tannaka.scalarExtensionComponent (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) : TensorProduct R A ↑M →ₗ[A] TensorProduct R A ↑M

The component of a tensor automorphism, transported from the object chosen by the scalar-extension functor to the explicit tensor product A ⊗[R] M.

Equations

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

theorem TauCeti.Tannaka.scalarExtensionComponent_apply (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) (x : TensorProduct R A ↑M) : (scalarExtensionComponent R H A η M) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom (η.hom.hom.app M)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x))

Evaluation formula for a transported tensor-automorphism component.

theorem TauCeti.Tannaka.scalarExtensionComponent_ext (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η θ : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (h : ∀ (M : FGComoduleCat R H), scalarExtensionComponent R H A η M = scalarExtensionComponent R H A θ M) : η = θ

Tensor automorphisms of scalar extension are equal when all their explicitly transported components are equal.

theorem TauCeti.Tannaka.scalarExtensionComponent_ext_iff {R : Type u} [CommSemiring R] {H : Type v} [Semiring H] [Bialgebra R H] {A : Type u} [CommSemiring A] [Algebra R A] {η θ : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)} : η = θ ↔ ∀ (M : FGComoduleCat R H), scalarExtensionComponent R H A η M = scalarExtensionComponent R H A θ M

theorem TauCeti.Tannaka.scalarExtensionComponent_natural (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) {M N : FGComoduleCat R H} (f : M ⟶ N) : LinearMap.baseChange A f.hom.toLinearMap ∘ₗ scalarExtensionComponent R H A η M = scalarExtensionComponent R H A η N ∘ₗ LinearMap.baseChange A f.hom.toLinearMap

Naturality of the explicitly transported components of a tensor automorphism.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_tensor (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M N : FGComoduleCat R H) (x : TensorProduct R A ↑M) (y : TensorProduct R A ↑N) : (scalarExtensionComponent R H A η (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) ((TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm (x ⊗ₜ[A] y)) = (TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm ((scalarExtensionComponent R H A η M) x ⊗ₜ[A] (scalarExtensionComponent R H A η N) y)

Tensor compatibility of the explicitly transported components of a tensor automorphism.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_one (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (M : FGComoduleCat R H) : scalarExtensionComponent R H A 1 M = LinearMap.id

The identity tensor automorphism has identity transported components.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_mul (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η θ : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) : scalarExtensionComponent R H A (η * θ) M = scalarExtensionComponent R H A η M ∘ₗ scalarExtensionComponent R H A θ M

Multiplying tensor automorphisms composes their transported components: multiplication in Aut is reverse composition, and the object transports between the two components cancel.

noncomputable def TauCeti.Tannaka.scalarExtensionComponentGL (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) : LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)

The transported component of a tensor automorphism, as an element of the general linear group of the scalar extension. Its inverse is the component of the inverse automorphism.

Equations

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

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponentGL_coe (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) : ↑(scalarExtensionComponentGL R H A η M) = scalarExtensionComponent R H A η M

The underlying linear map of the general-linear-group form of a transported component is that component.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponentGL_inv (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M : FGComoduleCat R H) : (scalarExtensionComponentGL R H A η M)⁻¹ = scalarExtensionComponentGL R H A η⁻¹ M

The inverse of a transported component is the transported component of the inverse tensor automorphism.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_tensorUnit (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) : scalarExtensionComponent R H A η (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat R H)) = LinearMap.id

The transported component of a tensor automorphism at the tensor unit is the identity: this is the unit half of the monoidal condition.

theorem TauCeti.Tannaka.distribBaseChange_comp_scalarExtensionComponent (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (M N : FGComoduleCat R H) : ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm ∘ₗ TensorProduct.map (scalarExtensionComponent R H A η M) (scalarExtensionComponent R H A η N) = scalarExtensionComponent R H A η (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm

Composite form of the tensor law for transported components: the scalar-extension tensorator intertwines the components at M and N with the component at M ⊗ N.

theorem TauCeti.Tannaka.scalarExtensionComponent_eq_of_hom_app (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (M : FGComoduleCat R H) (F : LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (eta : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)) (happ : eta.hom.hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp F.toLinearEquiv.toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))) : scalarExtensionComponent R H A eta M = ↑F

Evaluate a transported scalar-extension component from the corresponding natural transformation component.

theorem TauCeti.Tannaka.isMonoidal_of_linear_components (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (F : (M : FGComoduleCat R H) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (η : CategoryTheory.Aut (FGComoduleCat.scalarExtensionFunctor R H A)) (happ : ∀ (M : FGComoduleCat R H), η.hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F M).toLinearEquiv.toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))) (hunit : F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat R H)) = 1) (htensor : ∀ (M N : FGComoduleCat R H), ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm ∘ₗ TensorProduct.map ↑(F M) ↑(F N) = ↑(F (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm) : CategoryTheory.NatTrans.IsMonoidal η.hom

A natural automorphism of scalar extension is monoidal when its transported linear components preserve the tensor unit and tensor products.

noncomputable def TauCeti.Tannaka.monoidalAutOfComponents (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (F : (M : FGComoduleCat R H) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hnat : ∀ {M N : FGComoduleCat R H} (g : M ⟶ N), LinearMap.baseChange A g.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A g.hom.toLinearMap) (hunit : F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat R H)) = 1) (htensor : ∀ (M N : FGComoduleCat R H), ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm ∘ₗ TensorProduct.map ↑(F M) ↑(F N) = ↑(F (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm) : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor R H A)

A family of A-linear automorphisms of the scalar extensions of the finite comodules that is natural in the comodule, preserves the tensor unit, and is compatible with the tensor comparison, as a tensor automorphism of scalar extension.

Equations

• TauCeti.Tannaka.monoidalAutOfComponents R H A F hnat hunit htensor = CategoryTheory.LaxMonoidalFunctor.isoMk (TauCeti.FGComoduleCat.autOfComponents R H A F ⋯)

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_monoidalAutOfComponents (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [Bialgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (F : (M : FGComoduleCat R H) → LinearMap.GeneralLinearGroup A (TensorProduct R A ↑M)) (hnat : ∀ {M N : FGComoduleCat R H} (g : M ⟶ N), LinearMap.baseChange A g.hom.toLinearMap ∘ₗ ↑(F M) = ↑(F N) ∘ₗ LinearMap.baseChange A g.hom.toLinearMap) (hunit : F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat R H)) = 1) (htensor : ∀ (M N : FGComoduleCat R H), ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm ∘ₗ TensorProduct.map ↑(F M) ↑(F N) = ↑(F (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm) (M : FGComoduleCat R H) : scalarExtensionComponent R H A (monoidalAutOfComponents R H A F ⋯ hunit htensor) M = ↑(F M)

The transported component of the tensor automorphism assembled from a natural monoidal family of linear automorphisms is that family.

@[simp]

theorem TauCeti.Tannaka.ofLinearEquiv_pointsAction_tensorUnit_eq_one (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat R H))) g) = 1

The point action on the tensor unit is the identity automorphism.

theorem TauCeti.Tannaka.distribBaseChange_comp_pointsAction (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (M N : FGComoduleCat R H) : ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm ∘ₗ TensorProduct.map ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)) ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑N) g)) = ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) g)) ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A ↑M ↑N).symm

The scalar-extension tensorator intertwines the tensor product of two point actions with the point action on the tensor product comodule.

theorem TauCeti.Tannaka.isMonoidal_fgPointNatIsoHom_hom (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : CategoryTheory.NatTrans.IsMonoidal ((fgPointNatIsoHom R H A) g).hom

The natural automorphism induced by an algebra-valued point is monoidal.

noncomputable def TauCeti.Tannaka.fgPointTensorIso (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : FGComoduleCat.scalarExtensionMonoidalFunctor R H A ≅ FGComoduleCat.scalarExtensionMonoidalFunctor R H A

An algebra-valued point as a tensor automorphism of finite-comodule scalar extension.

Equations

• TauCeti.Tannaka.fgPointTensorIso R H A g = CategoryTheory.LaxMonoidalFunctor.isoMk ((TauCeti.Tannaka.fgPointNatIsoHom R H A) g)

@[simp]

theorem TauCeti.Tannaka.fgPointTensorIso_hom_hom (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : (fgPointTensorIso R H A g).hom.hom = ((fgPointNatIsoHom R H A) g).hom

Forgetting tensor compatibility from the point automorphism recovers its underlying natural automorphism.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_fgPointTensorIso (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (M : FGComoduleCat R H) : scalarExtensionComponent R H A (fgPointTensorIso R H A g) M = ↑((Comodule.pointsAction ↑M) g)

The transported component of the tensor automorphism induced by a point is the usual point action on every finite comodule.

@[simp]

theorem TauCeti.Tannaka.fgPointTensorIso_inv_hom (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : (fgPointTensorIso R H A g).inv.hom = ((fgPointNatIsoHom R H A) g).inv

Forgetting tensor compatibility from the inverse point automorphism recovers the inverse underlying natural automorphism.

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

Algebra-valued points act on finite-comodule scalar extension by tensor automorphisms.

Equations

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

@[simp]

theorem TauCeti.Tannaka.fgPointTensorIsoHom_apply (R : Type u) [CommSemiring R] (H : Type v) [Semiring H] [HopfAlgebra R H] (A : Type u) [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : (fgPointTensorIsoHom R H A) g = fgPointTensorIso R H A g

Evaluating the point tensor-action homomorphism gives the corresponding tensor automorphism.

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

The tensor-automorphism action of points is faithful over a principal ideal domain when the Hopf algebra is free as a module.