Jordan factors of point actions

Let H be a Hopf algebra over a commutative semiring k, let K be a perfect extension field, and let g : H →ₐ[k] K be a K-valued point. On every finite-dimensional H-comodule, g acts by a linear automorphism after scalar extension to K. This file packages the semisimple and unipotent parts of those automorphisms as natural automorphisms of the finite-comodule scalar extension functor.

Naturality is substantive: a comodule morphism need be neither injective nor surjective. It follows from functoriality of the multiplicative Jordan--Chevalley decomposition under arbitrary intertwiners. The two natural factors commute and their product recovers the original point action in the automorphism group of the scalar-extension functor.

The final section combines this naturality with tensor-product compatibility of multiplicative Jordan decomposition. Thus both factors are tensor automorphisms. In the commutative coordinate-Hopf-algebra setting of the roadmap, Tannakian reconstruction can now lift them from compatible actions on representations to points of the original affine group. This is the representation-theoretic bridge in Layer 4 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.Tannaka.fgPointSemisimplePartNatIso: the natural semisimple part of a point action.
• TauCeti.Tannaka.fgPointUnipotentPartNatIso: the natural unipotent part of a point action.
• TauCeti.Tannaka.fgPointSemisimplePartTensorIso: the semisimple factors as a tensor automorphism.
• TauCeti.Tannaka.fgPointUnipotentPartTensorIso: the unipotent factors as a tensor automorphism.
• TauCeti.Tannaka.fgPointSemisimplePartNatIso_mul_fgPointUnipotentPartNatIso: their product is the original point action.
• TauCeti.Tannaka.fgPointSemisimplePartTensorIso_mul_fgPointUnipotentPartTensorIso: the same factorization among tensor automorphisms.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.

noncomputable def TauCeti.Tannaka.fgPointSemisimplePartNatIso (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : CategoryTheory.Aut (FGComoduleCat.scalarExtensionFunctor k H K)

The semisimple parts of a point's actions on finite comodules form an automorphism of scalar extension.

Equations

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

noncomputable def TauCeti.Tannaka.fgPointUnipotentPartNatIso (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : CategoryTheory.Aut (FGComoduleCat.scalarExtensionFunctor k H K)

The unipotent parts of a point's actions on finite comodules form an automorphism of scalar extension.

Equations

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

@[simp]

theorem TauCeti.Tannaka.fgPointSemisimplePartNatIso_hom_app (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : (fgPointSemisimplePartNatIso k H K g).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).semisimplePart.toLinearEquiv.toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))

The hom component of the semisimple-part automorphism is the semisimple part of the point action, transported across the scalar-extension functor's object equality.

@[simp]

theorem TauCeti.Tannaka.fgPointSemisimplePartNatIso_inv_app (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : (fgPointSemisimplePartNatIso k H K g).inv.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).semisimplePart.toLinearEquiv.toModuleIsoₛ.inv (CategoryTheory.eqToHom ⋯))

The inverse component of the semisimple-part automorphism is the inverse semisimple part of the point action, transported across the scalar-extension functor's object equality.

@[simp]

theorem TauCeti.Tannaka.fgPointUnipotentPartNatIso_hom_app (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : (fgPointUnipotentPartNatIso k H K g).hom.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).unipotentPart.toLinearEquiv.toModuleIsoₛ.hom (CategoryTheory.eqToHom ⋯))

The hom component of the unipotent-part automorphism is the unipotent part of the point action, transported across the scalar-extension functor's object equality.

@[simp]

theorem TauCeti.Tannaka.fgPointUnipotentPartNatIso_inv_app (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : (fgPointUnipotentPartNatIso k H K g).inv.app M = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).unipotentPart.toLinearEquiv.toModuleIsoₛ.inv (CategoryTheory.eqToHom ⋯))

The inverse component of the unipotent-part automorphism is the inverse unipotent part of the point action, transported across the scalar-extension functor's object equality.

