Morphisms of point representations and comodules

This file characterizes the morphisms of comodules and natural point representations of the affine group represented by a commutative Hopf algebra. A linear map is colinear exactly when every scalar extension intertwines the actions of every algebra-valued point. Explicit comodules may have carriers in independent universes; arbitrary point representations share the universe of their value-algebra category.

The converse uses the universal point of the Hopf algebra: evaluating equivariance there recovers the colinearity square. Consequently the pointwise condition ranges over all commutative value algebras, including nonreduced ones.

Main declarations

• TauCeti.HopfAlgebra.PointRepresentation.map_coact_of_baseChange_comp_endOfPoint_universal: intertwining at the universal point alone already forces colinearity.
• TauCeti.HopfAlgebra.PointRepresentation.map_coact_iff_baseChange_comp_endOfPoint: the fixed-morphism criterion for explicit comodules with carriers in independent universes.
• TauCeti.HopfAlgebra.PointRepresentation.map_coact_iff_baseChange_comp_action: the fixed-morphism representation--comodule dictionary for arbitrary point representations.
• TauCeti.HopfAlgebra.PointRepresentation.map_coact_iff_baseChange_comp_ofComodule_action: the specialization to point actions induced by explicit comodules.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter VIII, §§2, 4, and 6.

theorem TauCeti.HopfAlgebra.PointRepresentation.map_coact_of_baseChange_comp_endOfPoint_universal {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] {W : Type x} [AddCommMonoid W] [Module R W] (rho : Comodule R H V) (sigma : Comodule R H W) (f : V →ₗ[R] W) (huniv : LinearMap.baseChange (↑↧(ULift.{max u v w x, v} H)) f ∘ₗ Comodule.endOfPoint V (WithConv.toConv ↑ULift.algEquiv.{u, v, max (max (max u v) w) x}.symm).ofConv = Comodule.endOfPoint W (WithConv.toConv ↑ULift.algEquiv.{u, v, max (max (max u v) w) x}.symm).ofConv ∘ₗ LinearMap.baseChange (↑↧(ULift.{max u v w x, v} H)) f) : TensorProduct.map f LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ f

Intertwining at the universal point suffices for colinearity. A linear map between two right comodules is colinear as soon as its scalar extension to ULift H intertwines the point actions of the universal point; no condition at other value algebras is needed.

theorem TauCeti.HopfAlgebra.PointRepresentation.map_coact_iff_baseChange_comp_endOfPoint {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] {W : Type x} [AddCommMonoid W] [Module R W] (rho : Comodule R H V) (sigma : Comodule R H W) (f : V →ₗ[R] W) : TensorProduct.map f LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ f ↔ ∀ (A : CommAlgCat R) (p : ↑(points A)), LinearMap.baseChange (↑A) f ∘ₗ Comodule.endOfPoint V p.ofConv = Comodule.endOfPoint W p.ofConv ∘ₗ LinearMap.baseChange (↑A) f

A linear map between two right comodules is colinear if and only if all its scalar extensions intertwine their point actions.

The two carriers may lie in independent universes. The value algebras lie in one common universe large enough for the base ring, Hopf algebra, and both carriers. No finiteness or flatness assumption is required.

theorem TauCeti.HopfAlgebra.PointRepresentation.map_coact_iff_baseChange_comp_action {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] {W : Type w} [AddCommMonoid W] [Module R W] (Theta : PointRepresentation) (Psi : PointRepresentation) (f : V →ₗ[R] W) : TensorProduct.map f LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ f ↔ ∀ (A : CommAlgCat R) (x : ↑(points A)), LinearMap.baseChange (↑A) f ∘ₗ ↑((CategoryTheory.ConcreteCategory.hom (Theta.action A)) x) = ↑((CategoryTheory.ConcreteCategory.hom (Psi.action A)) x) ∘ₗ LinearMap.baseChange (↑A) f

A linear map between two natural point representations is colinear between their recovered comodules if and only if all its scalar extensions intertwine every algebra-valued point action.

The two carriers share a universe so that the point representations are defined on the same literal category of value algebras. No finiteness or flatness assumption is required.

theorem TauCeti.HopfAlgebra.PointRepresentation.map_coact_iff_baseChange_comp_ofComodule_action {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] {W : Type w} [AddCommMonoid W] [Module R W] (rho : Comodule R H V) (sigma : Comodule R H W) (f : V →ₗ[R] W) : TensorProduct.map f LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ f ↔ ∀ (A : CommAlgCat R) (x : ↑(points A)), LinearMap.baseChange (↑A) f ∘ₗ ↑((CategoryTheory.ConcreteCategory.hom ((ofComodule rho).action A)) x) = ↑((CategoryTheory.ConcreteCategory.hom ((ofComodule sigma).action A)) x) ∘ₗ LinearMap.baseChange (↑A) f

A linear map between two right comodules is a comodule morphism if and only if all its scalar extensions intertwine the point representations induced by those comodules.