Documentation

TauCeti.Algebra.Coalgebra.Comodule.Finite.Corestrict

Corestriction of finitely generated comodules #

This file lifts corestriction along a coalgebra morphism from all right comodules to the full subcategory of finitely generated right comodules. Since corestriction changes only the target coalgebra of the coaction and leaves the underlying module unchanged, finite generation is preserved automatically.

This is Layer 1 infrastructure for the reductive-groups roadmap target "Comodules over a coalgebra/Hopf algebra": the finitely generated comodule category must remain available when the coordinate coalgebra is changed along a coalgebra morphism.

Main definitions #

References #

This is the standard corestriction of comodules along a coalgebra morphism; see Sweedler, Hopf Algebras, Chapter 2. The categorical lift reuses Mathlib's ObjectProperty.FullSubcategory API.

source
def TauCeti.FGComoduleCat.corestrict {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) :
CategoryTheory.Functor (FGComoduleCat R C) (FGComoduleCat R D)

Corestriction of finitely generated right comodules along a coalgebra morphism.

The underlying module is unchanged, so the finite-generation proof is inherited from the source object.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_obj_obj {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (M : FGComoduleCat R C) :
    ((corestrict f).obj M).obj = (ComoduleCat.corestrict f).obj M.obj

    Corestriction on finitely generated comodules is corestriction on the ambient comodule.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_obj_coe {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (M : FGComoduleCat R C) :
    ↑((corestrict f).obj M) = ↑M

    Corestriction leaves the underlying type of a finitely generated comodule unchanged.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_obj_coact {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (M : FGComoduleCat R C) :
    Comodule.coact = Comodule.corestrictCoact f

    The coaction after corestricting a finitely generated comodule is (id ⊗ f) ∘ ρ.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_obj_coact_apply {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (M : FGComoduleCat R C) (m : ↑M) :
    Comodule.coact m = (TensorProduct.map LinearMap.id f.toLinearMap) (Comodule.coact m)

    The coaction after corestricting a finitely generated comodule evaluates as (id ⊗ f) (ρ m).

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_map_hom {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {M N : FGComoduleCat R C} (g : M ⟶ N) :
    ((corestrict f).map g).hom = (ComoduleCat.corestrict f).map g.hom

    Corestriction on finitely generated morphisms is corestriction on ambient comodule morphisms.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_map_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {M N : FGComoduleCat R C} (g : M ⟶ N) :
    ((corestrict f).map g).hom.toLinearMap = g.hom.toLinearMap

    Corestriction leaves the underlying linear map of a finitely generated comodule morphism unchanged.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_map_apply {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {M N : FGComoduleCat R C} (g : M ⟶ N) (m : ↑M) :
    (CategoryTheory.ConcreteCategory.hom ((corestrict f).map g)) m = (CategoryTheory.ConcreteCategory.hom g) m

    Corestriction leaves the underlying function of a finitely generated comodule morphism unchanged.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.incl_corestrict_obj {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (M : FGComoduleCat R C) :
    incl.obj ((corestrict f).obj M) = (ComoduleCat.corestrict f).obj (incl.obj M)

    Corestriction of finitely generated comodules commutes with the inclusion into all comodules on objects.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.incl_corestrict_map {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {M N : FGComoduleCat R C} (g : M ⟶ N) :
    incl.map ((corestrict f).map g) = (ComoduleCat.corestrict f).map (incl.map g)

    Corestriction of finitely generated comodules commutes with the inclusion into all comodules on morphisms.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_corestrict_obj {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (M : FGComoduleCat R C) :
    (CategoryTheory.forget₂ (FGComoduleCat R D) (SemimoduleCat R)).obj ((corestrict f).obj M) = (CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).obj M

    Corestriction leaves the underlying semimodule object unchanged.

    source
    theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_corestrict_map {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) {M N : FGComoduleCat R C} (g : M ⟶ N) :
    (CategoryTheory.forget₂ (FGComoduleCat R D) (SemimoduleCat R)).map ((corestrict f).map g) = (CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).map g

    Corestriction leaves the underlying semimodule morphism unchanged.

    source
    theorem TauCeti.FGComoduleCat.corestrict_obj_coact_id {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : FGComoduleCat R C) :
    Comodule.coact = Comodule.coact

    Corestricting finitely generated comodules along the identity coalgebra morphism leaves the coaction unchanged.

    source
    theorem TauCeti.FGComoduleCat.corestrict_map_comp_coalg_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {E : Type y} [AddCommMonoid E] [Module R E] [Coalgebra R E] (f : C →ₗc[R] D) (g : D →ₗc[R] E) {M N : FGComoduleCat R C} (h : M ⟶ N) :
    ((corestrict (g.comp f)).map h).hom.toLinearMap = ((corestrict g).map ((corestrict f).map h)).hom.toLinearMap

    Corestriction functors compose in the coalgebra morphism on underlying linear maps.

    source
    @[simp]
    theorem TauCeti.FGComoduleCat.corestrict_map_comp_coalg_apply {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {E : Type y} [AddCommMonoid E] [Module R E] [Coalgebra R E] (f : C →ₗc[R] D) (g : D →ₗc[R] E) {M N : FGComoduleCat R C} (h : M ⟶ N) (m : ↑M) :
    (CategoryTheory.ConcreteCategory.hom ((corestrict (g.comp f)).map h)) m = (CategoryTheory.ConcreteCategory.hom ((corestrict g).map ((corestrict f).map h))) m

    Corestriction functors compose in the coalgebra morphism on elements.