theorem TauCeti.Tannaka.commute_fgPointSemisimplePartNatIso_fgPointUnipotentPartNatIso (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : Commute (fgPointSemisimplePartNatIso k H K g) (fgPointUnipotentPartNatIso k H K g)

The semisimple- and unipotent-part automorphisms of a point action commute.

@[simp]

theorem TauCeti.Tannaka.fgPointSemisimplePartNatIso_mul_fgPointUnipotentPartNatIso (k : Type u) (H : Type v) (K : Type x) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : fgPointSemisimplePartNatIso k H K g * fgPointUnipotentPartNatIso k H K g = (fgPointNatIsoHom k H K) g

Multiplying the semisimple- and unipotent-part automorphisms recovers the original point action.

theorem TauCeti.Tannaka.isMonoidal_fgPointSemisimplePartNatIso_hom (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : CategoryTheory.NatTrans.IsMonoidal (fgPointSemisimplePartNatIso k H K g).hom

The natural semisimple-factor automorphism preserves the tensor unit and tensor products.

theorem TauCeti.Tannaka.isMonoidal_fgPointUnipotentPartNatIso_hom (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : CategoryTheory.NatTrans.IsMonoidal (fgPointUnipotentPartNatIso k H K g).hom

The natural unipotent-factor automorphism preserves the tensor unit and tensor products.

noncomputable def TauCeti.Tannaka.fgPointSemisimplePartTensorIso (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H K)

The semisimple factors of a point's actions on finite comodules, as an automorphism of the monoidal scalar-extension functor.

Equations

• TauCeti.Tannaka.fgPointSemisimplePartTensorIso k H K g = CategoryTheory.LaxMonoidalFunctor.isoMk (TauCeti.Tannaka.fgPointSemisimplePartNatIso k H K g)

noncomputable def TauCeti.Tannaka.fgPointUnipotentPartTensorIso (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : CategoryTheory.Aut (FGComoduleCat.scalarExtensionMonoidalFunctor k H K)

The unipotent factors of a point's actions on finite comodules, as an automorphism of the monoidal scalar-extension functor.

Equations

• TauCeti.Tannaka.fgPointUnipotentPartTensorIso k H K g = CategoryTheory.LaxMonoidalFunctor.isoMk (TauCeti.Tannaka.fgPointUnipotentPartNatIso k H K g)

@[simp]

theorem TauCeti.Tannaka.fgPointSemisimplePartTensorIso_hom_hom (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (fgPointSemisimplePartTensorIso k H K g).hom.hom = (fgPointSemisimplePartNatIso k H K g).hom

Forgetting tensor compatibility from the semisimple-factor automorphism recovers its underlying natural automorphism.

@[simp]

theorem TauCeti.Tannaka.fgPointUnipotentPartTensorIso_hom_hom (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (fgPointUnipotentPartTensorIso k H K g).hom.hom = (fgPointUnipotentPartNatIso k H K g).hom

Forgetting tensor compatibility from the unipotent-factor automorphism recovers its underlying natural automorphism.

@[simp]

theorem TauCeti.Tannaka.fgPointSemisimplePartTensorIso_inv_hom (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (fgPointSemisimplePartTensorIso k H K g).inv.hom = (fgPointSemisimplePartNatIso k H K g).inv

Forgetting tensor compatibility from the inverse semisimple-factor automorphism recovers the inverse underlying natural automorphism.

@[simp]

theorem TauCeti.Tannaka.fgPointUnipotentPartTensorIso_inv_hom (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (fgPointUnipotentPartTensorIso k H K g).inv.hom = (fgPointUnipotentPartNatIso k H K g).inv

Forgetting tensor compatibility from the inverse unipotent-factor automorphism recovers the inverse underlying natural automorphism.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_fgPointSemisimplePartTensorIso (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : scalarExtensionComponent k H K (fgPointSemisimplePartTensorIso k H K g) M = ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).semisimplePart

The transported component of the semisimple-factor tensor automorphism is the semisimple part of the point action.

@[simp]

theorem TauCeti.Tannaka.scalarExtensionComponent_fgPointUnipotentPartTensorIso (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : scalarExtensionComponent k H K (fgPointUnipotentPartTensorIso k H K g) M = ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).unipotentPart

The transported component of the unipotent-factor tensor automorphism is the unipotent part of the point action.

theorem TauCeti.Tannaka.commute_fgPointSemisimplePartTensorIso_fgPointUnipotentPartTensorIso (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : Commute (fgPointSemisimplePartTensorIso k H K g) (fgPointUnipotentPartTensorIso k H K g)

The tensor automorphisms formed by the semisimple and unipotent factors commute.

@[simp]

theorem TauCeti.Tannaka.fgPointSemisimplePartTensorIso_mul_fgPointUnipotentPartTensorIso (k : Type u) (H : Type v) (K : Type u) [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : fgPointSemisimplePartTensorIso k H K g * fgPointUnipotentPartTensorIso k H K g = fgPointTensorIso k H K g

Multiplying the tensor automorphisms formed by the semisimple and unipotent factors recovers the tensor automorphism induced by the original point.