Finite subcoalgebras and directed unions

This file proves the elementwise fundamental theorem of coalgebras over a principal ideal domain: if the coalgebra is free as a module, then each of its elements belongs to a finite subcoalgebra. Over a field the freeness hypothesis is automatic, so every coalgebra element belongs to a finite-dimensional subcoalgebra.

Over a commutative semiring, the module-finite subcoalgebras are nonempty and directed under finite joins. An abstract elementwise covering hypothesis therefore upgrades to containment of finite subsets and finitely generated submodules, and identifies the coalgebra as both the supremum and the literal union of its module-finite subcoalgebras. Applying the elementwise theorems gives these conclusions over a principal ideal domain and over a field.

The finite regular subcomodule containing the element need not itself be a subcoalgebra. Instead, we equip its subtype with the induced comodule structure and take its matrix-coefficient subcoalgebra. The counit matrix coefficient recovers the original element.

Main declarations

• TauCeti.Subcoalgebra.exists_finite_subcoalgebra_mem: the PID result for a coalgebra that is free as a module.
• TauCeti.Subcoalgebra.exists_finiteDimensional_subcoalgebra_mem: the field specialization.
• TauCeti.Subcoalgebra.directedOn_finiteSubcoalgebras: module-finite subcoalgebras are directed.
• TauCeti.Subcoalgebra.exists_finite_subcoalgebra_of_setFinite: every finite subset is contained in a module-finite subcoalgebra under the PID hypotheses.
• TauCeti.Subcoalgebra.sSup_finiteSubcoalgebras_eq_top: a PID/free coalgebra is the supremum of its module-finite subcoalgebras.
• TauCeti.Subcoalgebra.sSup_finiteDimensional_subcoalgebras_eq_top: a coalgebra over a field is the supremum of its finite-dimensional subcoalgebras.

References

See Sweedler, Hopf Algebras, Chapter 2; Milne, Algebraic Groups, Proposition 4.7 and Section 9d; and Hazewinkel, "Cofree coalgebras and multivariable recursiveness", Theorem 8.4.

