The induced comodule on a subcomodule

This file equips a subcomodule with its inherited right-comodule structure. The definition is made under the flatness hypothesis on the coalgebra: flatness makes N ⊗ C → M ⊗ C injective for the subtype map of a subcomodule N ≤ M, so the ambient coaction has a unique lift to N ⊗ C.

This is Layer 1 infrastructure for the reductive-groups roadmap target "Comodules over a coalgebra/Hopf algebra": finite-dimensional subcomodules and categorical kernels need subcomodules to be usable as comodules in their own right.

Main declarations

• TauCeti.Subcomodule.inducedCoact: the coaction on the subtype of a subcomodule.
• TauCeti.Subcomodule.instComodule: the induced right-comodule structure.
• TauCeti.Subcomodule.coact_coe_eq_tmul_one: a fixed vector of a subcomodule is fixed in the ambient comodule.
• TauCeti.Subcomodule.subtype: the inclusion as a comodule morphism.
• TauCeti.Comodule.Hom.codRestrict: a comodule morphism corestricted to a subcomodule containing its image.

References

This is the standard inherited comodule structure on a subcomodule; see Sweedler, Hopf Algebras, Chapter 2. The formalization uses Mathlib's LinearMap.codRestrictOfInjective and flatness preservation of injective maps under tensor product.

noncomputable def TauCeti.Subcomodule.inducedCoact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : ↥N →ₗ[R] TensorProduct R (↥N) C

The coaction induced on the subtype of a subcomodule.

It is the unique lift of the ambient coaction along N ⊗ C → M ⊗ C.

Equations

• N.inducedCoact = (TauCeti.Comodule.coact ∘ₗ SMulMemClass.subtype N).codRestrictOfInjective (LinearMap.rTensor C (SMulMemClass.subtype N)) ⋯ ⋯

@[simp]

theorem TauCeti.Subcomodule.subtype_rTensor_inducedCoact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) (n : ↥N) : (LinearMap.rTensor C (SMulMemClass.subtype N)) (N.inducedCoact n) = Comodule.coact ↑n

The induced coaction, included back into M ⊗ C, is the ambient coaction.

@[simp]

theorem TauCeti.Subcomodule.subtype_rTensor_comp_inducedCoact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : LinearMap.rTensor C (SMulMemClass.subtype N) ∘ₗ N.inducedCoact = Comodule.coact ∘ₗ SMulMemClass.subtype N

The induced coaction included into the ambient tensor product, as an equality of linear maps.

@[instance_reducible]

noncomputable instance TauCeti.Subcomodule.instComodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Comodule R C ↥N

The subtype of a subcomodule carries the inherited right-comodule structure.

Equations

• N.instComodule = { coact := N.inducedCoact, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Subcomodule.induced_coact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Comodule.coact = N.inducedCoact

The inherited coaction on a subcomodule is Subcomodule.inducedCoact.

theorem TauCeti.Subcomodule.subtype_rTensor_coact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) (n : ↥N) : (LinearMap.rTensor C (SMulMemClass.subtype N)) (Comodule.coact n) = Comodule.coact ↑n

The inherited coaction, included back into M ⊗ C, is the ambient coaction.

theorem TauCeti.Subcomodule.coact_coe_eq_tmul_one {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) [One C] {n : ↥N} (hn : Comodule.coact n = n ⊗ₜ[R] 1) : Comodule.coact ↑n = ↑n ⊗ₜ[R] 1

A vector of a subcomodule whose inherited coaction is v ↦ v ⊗ 1 is fixed by the ambient coaction too.

noncomputable def TauCeti.Subcomodule.subtype {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Comodule.Hom R C (↥N) M

The subtype map of a subcomodule as a morphism of right comodules.

Equations

• N.subtype = { toLinearMap := SMulMemClass.subtype N, map_coact := ⋯ }

@[simp]

theorem TauCeti.Subcomodule.subtype_toLinearMap {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : N.subtype.toLinearMap = SMulMemClass.subtype N

The underlying linear map of the subcomodule inclusion is the linear inclusion.

@[simp]

theorem TauCeti.Subcomodule.subtype_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) (n : ↥N) : N.subtype n = ↑n

The subcomodule inclusion acts as the underlying subtype coercion.

noncomputable def TauCeti.Comodule.Hom.codRestrict {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (P : Subcomodule R C N) (h : ∀ (m : M), f m ∈ P) : Hom R C M ↥P

Corestrict a comodule morphism to a subcomodule containing its image.

Equations

• f.codRestrict P h = { toFun := fun (m : M) => ⟨f m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.codRestrict_toLinearMap {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (P : Subcomodule R C N) (h : ∀ (m : M), f m ∈ P) : (f.codRestrict P h).toLinearMap = LinearMap.codRestrict P.toSubmodule f.toLinearMap h

The underlying linear map of a corestricted comodule morphism is the ordinary linear corestriction.

@[simp]

theorem TauCeti.Comodule.Hom.codRestrict_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (P : Subcomodule R C N) (h : ∀ (m : M), f m ∈ P) (m : M) : ↑((f.codRestrict P h) m) = f m

Corestricting a comodule morphism changes only its codomain.

@[simp]

theorem TauCeti.Comodule.Hom.subtype_comp_codRestrict {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (P : Subcomodule R C N) (h : ∀ (m : M), f m ∈ P) : P.subtype.comp (f.codRestrict P h) = f

Composing a corestricted comodule morphism with the subcomodule inclusion recovers the original morphism.