The category of point representations

Let H be a commutative Hopf algebra over a commutative ring R. This file bundles natural actions of the affine group represented by H into a category. Morphisms are linear maps whose scalar extensions intertwine every algebra-valued point action.

The objects and the value-algebra category used by their actions live in the maximum universe of R, H, and the underlying module. In particular, morphisms here relate representations whose underlying modules lie in the same universe.

Main declarations

• TauCeti.PointRepresentationCat: the category of natural point representations.
• TauCeti.PointRepresentationCat.Hom: equivariant linear maps between point representations.

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.

structure TauCeti.PointRepresentationCat (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] extends SemimoduleCat R : Type (max (max (u + 1) (v + 1)) (w + 1))

The category of natural point representations of the affine group represented by H.

An object is an R-module together with a natural action of the represented point groups on all of its scalar extensions.

• carrier : Type w
• isAddCommMonoid : AddCommMonoid ↑self.toSemimoduleCat
• isModule : Module R ↑self.toSemimoduleCat
• representation : HopfAlgebra.PointRepresentation

  The natural point action on the underlying module.

@[instance_reducible]

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

Equations

• TauCeti.PointRepresentationCat.instCoeSortType R H = { coe := fun (V : TauCeti.PointRepresentationCat R H) => ↑V.toSemimoduleCat }

@[instance_reducible]

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

Equations

• TauCeti.PointRepresentationCat.instAddCommMonoidCarrier R H V = V.isAddCommMonoid

@[instance_reducible]

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

Equations

• TauCeti.PointRepresentationCat.instModuleCarrier R H V = V.isModule

@[reducible, inline]

abbrev TauCeti.PointRepresentationCat.of (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : Type w) [AddCommMonoid V] [Module R V] (Theta : HopfAlgebra.PointRepresentation) : PointRepresentationCat R H

Bundle a natural point representation on an R-module.

Equations

• TauCeti.PointRepresentationCat.of R H V Theta = { carrier := V, isAddCommMonoid := inst✝¹, isModule := inst✝, representation := Theta }

structure TauCeti.PointRepresentationCat.Hom (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V W : PointRepresentationCat R H) : Type w

A morphism of point representations is a linear map whose scalar extensions intertwine every algebra-valued point action in CommAlgCat.{max u v w} R.

• toLinearMap : ↑V.toSemimoduleCat →ₗ[R] ↑W.toSemimoduleCat

  The underlying linear map.

• intertwines (A : CommAlgCat R) (x : ↑(HopfAlgebra.points A)) : LinearMap.baseChange (↑A) self.toLinearMap ∘ₗ ↑((CategoryTheory.ConcreteCategory.hom (V.representation.action A)) x) = ↑((CategoryTheory.ConcreteCategory.hom (W.representation.action A)) x) ∘ₗ LinearMap.baseChange (↑A) self.toLinearMap

  Every scalar extension of the linear map intertwines every point action.

def TauCeti.PointRepresentationCat.Hom.id (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : Hom R H V V

The identity morphism of a point representation.

Equations

• TauCeti.PointRepresentationCat.Hom.id R H V = { toLinearMap := LinearMap.id, intertwines := ⋯ }

def TauCeti.PointRepresentationCat.Hom.comp (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {U V W : PointRepresentationCat R H} (g : Hom R H V W) (f : Hom R H U V) : Hom R H U W

Composition of morphisms of point representations.

Equations

• TauCeti.PointRepresentationCat.Hom.comp R H g f = { toLinearMap := g.toLinearMap ∘ₗ f.toLinearMap, intertwines := ⋯ }

theorem TauCeti.PointRepresentationCat.Hom.ext (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} {f g : Hom R H V W} (h : f.toLinearMap = g.toLinearMap) : f = g

Morphisms of point representations are equal when their underlying linear maps are equal.

@[instance_reducible]

instance TauCeti.PointRepresentationCat.category (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.Category.{w, max (max (u + 1) (v + 1)) (w + 1)} (PointRepresentationCat R H)

Equations

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

@[instance_reducible]

instance TauCeti.PointRepresentationCat.instFunLikeHomCarrier (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} : FunLike (Hom R H V W) ↑V.toSemimoduleCat ↑W.toSemimoduleCat

Equations

• TauCeti.PointRepresentationCat.instFunLikeHomCarrier R H = { coe := fun (f : TauCeti.PointRepresentationCat.Hom R H V W) => ⇑f.toLinearMap, coe_injective := ⋯ }

@[instance_reducible]

instance TauCeti.PointRepresentationCat.concreteCategory (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.ConcreteCategory (PointRepresentationCat R H) (Hom R H)

PointRepresentationCat is concrete, with concrete morphisms the equivariant linear maps.

Equations

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

theorem TauCeti.PointRepresentationCat.hom_ext (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} {f g : V ⟶ W} (h : ∀ (v : (fun (X : PointRepresentationCat R H) => ↑X.toSemimoduleCat) V), (CategoryTheory.ConcreteCategory.hom f) v = (CategoryTheory.ConcreteCategory.hom g) v) : f = g

Two categorical morphisms of point representations are equal when they agree on every vector.

theorem TauCeti.PointRepresentationCat.hom_ext_iff {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} {f g : V ⟶ W} : f = g ↔ ∀ (v : (fun (X : PointRepresentationCat R H) => ↑X.toSemimoduleCat) V), (CategoryTheory.ConcreteCategory.hom f) v = (CategoryTheory.ConcreteCategory.hom g) v

@[simp]

theorem TauCeti.PointRepresentationCat.toLinearMap_id (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : (CategoryTheory.CategoryStruct.id V).toLinearMap = LinearMap.id

The identity morphism has the identity linear map underneath.

@[simp]

theorem TauCeti.PointRepresentationCat.toLinearMap_comp (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {U V W : PointRepresentationCat R H} (f : U ⟶ V) (g : V ⟶ W) : (CategoryTheory.CategoryStruct.comp f g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Composition of representation morphisms is composition of their underlying linear maps.

@[instance_reducible]

instance TauCeti.PointRepresentationCat.hasForgetToSemimodule (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.HasForget₂ (PointRepresentationCat R H) (SemimoduleCat R)

Forget a point representation to its underlying semimodule.

Equations

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

@[simp]

theorem TauCeti.PointRepresentationCat.forget₂_obj (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] (V : PointRepresentationCat R H) : (CategoryTheory.forget₂ (PointRepresentationCat R H) (SemimoduleCat R)).obj V = ↧↑V.toSemimoduleCat

The forgetful functor sends a point representation to its underlying semimodule.

@[simp]

theorem TauCeti.PointRepresentationCat.forget₂_map (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} (f : V ⟶ W) : (CategoryTheory.forget₂ (PointRepresentationCat R H) (SemimoduleCat R)).map f = SemimoduleCat.ofHom f.toLinearMap

The forgetful functor sends a representation morphism to its underlying linear map.

def TauCeti.PointRepresentationCat.isoToLinearEquiv (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] {V W : PointRepresentationCat R H} (i : V ≅ W) : ↑V.toSemimoduleCat ≃ₗ[R] ↑W.toSemimoduleCat

A categorical isomorphism of point representations induces the underlying linear equivalence.

Equations

• TauCeti.PointRepresentationCat.isoToLinearEquiv R H i = ((CategoryTheory.forget₂ (TauCeti.PointRepresentationCat R H) (SemimoduleCat R)).mapIso i).toLinearEquivₛ