The point-representation--comodule equivalence

Let H be a commutative Hopf algebra over a commutative ring R. A point representation of the affine group represented by H is a natural action of every group of algebra-valued points on the corresponding scalar extension of a fixed R-module. The objects and their value-algebra category live in the maximum universe of R, H, and their shared underlying-module universe.

The fixed-module representation--comodule correspondence and its morphism criterion identify this category with the category of right H-comodules. Thus the functor-of-points and coordinate-Hopf- algebra descriptions agree not only on objects, but also on morphisms.

Main declarations

• TauCeti.PointRepresentationCat.toComodule: the functor recovering the associated comodule.
• TauCeti.pointRepresentationCategoryEquivalence: the equivalence between point representations and right comodules.
• TauCeti.FGPointRepresentationCat: the finite-generation restriction, equivalent to FGComoduleCat and hence the finite-dimensional representation category over a field.
• TauCeti.FGPointRepresentationCat.toComodule: the finite-generation restriction of the comodule functor.
• TauCeti.fgPointRepresentationCategoryEquivalence: the equivalence between finitely generated point representations and finitely generated comodules.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter VIII, §§2, 4, and 6.
• J. S. Milne, Algebraic Groups (2017), Chapter 4(a), Remark 4.1.

This supplies the categorical form of the Layer 1 representation--comodule dictionary in the ReductiveGroups roadmap; the monoidal and rigid refinements are not provided here.

