Corestriction of comodules along a coalgebra morphism

This file proves the basic functoriality of right comodules in the coalgebra. A coalgebra morphism f : C →ₗc[R] D turns every right C-comodule into a right D-comodule by postcomposing the coaction with id ⊗ f.

This is Layer 1 infrastructure for the reductive-groups roadmap target "Comodules over a coalgebra/Hopf algebra": representations of affine group schemes are comodules over their coordinate coalgebras, and changing the coordinate coalgebra along a morphism needs this corestriction functor.

A coalgebra morphism also gives a morphism from its corestricted regular source comodule to its regular target comodule.

Main definitions

• TauCeti.Comodule.Corestrict: the induced right D-comodule structure.
• TauCeti.Comodule.corestrictHom: a comodule morphism after corestricting both sides.
• TauCeti.ComoduleCat.corestrict: the corresponding functor between bundled comodule categories.
• CoalgHom.toComoduleHom: a coalgebra morphism as a morphism of regular comodules.

References

This is the standard corestriction of comodules along a coalgebra morphism; see for example Sweedler, Hopf Algebras, Chapter 2.

def TauCeti.Comodule.corestrictCoact {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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) : M →ₗ[R] TensorProduct R M D

The coaction obtained from a right C-comodule by corestricting along a coalgebra morphism f : C →ₗc[R] D.

Equations

• TauCeti.Comodule.corestrictCoact f = TensorProduct.map LinearMap.id f.toLinearMap ∘ₗ TauCeti.Comodule.coact

@[implicit_reducible]

def TauCeti.Comodule.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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) : Comodule R D M

Corestrict a right comodule along a coalgebra morphism.

If M is a right C-comodule and f : C →ₗc[R] D, the new right D-coaction is (id ⊗ f) ∘ ρ.

Equations

• TauCeti.Comodule.Corestrict f = { coact := TauCeti.Comodule.corestrictCoact f, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.corestrict_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) : coact = corestrictCoact f

The corestricted coaction is (id ⊗ f) ∘ ρ.

@[simp]

theorem TauCeti.Comodule.corestrictCoact_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) (m : M) : (corestrictCoact f) m = (TensorProduct.map LinearMap.id f.toLinearMap) (coact m)

The corestricted coaction evaluates as (id ⊗ f) (ρ m).

@[simp]

theorem TauCeti.Comodule.corestrict_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) (m : M) : coact m = (TensorProduct.map LinearMap.id f.toLinearMap) (coact m)

The coaction of Corestrict f evaluates as (id ⊗ f) (ρ m).

@[simp]

theorem TauCeti.Comodule.corestrictCoact_id {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] : corestrictCoact (CoalgHom.id R C) = coact

Corestricting along the identity coalgebra morphism leaves the coaction unchanged.

@[simp]

theorem TauCeti.Comodule.corestrictCoact_comp {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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {E : Type u_1} [AddCommMonoid E] [Module R E] [Coalgebra R E] (f : C →ₗc[R] D) (g : D →ₗc[R] E) : corestrictCoact (g.comp f) = corestrictCoact g

Corestricted coactions compose in the coalgebra morphism.

def TauCeti.Comodule.corestrictHom {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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_2} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : C →ₗc[R] D) (g : Hom R C M N) : Hom R D M N

A morphism of C-comodules is also a morphism after corestricting both comodules along the same coalgebra morphism.

Equations

• TauCeti.Comodule.corestrictHom f g = { toLinearMap := g.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.corestrictHom_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_2} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : C →ₗc[R] D) (g : Hom R C M N) : (corestrictHom f g).toLinearMap = g.toLinearMap

Corestricting a comodule morphism does not change its underlying linear map.

@[simp]

theorem TauCeti.Comodule.corestrictHom_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_2} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : C →ₗc[R] D) (g : Hom R C M N) (m : M) : (corestrictHom f g) m = g m

Corestricting a comodule morphism does not change its underlying function.

