Subcomodules #
This file defines subcomodules of a right comodule as submodules whose elements have
coaction in the tensor product of the submodule with the coalgebra. It is deliberately a
lightweight predicate-style API: over a general commutative semiring, the map
N ⊗ C → M ⊗ C need not be known injective, so the induced comodule structure on N is
not registered here.
Finite generation of a subcomodule is expressed by Module.Finite R N.toSubmodule;
images under comodule morphisms preserve this property.
Main definitions #
TauCeti.Subcomodule: a submodule stable under the coaction.TauCeti.Subcomodule.toSubmodule: the underlying submodule.TauCeti.Subcomodule.finite: subcomodules of noetherian modules are finite.TauCeti.Subcomodule.rid_lTensor_coact_mem: a subcomodule is stable under contracting the coaction against a linear functional on the coalgebra.⊤and⊥: the full and zero subcomodules, which bound the order of subcomodules.TauCeti.Subcomodule.toSubmodule_eq_topandTauCeti.Subcomodule.toSubmodule_eq_bot: the underlying submodule detects the extreme subcomodules.TauCeti.Subcomodule.ne_bot_iff: a subcomodule is nonzero exactly when it contains a nonzero vector.TauCeti.Subcomodule.isSimpleOrder_of_transitive: a family of maps that preserves every subcomodule and acts transitively on nonzero vectors makes the subcomodule lattice simple.TauCeti.Subcomodule.map: the image of a subcomodule under a comodule morphism.TauCeti.Subcomodule.map_finite: images preserve finite generation of the underlying submodule.TauCeti.Comodule.Hom.range: the image subcomodule of a comodule morphism.TauCeti.Comodule.Hom.range_finite: ranges of morphisms out of finite modules are finite.
References #
This follows the standard definition of a subcomodule: N ≤ M satisfies
ρ(N) ⊆ N ⊗ C. See Sweedler, Hopf Algebras, Chapter 2.
The lightweight range-based API follows the pattern of TauCeti.Subcoalgebra.
structure
TauCeti.Subcomodule
(R : Type u)
(C : Type v)
(M : Type w)
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
Type w
A subcomodule of a right C-comodule M.
It is an R-submodule carrier such that the coaction of every element of carrier lies in
the range of carrier ⊗ C → M ⊗ C.
- carrier : Submodule R M
The underlying submodule of a subcomodule.
- coact_mem' ⦃m : M⦄ : m ∈ self.carrier → Comodule.coact m ∈ (TensorProduct.map self.carrier.subtype LinearMap.id).range
The coaction of an element of the submodule lies in its tensor product with
C.
Instances For
@[instance_reducible]
instance
TauCeti.Subcomodule.instSetLike
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
SetLike (Subcomodule R C M) M
Equations
- TauCeti.Subcomodule.instSetLike = { coe := fun (N : TauCeti.Subcomodule R C M) => ↑N.carrier, coe_injective := ⋯ }
instance
TauCeti.Subcomodule.instAddSubmonoidClass
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
AddSubmonoidClass (Subcomodule R C M) M
instance
TauCeti.Subcomodule.instSMulMemClass
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
SMulMemClass (Subcomodule R C M) R M
@[instance_reducible]
instance
TauCeti.Subcomodule.instPartialOrder
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
PartialOrder (Subcomodule R C M)
Equations
def
TauCeti.Subcomodule.toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Subcomodule R C M)
:
Submodule R M
The underlying submodule of a subcomodule.
Equations
- N.toSubmodule = N.carrier
Instances For
@[simp]
theorem
TauCeti.Subcomodule.mem_carrier
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Subcomodule R C M}
{m : M}
:
@[simp]
theorem
TauCeti.Subcomodule.mem_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Subcomodule R C M}
{m : M}
:
theorem
TauCeti.Subcomodule.toSubmodule_carrier
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Subcomodule R C M)
:
theorem
TauCeti.Subcomodule.finite
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Subcomodule R C M)
[IsNoetherian R M]
:
Module.Finite R ↥N.toSubmodule
A subcomodule of a noetherian module is finitely generated as an R-module.
theorem
TauCeti.Subcomodule.le_def
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N P : Subcomodule R C M}
:
theorem
TauCeti.Subcomodule.toSubmodule_le_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N P : Subcomodule R C M}
:
theorem
TauCeti.Subcomodule.ext
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N P : Subcomodule R C M}
(h : ∀ (m : M), m ∈ N ↔ m ∈ P)
:
Two subcomodules are equal when they contain the same elements.
theorem
TauCeti.Subcomodule.ext_iff
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N P : Subcomodule R C M}
:
theorem
TauCeti.Subcomodule.coact_mem
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Subcomodule R C M)
{m : M}
(hm : m ∈ N)
:
The coaction of an element of a subcomodule belongs to its tensor product with the coalgebra.
theorem
TauCeti.Subcomodule.rid_lTensor_coact_mem
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Subcomodule R C M)
(f : C →ₗ[R] R)
{m : M}
(hm : m ∈ N)
:
A subcomodule is stable under contracting the coaction against a linear functional on the coalgebra.
For a comodule over a Hopf algebra the contractions along the algebra homomorphisms C →ₐ[R] R
are the actions of the R-valued points of the represented affine group, so this is the
statement that a subcomodule is a subrepresentation.
def
TauCeti.Subcomodule.ofSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Submodule R M)
(hN : ∀ ⦃m : M⦄, m ∈ N → Comodule.coact m ∈ (TensorProduct.map N.subtype LinearMap.id).range)
:
Subcomodule R C M
Constructor from a submodule and the tensor-product stability condition.
Equations
- TauCeti.Subcomodule.ofSubmodule N hN = { carrier := N, coact_mem' := hN }
Instances For
@[simp]
theorem
TauCeti.Subcomodule.ofSubmodule_carrier
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(N : Submodule R M)
(hN : ∀ ⦃m : M⦄, m ∈ N → Comodule.coact m ∈ (TensorProduct.map N.subtype LinearMap.id).range)
:
@[simp]
theorem
TauCeti.Subcomodule.mem_ofSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Submodule R M}
{hN : ∀ ⦃m : M⦄, m ∈ N → Comodule.coact m ∈ (TensorProduct.map N.subtype LinearMap.id).range}
{m : M}
:
theorem
TauCeti.Subcomodule.coact_mem_tensor_top
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(m : M)
:
The coaction of any element lies in the tensor product of the top submodule with C,
because the inclusion of ⊤ is surjective.
@[instance_reducible]
instance
TauCeti.Subcomodule.instTop
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
Top (Subcomodule R C M)
The full module as a subcomodule.
@[simp]
theorem
TauCeti.Subcomodule.top_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
@[simp]
theorem
TauCeti.Subcomodule.mem_top
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(m : M)
:
@[instance_reducible]
instance
TauCeti.Subcomodule.instOrderTop
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
OrderTop (Subcomodule R C M)
Equations
- TauCeti.Subcomodule.instOrderTop = { toTop := TauCeti.Subcomodule.instTop, le_top := ⋯ }
@[instance_reducible]
instance
TauCeti.Subcomodule.instBot
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
Bot (Subcomodule R C M)
The zero submodule as a subcomodule.
@[simp]
theorem
TauCeti.Subcomodule.bot_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
@[simp]
theorem
TauCeti.Subcomodule.mem_bot
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{m : M}
:
@[instance_reducible]
instance
TauCeti.Subcomodule.instOrderBot
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
OrderBot (Subcomodule R C M)
The zero subcomodule is contained in every subcomodule.
Equations
- TauCeti.Subcomodule.instOrderBot = { toBot := TauCeti.Subcomodule.instBot, bot_le := ⋯ }
@[instance_reducible]
instance
TauCeti.Subcomodule.instBoundedOrder
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
:
BoundedOrder (Subcomodule R C M)
The zero and full subcomodules bound the order of subcomodules.
Equations
- TauCeti.Subcomodule.instBoundedOrder = { toOrderTop := TauCeti.Subcomodule.instOrderTop, toOrderBot := TauCeti.Subcomodule.instOrderBot }
@[simp]
theorem
TauCeti.Subcomodule.toSubmodule_eq_top
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Subcomodule R C M}
:
The underlying submodule detects the full subcomodule.
@[simp]
theorem
TauCeti.Subcomodule.toSubmodule_eq_bot
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Subcomodule R C M}
:
The underlying submodule detects the zero subcomodule.
theorem
TauCeti.Subcomodule.ne_bot_iff
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Subcomodule R C M}
:
A subcomodule is nonzero exactly when it contains a nonzero vector.
theorem
TauCeti.Subcomodule.isSimpleOrder_of_transitive
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{G : Type x}
(v₀ : M)
(hv₀ : v₀ ≠ 0)
(act : G → M → M)
(htrans : ∀ {v w : M}, v ≠ 0 → w ≠ 0 → ∃ (g : G), act g w = v)
(hmem : ∀ (N : Subcomodule R C M) (g : G) {w : M}, w ∈ N → act g w ∈ N)
:
IsSimpleOrder (Subcomodule R C M)
If a family of maps preserves every subcomodule and acts transitively on nonzero vectors, then the subcomodule lattice is simple.
def
TauCeti.Subcomodule.map
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(A : Subcomodule R C M)
(f : Comodule.Hom R C M N)
:
Subcomodule R C N
The image of a subcomodule under a comodule morphism.
Equations
- A.map f = { carrier := Submodule.map f.toLinearMap A.carrier, coact_mem' := ⋯ }
Instances For
@[simp]
theorem
TauCeti.Subcomodule.map_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(A : Subcomodule R C M)
(f : Comodule.Hom R C M N)
:
The underlying submodule of the image subcomodule is the image of the underlying submodule.
theorem
TauCeti.Subcomodule.map_finite
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Comodule.Hom R C M N)
(A : Subcomodule R C M)
[Module.Finite R ↥A.toSubmodule]
:
Module.Finite R ↥(A.map f).toSubmodule
The image of a finitely generated subcomodule is finitely generated as an R-module.
theorem
TauCeti.Subcomodule.mem_map
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
{A : Subcomodule R C M}
{f : Comodule.Hom R C M N}
{n : N}
:
Membership in the image subcomodule.
theorem
TauCeti.Subcomodule.mem_map_of_mem
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Comodule.Hom R C M N)
{A : Subcomodule R C M}
{m : M}
(hm : m ∈ A)
:
The image of an element of a subcomodule belongs to the image subcomodule.
theorem
TauCeti.Subcomodule.map_le_iff
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
{A : Subcomodule R C M}
{f : Comodule.Hom R C M N}
{B : Subcomodule R C N}
:
The image subcomodule is contained in B exactly when each image of an element of the
source subcomodule belongs to B.
theorem
TauCeti.Subcomodule.map_mono
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Comodule.Hom R C M N)
{A B : Subcomodule R C M}
(hAB : A ≤ B)
:
The image construction is monotone in the source subcomodule.
@[simp]
theorem
TauCeti.Subcomodule.map_bot
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Comodule.Hom R C M N)
:
The image of the bottom subcomodule is bottom.
@[simp]
theorem
TauCeti.Subcomodule.map_top_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Comodule.Hom R C M N)
:
The image of the top subcomodule is the range of the comodule morphism as a submodule.
@[simp]
theorem
TauCeti.Subcomodule.map_id
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(A : Subcomodule R C M)
:
The identity comodule morphism leaves a subcomodule unchanged.
@[simp]
theorem
TauCeti.Subcomodule.map_map
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
{P : Type u_1}
[AddCommMonoid P]
[Module R P]
[Comodule R C P]
(A : Subcomodule R C M)
(f : Comodule.Hom R C M N)
(g : Comodule.Hom R C N P)
:
Images of subcomodules compose with comodule morphisms.
def
TauCeti.Comodule.Hom.range
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Hom R C M N)
:
Subcomodule R C N
The image of a comodule morphism as a subcomodule of the codomain.
Instances For
@[simp]
theorem
TauCeti.Comodule.Hom.range_toSubmodule
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Hom R C M N)
:
theorem
TauCeti.Comodule.Hom.range_finite
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Hom R C M N)
[Module.Finite R M]
:
The range of a comodule morphism out of a finitely generated module is finitely generated
as an R-module.
@[simp]
theorem
TauCeti.Comodule.Hom.mem_range
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
{f : Hom R C M N}
{n : N}
:
theorem
TauCeti.Comodule.Hom.mem_range_self
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
(f : Hom R C M N)
(m : M)
:
A comodule morphism lands in its image subcomodule.
theorem
TauCeti.Comodule.Hom.range_le_iff
{R : Type u}
{C : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
{N : Type x}
[AddCommMonoid N]
[Module R N]
[Comodule R C N]
{f : Hom R C M N}
{P : Subcomodule R C N}
:
The range of a comodule morphism is contained in P exactly when each value of the
morphism belongs to P.