Finite subcomodules

This file proves that, when the coalgebra is free as a module over a commutative semiring, every element of a right comodule is contained in a finitely generated subcomodule. It also packages the order-theoretic consequences: finite subcomodules form a nonempty directed family, finite subsets and finitely generated submodules are contained in one finite subcomodule, and the supremum and literal union of the finite subcomodules are the whole comodule. Over a field these become statements about finite-dimensional subcomodules through the same generic API.

For the elementwise result, the carrier is the span of the finitely many coefficients occurring when the element's coaction is expanded in a basis of the coalgebra. The counit shows that the original element lies in this span, and coordinate slices of coassociativity show that the span is stable under the coaction.

No flatness or noetherian hypothesis is needed.

Main declarations

• TauCeti.Subcomodule.exists_finite_subcomodule_mem: every element belongs to a subcomodule whose underlying module is finite.
• TauCeti.Subcomodule.directedOn_finiteSubcomodules: finite subcomodules form a directed family.
• TauCeti.Subcomodule.sSup_finiteSubcomodules_eq_top: for a free coefficient coalgebra, the finite subcomodules have supremum ⊤.

References

The directed-union theorem sequence from nonempty_finiteSubcomodules through iUnion_finiteSubcomodules_eq_univ_of_exists_mem is adapted from the corresponding subcoalgebra development in TauCeti.Algebra.Coalgebra.Subcoalgebra.Finite.

See Sweedler, Hopf Algebras, Chapter 2.

theorem TauCeti.Subcomodule.exists_finite_subcomodule_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] [Module.Free R C] (m : M) : ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N

If a coalgebra is free as a module over a commutative semiring, every element of a right comodule belongs to a subcomodule that is finitely generated as a module.

def TauCeti.Subcomodule.finiteSubcomodules {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] : Set (Subcomodule R C M)

The set of subcomodules that are finitely generated as R-modules.

Equations

• TauCeti.Subcomodule.finiteSubcomodules = {N : TauCeti.Subcomodule R C M | Module.Finite R ↥N.toSubmodule}

@[simp]

theorem TauCeti.Subcomodule.mem_finiteSubcomodules {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} : N ∈ finiteSubcomodules ↔ Module.Finite R ↥N.toSubmodule

theorem TauCeti.Subcomodule.nonempty_finiteSubcomodules {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] : finiteSubcomodules.Nonempty

The zero subcomodule makes the family of finite subcomodules nonempty.

theorem TauCeti.Subcomodule.supClosed_finiteSubcomodules {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] : SupClosed finiteSubcomodules

Finite subcomodules are closed under binary joins.

theorem TauCeti.Subcomodule.directedOn_finiteSubcomodules {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] : DirectedOn (fun (x1 x2 : Subcomodule R C M) => x1 ≤ x2) finiteSubcomodules

Finite subcomodules form a directed family under inclusion.

@[simp]

theorem TauCeti.Subcomodule.coe_sSup_finiteSubcomodules {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] : ↑(sSup finiteSubcomodules) = ⋃ (N : ↑finiteSubcomodules), ↑↑N

The carrier of the supremum of all finite subcomodules is their literal union.

@[simp]

theorem TauCeti.Subcomodule.mem_sSup_finiteSubcomodules {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} : m ∈ sSup finiteSubcomodules ↔ ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N

Membership in the supremum of all finite subcomodules means membership in one finite subcomodule.

theorem TauCeti.Subcomodule.exists_finite_subcomodule_of_setFinite_of_exists_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] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) {s : Set M} (hs : s.Finite) : ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ s ⊆ ↑N

If every element lies in a finite subcomodule, then every finite set lies in one finite subcomodule.

theorem TauCeti.Subcomodule.exists_finite_subcomodule_of_fg_of_exists_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] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) (P : Submodule R M) (hP : P.FG) : ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ P ≤ N.toSubmodule

If every element lies in a finite subcomodule, then every finitely generated submodule lies in one finite subcomodule.

theorem TauCeti.Subcomodule.sSup_finiteSubcomodules_eq_top_of_exists_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] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) : sSup finiteSubcomodules = ⊤

If every element lies in a finite subcomodule, then the supremum of all finite subcomodules is the whole comodule.

theorem TauCeti.Subcomodule.iUnion_finiteSubcomodules_eq_univ_of_exists_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] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) : ⋃ (N : ↑finiteSubcomodules), ↑↑N = Set.univ

If every element lies in a finite subcomodule, then the union of all finite subcomodules is the whole carrier.

theorem TauCeti.Subcomodule.exists_finite_subcomodule_of_setFinite {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] [Module.Free R C] {s : Set M} (hs : s.Finite) : ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ s ⊆ ↑N

If the coefficient coalgebra is free, every finite set lies in a finite subcomodule.

theorem TauCeti.Subcomodule.exists_finite_subcomodule_of_fg {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] [Module.Free R C] (P : Submodule R M) (hP : P.FG) : ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ P ≤ N.toSubmodule

If the coefficient coalgebra is free, every finitely generated submodule lies in a finite subcomodule.

@[simp]

theorem TauCeti.Subcomodule.sSup_finiteSubcomodules_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] [Module.Free R C] : sSup finiteSubcomodules = ⊤

If the coefficient coalgebra is free, the finite subcomodules have supremum ⊤.

@[simp]

theorem TauCeti.Subcomodule.iUnion_finiteSubcomodules_eq_univ {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] [Module.Free R C] : ⋃ (N : Subcomodule R C M), ⋃ (_ : Module.Finite R ↥N.toSubmodule), ↑N = Set.univ

If the coefficient coalgebra is free, the union of the finite subcomodules is the whole carrier.