Documentation

TauCeti.Algebra.Coalgebra.Comodule.Finite.Basic

Finitely generated comodules #

This file packages finitely generated right comodules over a coalgebra as a full subcategory of ComoduleCat. An object of FGComoduleCat R C is a right C-comodule whose underlying R-module is finitely generated; over a field this is the finite-dimensional comodule category requested by the reductive-groups roadmap.

This is a small Layer 1 prerequisite for the finite-dimensional representation category of an affine group scheme: later tensor products, duals, matrix coefficients, and Tannakian reconstruction should be built on this full subcategory rather than on all comodules.

Main definitions #

TauCeti.ComoduleCat.isFG: the finite-generation object property on ComoduleCat.
TauCeti.ComoduleCat.isFG_isClosedUnderIsomorphisms: finite generation is invariant under comodule isomorphisms.
TauCeti.FGComoduleCat: finitely generated right comodules as a full subcategory.
TauCeti.FGComoduleCat.incl: the inclusion into all comodules.
forget₂ (FGComoduleCat R C) (ComoduleCat R C): the forgetful functor to all comodules.
forget₂ (FGComoduleCat R C) (SemimoduleCat R): the forgetful functor to semimodules.
TauCeti.FGComoduleCat.of: build a finitely generated bundled comodule from unbundled data.
TauCeti.FGComoduleCat.ofHom: lift an unbundled comodule morphism between finitely generated comodules.
TauCeti.FGComoduleCat.isoOfLinearEquiv: build an isomorphism from a coaction-compatible linear equivalence.
TauCeti.FGComoduleCat.isZero_zero: FGComoduleCat.zero is a zero object.
HasZeroObject (FGComoduleCat R C).

References #

This supplies the finite-dimensional-category part of ReductiveGroups/README.md in TauCetiRoadmap, Layer 1 target "Comodules over a coalgebra/Hopf algebra". The construction follows Mathlib's FGModuleCat pattern: finite objects are a full subcategory defined by the object property Module.Finite.