@[simp]

theorem TauCeti.Comodule.corestrictHom_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {E : Type u_1} [AddCommMonoid E] [Module R E] [Coalgebra R E] {N : Type u_2} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : C →ₗc[R] D) (g : D →ₗc[R] E) (h : Hom R C M N) : (corestrictHom (g.comp f) h).toLinearMap = (corestrictHom g (corestrictHom f h)).toLinearMap

Corestriction of morphisms is unchanged on underlying linear maps under composition of coalgebra morphisms.

@[simp]

theorem TauCeti.Comodule.corestrictHom_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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {E : Type u_1} [AddCommMonoid E] [Module R E] [Coalgebra R E] {N : Type u_2} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : C →ₗc[R] D) (g : D →ₗc[R] E) (h : Hom R C M N) (m : M) : (corestrictHom (g.comp f) h) m = (corestrictHom g (corestrictHom f h)) m

Corestriction of morphisms is unchanged on elements under composition of coalgebra morphisms.

@[simp]

theorem TauCeti.Comodule.corestrictHom_id {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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) : corestrictHom f (Hom.id R C M) = Hom.id R D M

Corestriction sends identity morphisms to identity morphisms.

@[simp]

theorem TauCeti.Comodule.corestrictHom_comp {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] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_2} [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_3} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : C →ₗc[R] D) (g : Hom R C M N) (h : Hom R C N P) : corestrictHom f (h.comp g) = (corestrictHom f h).comp (corestrictHom f g)

Corestriction preserves composition of comodule morphisms.

def TauCeti.ComoduleCat.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 (ComoduleCat R C) (ComoduleCat R D)

Corestriction of bundled right comodules along a coalgebra morphism.

Equations

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

@[simp]

theorem TauCeti.ComoduleCat.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 : ComoduleCat R C) : (corestrict f).obj M = of R D ↑M.toSemimoduleCat

The corestriction functor leaves the underlying type of an object unchanged.

@[simp]

theorem TauCeti.ComoduleCat.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 : ComoduleCat R C} (g : M ⟶ N) : ((corestrict f).map g).toLinearMap = g.toLinearMap

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

@[simp]

theorem TauCeti.ComoduleCat.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 : ComoduleCat R C} (g : M ⟶ N) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom ((corestrict f).map g)) m = (CategoryTheory.ConcreteCategory.hom g) m

The corestriction functor leaves the underlying function of a morphism unchanged.

theorem TauCeti.ComoduleCat.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 u_1} [AddCommMonoid E] [Module R E] [Coalgebra R E] (f : C →ₗc[R] D) (g : D →ₗc[R] E) {M N : ComoduleCat R C} (h : M ⟶ N) : ((corestrict (g.comp f)).map h).toLinearMap = ((corestrict g).map ((corestrict f).map h)).toLinearMap

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

@[simp]

theorem TauCeti.ComoduleCat.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 u_1} [AddCommMonoid E] [Module R E] [Coalgebra R E] (f : C →ₗc[R] D) (g : D →ₗc[R] E) {M N : ComoduleCat R C} (h : M ⟶ N) (m : ↑M.toSemimoduleCat) : (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.

def CoalgHom.toComoduleHom {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) : TauCeti.Comodule.Hom R D C D

A coalgebra morphism as a morphism from its corestricted regular source comodule to its regular target comodule.

Equations

• f.toComoduleHom = { toLinearMap := f.toLinearMap, map_coact := ⋯ }

@[simp]

theorem CoalgHom.toComoduleHom_toLinearMap {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) : f.toComoduleHom.toLinearMap = f.toLinearMap

The underlying linear map of the regular-comodule morphism is the coalgebra map.

@[simp]

theorem CoalgHom.toComoduleHom_apply {R : Type u} {C : Type v} {D : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] (f : C →ₗc[R] D) (c : C) : f.toComoduleHom c = f c

The regular-comodule morphism evaluates as the coalgebra map.