def TauCeti.Subcoalgebra.finiteSubcoalgebras (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Set (Subcoalgebra R C)

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

Equations

• TauCeti.Subcoalgebra.finiteSubcoalgebras R C = {D : TauCeti.Subcoalgebra R C | Module.Finite R ↥D.toSubmodule}

@[simp]

theorem TauCeti.Subcoalgebra.mem_finiteSubcoalgebras {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D : Subcoalgebra R C} : D ∈ finiteSubcoalgebras R C ↔ Module.Finite R ↥D.toSubmodule

A subcoalgebra belongs to finiteSubcoalgebras exactly when its underlying module is finite.

theorem TauCeti.Subcoalgebra.nonempty_finiteSubcoalgebras {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : (finiteSubcoalgebras R C).Nonempty

The family of module-finite subcoalgebras is nonempty.

theorem TauCeti.Subcoalgebra.sup_mem_finiteSubcoalgebras {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} (hD : D ∈ finiteSubcoalgebras R C) (hE : E ∈ finiteSubcoalgebras R C) : D ⊔ E ∈ finiteSubcoalgebras R C

The join of two module-finite subcoalgebras is module-finite.

theorem TauCeti.Subcoalgebra.directedOn_finiteSubcoalgebras {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : DirectedOn (fun (x1 x2 : Subcoalgebra R C) => x1 ≤ x2) (finiteSubcoalgebras R C)

The family of module-finite subcoalgebras is directed under inclusion.

@[simp]

theorem TauCeti.Subcoalgebra.mem_sSup_finiteSubcoalgebras {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {c : C} : c ∈ sSup (finiteSubcoalgebras R C) ↔ ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D

Membership in the supremum of the module-finite subcoalgebras is membership in one such subcoalgebra.

theorem TauCeti.Subcoalgebra.coe_sSup_finiteSubcoalgebras {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : ↑(sSup (finiteSubcoalgebras R C)) = ⋃ D ∈ finiteSubcoalgebras R C, ↑D

The carrier of the supremum of the module-finite subcoalgebras is their literal union.

theorem TauCeti.Subcoalgebra.exists_finite_subcoalgebra_of_setFinite_of_exists_mem {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (hcover : ∀ (c : C), ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D) (s : Set C) (hs : s.Finite) : ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ s ⊆ ↑D

If every element is contained in a module-finite subcoalgebra, then every finite subset is contained in one module-finite subcoalgebra.

theorem TauCeti.Subcoalgebra.exists_finite_subcoalgebra_of_finite_submodule_of_exists_mem {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (hcover : ∀ (c : C), ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D) (M : Submodule R C) [Module.Finite R ↥M] : ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ M ≤ D.toSubmodule

If every element is contained in a module-finite subcoalgebra, then every module-finite submodule is contained in one module-finite subcoalgebra.

theorem TauCeti.Subcoalgebra.sSup_finiteSubcoalgebras_eq_top_of_exists_mem {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (hcover : ∀ (c : C), ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D) : sSup (finiteSubcoalgebras R C) = ⊤

If every element is contained in a module-finite subcoalgebra, then the supremum of all module-finite subcoalgebras is the whole coalgebra.

theorem TauCeti.Subcoalgebra.iUnion_finiteSubcoalgebras_eq_univ_of_exists_mem {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (hcover : ∀ (c : C), ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D) : ⋃ D ∈ finiteSubcoalgebras R C, ↑D = Set.univ

If every element is contained in a module-finite subcoalgebra, then the literal union of all module-finite subcoalgebras is the whole carrier.

theorem TauCeti.Subcoalgebra.exists_finite_subcoalgebra_mem {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] [Module.Free R C] (c : C) : ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D

If C is a coalgebra that is free as a module over a commutative principal ideal domain, then every element of C belongs to a subcoalgebra that is finite as a module.

theorem TauCeti.Subcoalgebra.exists_finite_subcoalgebra_of_setFinite {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] [Module.Free R C] (s : Set C) (hs : s.Finite) : ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ s ⊆ ↑D

Every finite subset of a coalgebra that is free over a commutative principal ideal domain is contained in a module-finite subcoalgebra.

theorem TauCeti.Subcoalgebra.exists_finite_subcoalgebra_of_finite_submodule {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] [Module.Free R C] (M : Submodule R C) [Module.Finite R ↥M] : ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ M ≤ D.toSubmodule

Every module-finite submodule of a coalgebra that is free over a commutative principal ideal domain is contained in a module-finite subcoalgebra.

theorem TauCeti.Subcoalgebra.sSup_finiteSubcoalgebras_eq_top {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] [Module.Free R C] : sSup (finiteSubcoalgebras R C) = ⊤

A coalgebra that is free over a commutative principal ideal domain is the supremum of its module-finite subcoalgebras.

theorem TauCeti.Subcoalgebra.iUnion_finiteSubcoalgebras_eq_univ {R : Type u} {C : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] [Module.Free R C] : ⋃ D ∈ finiteSubcoalgebras R C, ↑D = Set.univ

A coalgebra that is free over a commutative principal ideal domain is the literal union of its module-finite subcoalgebras.

theorem TauCeti.Subcoalgebra.exists_finiteDimensional_subcoalgebra_mem {C : Type v} {k : Type u} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] (c : C) : ∃ (D : Subcoalgebra k C), FiniteDimensional k ↥D.toSubmodule ∧ c ∈ D

Every element of a coalgebra over a field belongs to a finite-dimensional subcoalgebra.

theorem TauCeti.Subcoalgebra.exists_finiteDimensional_subcoalgebra_of_setFinite {C : Type v} {k : Type u} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] (s : Set C) (hs : s.Finite) : ∃ (D : Subcoalgebra k C), FiniteDimensional k ↥D.toSubmodule ∧ s ⊆ ↑D

Every finite subset of a coalgebra over a field is contained in a finite-dimensional subcoalgebra.

theorem TauCeti.Subcoalgebra.exists_finiteDimensional_subcoalgebra_of_finiteDimensional_submodule {C : Type v} {k : Type u} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] (M : Submodule k C) [FiniteDimensional k ↥M] : ∃ (D : Subcoalgebra k C), FiniteDimensional k ↥D.toSubmodule ∧ M ≤ D.toSubmodule

Every finite-dimensional subspace of a coalgebra over a field is contained in a finite-dimensional subcoalgebra.

theorem TauCeti.Subcoalgebra.sSup_finiteDimensional_subcoalgebras_eq_top {C : Type v} {k : Type u} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] : sSup {D : Subcoalgebra k C | FiniteDimensional k ↥D.toSubmodule} = ⊤

Every coalgebra over a field is the supremum of its finite-dimensional subcoalgebras.

theorem TauCeti.Subcoalgebra.iUnion_finiteDimensional_subcoalgebras_eq_univ {C : Type v} {k : Type u} [Field k] [AddCommGroup C] [Module k C] [Coalgebra k C] : ⋃ (D : Subcoalgebra k C), ⋃ (_ : FiniteDimensional k ↥D.toSubmodule), ↑D = Set.univ

Every coalgebra over a field is the literal union of its finite-dimensional subcoalgebras.