def TauCeti.ComoduleCat.isFG (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

CategoryTheory.ObjectProperty (ComoduleCat R C)

Finite-generation as an object property on the category of right comodules.

Equations

TauCeti.ComoduleCat.isFG R C M = Module.Finite R ↑M.toSemimoduleCat

Instances For

theorem TauCeti.ComoduleCat.isFG_iff (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : ComoduleCat R C) :

isFG R C M ↔ Module.Finite R ↑M.toSemimoduleCat

The finitely generated comodule property is exactly finite generation of the underlying module.

instance TauCeti.ComoduleCat.isFG_isClosedUnderIsomorphisms (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

(isFG R C).IsClosedUnderIsomorphisms

Finite generation of a comodule is preserved by comodule isomorphisms.

theorem TauCeti.ComoduleCat.finite_zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

Module.Finite R ↑(zero R C).toSemimoduleCat

The zero comodule is finitely generated.

instance TauCeti.ComoduleCat.isFG_containsZero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

(isFG R C).ContainsZero

The finite-generation property contains the zero comodule.

@[reducible, inline]

abbrev TauCeti.FGComoduleCat (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

Type (max (max u v) (w + 1))

The category of finitely generated right comodules over a fixed coalgebra.

For a field base, this is the category of finite-dimensional right comodules.

Equations

TauCeti.FGComoduleCat R C = (TauCeti.ComoduleCat.isFG R C).FullSubcategory

Instances For

@[reducible]

def TauCeti.FGComoduleCat.carrier {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

The underlying type of a finitely generated comodule.

Equations

↑M = ↑M.obj.toSemimoduleCat

Instances For

@[instance_reducible]

instance TauCeti.FGComoduleCat.instCoeSortType {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] :

CoeSort (FGComoduleCat R C) (Type w)

Equations

TauCeti.FGComoduleCat.instCoeSortType = { coe := TauCeti.FGComoduleCat.carrier }

@[instance_reducible]

instance TauCeti.FGComoduleCat.instAddCommMonoidCarrier {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

AddCommMonoid ↑M

Equations

M.instAddCommMonoidCarrier = TauCeti.ComoduleCat.instAddCommMonoidCarrier R C M.obj

@[instance_reducible]

instance TauCeti.FGComoduleCat.instModuleCarrier {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

Module R ↑M

Equations

M.instModuleCarrier = TauCeti.ComoduleCat.instModuleCarrier R C M.obj

@[instance_reducible]

instance TauCeti.FGComoduleCat.instComoduleCarrier {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

Comodule R C ↑M

Equations

M.instComoduleCarrier = M.obj.instComodule

instance TauCeti.FGComoduleCat.instFiniteCarrier {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

Module.Finite R ↑M

The underlying module of a finitely generated comodule is finitely generated.

@[reducible, inline]

abbrev TauCeti.FGComoduleCat.incl {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] :

CategoryTheory.Functor (FGComoduleCat R C) (ComoduleCat R C)

The inclusion from finitely generated comodules to all comodules.

Equations

TauCeti.FGComoduleCat.incl = (TauCeti.ComoduleCat.isFG R C).ι

Instances For

@[instance_reducible]

instance TauCeti.FGComoduleCat.hasForgetToSemimoduleCat {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] :

CategoryTheory.HasForget₂ (FGComoduleCat R C) (SemimoduleCat R)

Forget a finitely generated comodule to its underlying semimodule.

Equations

TauCeti.FGComoduleCat.hasForgetToSemimoduleCat = CategoryTheory.HasForget₂.trans (TauCeti.FGComoduleCat R C) (TauCeti.ComoduleCat R C) (SemimoduleCat R)

@[simp]

theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_obj {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

(CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).obj M = (CategoryTheory.forget₂ (ComoduleCat R C) (SemimoduleCat R)).obj M.obj

Forgetting a finitely generated comodule to semimodules agrees with forgetting its ambient comodule.

@[simp]

theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_map {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f : M ⟶ N) :

(CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).map f = (CategoryTheory.forget₂ (ComoduleCat R C) (SemimoduleCat R)).map f.hom

Forgetting a finitely generated comodule morphism to semimodules agrees with forgetting its ambient comodule morphism.

@[reducible, inline]

abbrev TauCeti.FGComoduleCat.of {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] :

FGComoduleCat R C

Lift an unbundled finitely generated right comodule to FGComoduleCat.

Equations

TauCeti.FGComoduleCat.of M = { obj := TauCeti.ComoduleCat.of R C M, property := inst✝ }

Instances For

@[simp]

theorem TauCeti.FGComoduleCat.of_obj {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] :

(of M).obj = ComoduleCat.of R C M

The object of ComoduleCat underlying FGComoduleCat.of is ComoduleCat.of.

@[simp]

theorem TauCeti.FGComoduleCat.of_coact {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] :

Comodule.coact = Comodule.coact

The coaction on FGComoduleCat.of is the original unbundled coaction.

@[reducible, inline]

abbrev TauCeti.FGComoduleCat.ofHom {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] [AddCommMonoid N] [Module R N] [Comodule R C N] [Module.Finite R N] (f : Comodule.Hom R C M N) :

Typecheck an unbundled comodule morphism between finitely generated comodules as a categorical morphism in FGComoduleCat.

Equations

TauCeti.FGComoduleCat.ofHom f = CategoryTheory.ObjectProperty.homMk (TauCeti.ComoduleCat.ofHom R C f)

Instances For

@[simp]

theorem TauCeti.FGComoduleCat.ofHom_hom {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] [AddCommMonoid N] [Module R N] [Comodule R C N] [Module.Finite R N] (f : Comodule.Hom R C M N) :

(ofHom f).hom = ComoduleCat.ofHom R C f

Turning an unbundled comodule morphism into an FGComoduleCat morphism and projecting to the ambient comodule category recovers the original bundled morphism.

@[simp]

theorem TauCeti.FGComoduleCat.ofHom_id {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] :

ofHom (Comodule.Hom.id R C M) = CategoryTheory.CategoryStruct.id (of M)

The categorical identity on a finitely generated bundled comodule is the bundled form of the identity comodule morphism.

@[simp]

theorem TauCeti.FGComoduleCat.ofHom_comp {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] [AddCommMonoid N] [Module R N] [Comodule R C N] [Module.Finite R N] [AddCommMonoid P] [Module R P] [Comodule R C P] [Module.Finite R P] (f : Comodule.Hom R C M N) (g : Comodule.Hom R C N P) :

ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

Categorical composition of finitely generated bundled comodule morphisms is the bundled form of composition of comodule morphisms.

@[simp]

theorem TauCeti.FGComoduleCat.ofHom_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Finite R M] [AddCommMonoid N] [Module R N] [Comodule R C N] [Module.Finite R N] (f : Comodule.Hom R C M N) (m : M) :

(CategoryTheory.ConcreteCategory.hom (ofHom f)) m = f m

The FGComoduleCat morphism induced by an unbundled morphism applies as that morphism.

def TauCeti.FGComoduleCat.isoOfLinearEquiv {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (e : ↑M ≃ₗ[R] ↑N) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) :

M ≅ N

Build an isomorphism of finitely generated comodules from a linear equivalence of the underlying modules whose forward map respects the coactions.

Compatibility of the inverse is automatic, and is supplied by TauCeti.ComoduleCat.isoOfLinearEquiv; being a full subcategory, FGComoduleCat then inherits the isomorphism from ComoduleCat.

Equations

TauCeti.FGComoduleCat.isoOfLinearEquiv e h = (TauCeti.ComoduleCat.isFG R C).isoMk (TauCeti.ComoduleCat.isoOfLinearEquiv R C e h)

Instances For

@[simp]

theorem TauCeti.FGComoduleCat.isoOfLinearEquiv_hom_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (e : ↑M ≃ₗ[R] ↑N) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) :

(isoOfLinearEquiv e h).hom.hom.toLinearMap = ↑e

The forward morphism of FGComoduleCat.isoOfLinearEquiv has the original linear equivalence underneath.

@[simp]

theorem TauCeti.FGComoduleCat.isoOfLinearEquiv_inv_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (e : ↑M ≃ₗ[R] ↑N) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) :

(isoOfLinearEquiv e h).inv.hom.toLinearMap = ↑e.symm

The inverse morphism of FGComoduleCat.isoOfLinearEquiv has the inverse linear equivalence underneath.

@[simp]

theorem TauCeti.FGComoduleCat.isoOfLinearEquiv_hom_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (e : ↑M ≃ₗ[R] ↑N) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) (m : ↑M) :

(CategoryTheory.ConcreteCategory.hom (isoOfLinearEquiv e h).hom) m = e m

The forward map of FGComoduleCat.isoOfLinearEquiv is the given linear equivalence.

@[simp]

theorem TauCeti.FGComoduleCat.isoOfLinearEquiv_inv_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (e : ↑M ≃ₗ[R] ↑N) (h : TensorProduct.map (↑e) LinearMap.id ∘ₗ Comodule.coact = Comodule.coact ∘ₗ ↑e) (n : ↑N) :

(CategoryTheory.ConcreteCategory.hom (isoOfLinearEquiv e h).inv) n = e.symm n

The inverse map of FGComoduleCat.isoOfLinearEquiv is the inverse linear equivalence.

def TauCeti.FGComoduleCat.zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

FGComoduleCat R C

The bundled finitely generated zero right comodule.

Equations

TauCeti.FGComoduleCat.zero R C = { obj := TauCeti.ComoduleCat.zero R C, property := ⋯ }

Instances For

@[simp]

theorem TauCeti.FGComoduleCat.zero_obj (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

(zero R C).obj = ComoduleCat.zero R C

The ambient comodule underlying the finitely generated zero comodule is the zero comodule.

theorem TauCeti.FGComoduleCat.isZero_zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] :

CategoryTheory.Limits.IsZero (zero R C)

The named finitely generated zero comodule is a zero object.

theorem TauCeti.FGComoduleCat.zero_hom_eq_zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) (f : zero R C ⟶ M) :

f = 0

Any morphism from the named finitely generated zero comodule is zero.

theorem TauCeti.FGComoduleCat.hom_zero_eq_zero (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) (f : M ⟶ zero R C) :

f = 0

Any morphism to the named finitely generated zero comodule is zero.

@[simp]

theorem TauCeti.FGComoduleCat.isZero_zero_to (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

⋯.to_ M = 0

The canonical morphism out of the named finitely generated zero comodule is the zero morphism.

@[simp]

theorem TauCeti.FGComoduleCat.isZero_zero_from (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

⋯.from_ M = 0

The canonical morphism into the named finitely generated zero comodule is the zero morphism.

theorem TauCeti.FGComoduleCat.zero_hom_ext (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : FGComoduleCat R C} (f g : zero R C ⟶ M) :

f = g

Morphisms from the named finitely generated zero comodule are unique.

theorem TauCeti.FGComoduleCat.zero_hom_ext_iff {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : FGComoduleCat R C} {f g : zero R C ⟶ M} :

theorem TauCeti.FGComoduleCat.hom_zero_ext (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : FGComoduleCat R C} (f g : M ⟶ zero R C) :

f = g

Morphisms to the named finitely generated zero comodule are unique.

theorem TauCeti.FGComoduleCat.hom_zero_ext_iff {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : FGComoduleCat R C} {f g : M ⟶ zero R C} :

@[instance_reducible]

instance TauCeti.FGComoduleCat.instAddCommGroupCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :

AddCommGroup ↑M

Equations

M.instAddCommGroupCarrier = Module.addCommMonoidToAddCommGroup R