noncomputable def TauCeti.PointRepresentationCat.toComodule (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.Functor (PointRepresentationCat R H) (ComoduleCat R H)

Recover the right comodule underlying a natural point representation.

Equations

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

@[simp]

theorem TauCeti.PointRepresentationCat.toComodule_obj_toSemimoduleCat (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : ((toComodule R H).obj V).toSemimoduleCat = V.toSemimoduleCat

The comodule functor leaves the underlying bundled semimodule of an object unchanged.

@[simp]

theorem TauCeti.PointRepresentationCat.toComodule_obj_coact (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : Comodule.coact ≍ Comodule.coact

The coaction on the image of a point representation is its recovered coaction.

@[simp]

theorem TauCeti.PointRepresentationCat.toComodule_map_toLinearMap (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} (f : V ⟶ W) : ((toComodule R H).map f).toLinearMap ≍ f.toLinearMap

The comodule functor leaves the underlying linear map of a morphism unchanged.

noncomputable def TauCeti.PointRepresentationCat.toComoduleFullyFaithful (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (toComodule R H).FullyFaithful

The comodule functor is fully faithful: colinearity is exactly equivariance for all algebra-valued point actions.

Equations

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

noncomputable def TauCeti.PointRepresentationCat.ofComodule (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (M : ComoduleCat R H) : PointRepresentationCat R H

Bundle a right comodule as its associated natural point representation, preserving its underlying bundled semimodule.

Equations

• TauCeti.PointRepresentationCat.ofComodule R H M = { toSemimoduleCat := M.toSemimoduleCat, representation := TauCeti.HopfAlgebra.PointRepresentation.ofComodule inferInstance }

@[simp]

theorem TauCeti.PointRepresentationCat.ofComodule_toSemimoduleCat (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (M : ComoduleCat R H) : (ofComodule R H M).toSemimoduleCat = M.toSemimoduleCat

The point representation associated to a comodule has the same underlying bundled semimodule.

@[simp]

theorem TauCeti.PointRepresentationCat.ofComodule_action_val (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (M : ComoduleCat R H) (A : CommAlgCat R) (x : ↑(HopfAlgebra.points A)) : ↑((CategoryTheory.ConcreteCategory.hom ((ofComodule R H M).representation.action A)) x) ≍ Comodule.endOfPoint (↑M.toSemimoduleCat) x.ofConv

The point action associated to a comodule is the comodule point-action endomorphism.

@[simp]

theorem TauCeti.PointRepresentationCat.toComodule_obj_ofComodule (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (M : ComoduleCat R H) : (toComodule R H).obj (ofComodule R H M) = M

Recovering the comodule associated to ofComodule returns the original bundled comodule.

instance TauCeti.PointRepresentationCat.toComoduleEssSurj (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (toComodule R H).EssSurj

Every right comodule is isomorphic to the comodule recovered from its natural point representation.

instance TauCeti.PointRepresentationCat.toComoduleIsEquivalence (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (toComodule R H).IsEquivalence

Recovering comodules from natural point representations is an equivalence of categories.

noncomputable def TauCeti.pointRepresentationCategoryEquivalence (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : PointRepresentationCat R H ≌ ComoduleCat R H

Natural point representations of an affine group and comodules over its coordinate Hopf algebra form equivalent categories.

Equations

• TauCeti.pointRepresentationCategoryEquivalence R H = (TauCeti.PointRepresentationCat.toComodule R H).asEquivalence

@[simp]

theorem TauCeti.pointRepresentationCategoryEquivalence_functor (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (pointRepresentationCategoryEquivalence R H).functor = PointRepresentationCat.toComodule R H

The forward functor of the point-representation equivalence is the concrete comodule functor.

noncomputable def TauCeti.pointRepresentationCategoryEquivalence.inverseObjIsoOfComodule (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (M : ComoduleCat R H) : (pointRepresentationCategoryEquivalence R H).inverse.obj M ≅ PointRepresentationCat.ofComodule R H M

The inverse equivalence sends a comodule to its associated point representation, up to the canonical isomorphism selected by Functor.inv.

Equations

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

def TauCeti.PointRepresentationCat.isFG (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.ObjectProperty (PointRepresentationCat R H)

The object property of finite generation on natural point representations. Over a field this is finite-dimensionality of the representation.

Equations

• TauCeti.PointRepresentationCat.isFG R H V = Module.Finite R ↑V.toSemimoduleCat

theorem TauCeti.PointRepresentationCat.isFG_iff (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : isFG R H V ↔ Module.Finite R ↑V.toSemimoduleCat

Finite generation of a point representation is finite generation of its underlying module.

@[simp]

theorem TauCeti.PointRepresentationCat.toComodule_obj_isFG_iff (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : ComoduleCat.isFG R H ((toComodule R H).obj V) ↔ isFG R H V

Recovering the comodule of a point representation preserves finite generation.

@[reducible, inline]

abbrev TauCeti.FGPointRepresentationCat (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : Type (max (max (u + 1) (v + 1)) (u_1 + 1))

The category of finitely generated natural point representations. Over a field, this is the category of finite-dimensional representations of the affine group represented by H.

Equations

• TauCeti.FGPointRepresentationCat R H = (TauCeti.PointRepresentationCat.isFG R H).FullSubcategory

instance TauCeti.PointRepresentationCat.isFG_isClosedUnderIsomorphisms (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (isFG R H).IsClosedUnderIsomorphisms

Finite generation of point representations is preserved under categorical isomorphisms.

noncomputable def TauCeti.fgPointRepresentationCategoryEquivalence (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : FGPointRepresentationCat R H ≌ FGComoduleCat R H

Finitely generated point representations and finitely generated comodules form equivalent categories. Over a field, this is the representation--comodule equivalence for finite-dimensional representations.

Equations

• TauCeti.fgPointRepresentationCategoryEquivalence R H = (TauCeti.PointRepresentationCat.toComodule R H).asEquivalence.congrFullSubcategory ⋯

@[reducible]

def TauCeti.FGPointRepresentationCat.carrier (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : Type w

The underlying type of a finitely generated point representation.

Equations

• ↑R H V = ↑V.obj.toSemimoduleCat

@[instance_reducible]

instance TauCeti.FGPointRepresentationCat.instCoeSortType (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CoeSort (FGPointRepresentationCat R H) (Type w)

Equations

• TauCeti.FGPointRepresentationCat.instCoeSortType R H = { coe := ↑R H }

@[instance_reducible]

instance TauCeti.FGPointRepresentationCat.instAddCommMonoidCarrier (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : AddCommMonoid (↑R H V)

Equations

• TauCeti.FGPointRepresentationCat.instAddCommMonoidCarrier R H V = TauCeti.PointRepresentationCat.instAddCommMonoidCarrier R H V.obj

@[instance_reducible]

instance TauCeti.FGPointRepresentationCat.instModuleCarrier (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : Module R (↑R H V)

Equations

• TauCeti.FGPointRepresentationCat.instModuleCarrier R H V = TauCeti.PointRepresentationCat.instModuleCarrier R H V.obj

instance TauCeti.FGPointRepresentationCat.instFiniteCarrier (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : Module.Finite R (↑R H V)

The underlying module of a finitely generated point representation is finitely generated.

@[reducible, inline]

abbrev TauCeti.FGPointRepresentationCat.representation (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : HopfAlgebra.PointRepresentation

The natural point action of a finitely generated point representation.

Equations

• TauCeti.FGPointRepresentationCat.representation R H V = V.obj.representation

@[reducible, inline]

abbrev TauCeti.FGPointRepresentationCat.incl (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.Functor (FGPointRepresentationCat R H) (PointRepresentationCat R H)

The inclusion of finitely generated point representations into all point representations.

Equations

• TauCeti.FGPointRepresentationCat.incl R H = (TauCeti.PointRepresentationCat.isFG R H).ι

@[reducible, inline]

noncomputable abbrev TauCeti.FGPointRepresentationCat.toComodule (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.Functor (FGPointRepresentationCat R H) (FGComoduleCat R H)

Recover the finitely generated comodule underlying a finitely generated point representation. This is the forward functor of fgPointRepresentationCategoryEquivalence.

Equations

• TauCeti.FGPointRepresentationCat.toComodule R H = (TauCeti.fgPointRepresentationCategoryEquivalence R H).functor

@[simp]

theorem TauCeti.FGPointRepresentationCat.toComodule_obj_obj (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : ((toComodule R H).obj V).obj = (PointRepresentationCat.toComodule R H).obj V.obj

The ambient comodule underlying the finite comodule functor is the recovered comodule.

@[simp]

theorem TauCeti.FGPointRepresentationCat.toComodule_obj_coact (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : FGPointRepresentationCat R H) : Comodule.coact ≍ Comodule.coact

The coaction on the finite comodule functor is the recovered coaction.

@[simp]

theorem TauCeti.FGPointRepresentationCat.toComodule_map_toLinearMap (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : FGPointRepresentationCat R H} (f : V ⟶ W) : ((toComodule R H).map f).hom.toLinearMap ≍ f.hom.toLinearMap

The finite comodule functor leaves the underlying linear map of a morphism unchanged.