Joins of subcoalgebras

This file adds suprema to the lightweight Subcoalgebra structure. The supremum of a family of subcoalgebras has underlying submodule the supremum of the underlying submodules; the comultiplication is stable because each summand lies in the inverse image under Δ of the larger submodule's tensor square. The universal property of the submodule supremum then gives the same containment for the join.

Main declarations

• Subcoalgebra.instCompleteSemilatticeSup: arbitrary suprema of subcoalgebras.
• Subcoalgebra.iSup_toSubmodule, Subcoalgebra.mem_iSup, Subcoalgebra.mem_sSup: characteristic API for arbitrary joins.
• Subcoalgebra.mem_iSup_of_directed, Subcoalgebra.coe_iSup_of_directed: a nonempty directed supremum is the union of its members.
• Subcoalgebra.mem_sSup_of_directedOn, Subcoalgebra.coe_sSup_of_directedOn: the corresponding set-indexed directed-union results.
• Subcoalgebra.sup_toSubmodule, Subcoalgebra.mem_sup: characteristic API for binary joins.
• Subcoalgebra.iSup_finite, Subcoalgebra.sup_finite, Subcoalgebra.finset_sup_finite: finite generation is preserved by finite joins.

@[instance_reducible]

instance TauCeti.Subcoalgebra.instMax {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Max (Subcoalgebra R C)

The join of two subcoalgebras has underlying submodule the join of the underlying submodules.

Equations

• TauCeti.Subcoalgebra.instMax = { max := fun (D E : TauCeti.Subcoalgebra R C) => { carrier := D.toSubmodule ⊔ E.toSubmodule, comul_mem' := ⋯ } }

@[instance_reducible]

instance TauCeti.Subcoalgebra.instSupSet {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : SupSet (Subcoalgebra R C)

The supremum of a set of subcoalgebras has underlying submodule the supremum of the underlying submodules.

Equations

• TauCeti.Subcoalgebra.instSupSet = { sSup := fun (S : Set (TauCeti.Subcoalgebra R C)) => { carrier := ⨆ (D : ↑S), (↑D).toSubmodule, comul_mem' := ⋯ } }

@[simp]

theorem TauCeti.Subcoalgebra.sup_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D E : Subcoalgebra R C) : (D ⊔ E).toSubmodule = D.toSubmodule ⊔ E.toSubmodule

The underlying submodule of the join is the join of the underlying submodules.

theorem TauCeti.Subcoalgebra.mem_sup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {D E : Subcoalgebra R C} {c : C} : c ∈ D ⊔ E ↔ ∃ d ∈ D, ∃ e ∈ E, d + e = c

Membership in the join of two subcoalgebras.

@[instance_reducible]

instance TauCeti.Subcoalgebra.instSemilatticeSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : SemilatticeSup (Subcoalgebra R C)

Subcoalgebras form a semilattice under the join whose carrier is the supremum of the underlying submodules.

Equations

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

@[simp]

theorem TauCeti.Subcoalgebra.sSup_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (S : Set (Subcoalgebra R C)) : (sSup S).toSubmodule = ⨆ (D : ↑S), (↑D).toSubmodule

The underlying submodule of a supremum of a set of subcoalgebras is the supremum of the underlying submodules indexed by that set.

theorem TauCeti.Subcoalgebra.mem_sSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {S : Set (Subcoalgebra R C)} {c : C} : c ∈ sSup S ↔ ∃ (f : ↑S →₀ C), (∀ (D : ↑S), f D ∈ ↑D) ∧ (f.sum fun (x : ↑S) (x_1 : C) => x_1) = c

Membership in the supremum of a set of subcoalgebras.

@[simp]

theorem TauCeti.Subcoalgebra.iSup_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Sort u_1} (D : ι → Subcoalgebra R C) : (⨆ (i : ι), D i).toSubmodule = ⨆ (i : ι), (D i).toSubmodule

The underlying submodule of a supremum of subcoalgebras is the supremum of the underlying submodules.

theorem TauCeti.Subcoalgebra.mem_iSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} {D : ι → Subcoalgebra R C} {c : C} : c ∈ ⨆ (i : ι), D i ↔ ∃ (f : ι →₀ C), (∀ (i : ι), f i ∈ D i) ∧ (f.sum fun (x : ι) (x_1 : C) => x_1) = c

Membership in the supremum of a family of subcoalgebras.

theorem TauCeti.Subcoalgebra.mem_iSup_of_directed {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} [Nonempty ι] {D : ι → Subcoalgebra R C} (hD : Directed (fun (x1 x2 : Subcoalgebra R C) => x1 ≤ x2) D) {c : C} : c ∈ ⨆ (i : ι), D i ↔ ∃ (i : ι), c ∈ D i

Membership in a nonempty directed supremum of subcoalgebras reduces to membership in one member of the family.

theorem TauCeti.Subcoalgebra.coe_iSup_of_directed {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} [Nonempty ι] {D : ι → Subcoalgebra R C} (hD : Directed (fun (x1 x2 : Subcoalgebra R C) => x1 ≤ x2) D) : ↑(⨆ (i : ι), D i) = ⋃ (i : ι), ↑(D i)

The carrier of a nonempty directed supremum of subcoalgebras is the union of their carriers.

theorem TauCeti.Subcoalgebra.mem_sSup_of_directedOn {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {S : Set (Subcoalgebra R C)} (hne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : Subcoalgebra R C) => x1 ≤ x2) S) {c : C} : c ∈ sSup S ↔ ∃ D ∈ S, c ∈ D

Membership in the supremum of a nonempty directed set of subcoalgebras reduces to membership in one member of the set.

theorem TauCeti.Subcoalgebra.coe_sSup_of_directedOn {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {S : Set (Subcoalgebra R C)} (hne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : Subcoalgebra R C) => x1 ≤ x2) S) : ↑(sSup S) = ⋃ D ∈ S, ↑D

The carrier of the supremum of a nonempty directed set of subcoalgebras is the union of their carriers.

@[instance_reducible]

instance TauCeti.Subcoalgebra.instCompleteSemilatticeSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : CompleteSemilatticeSup (Subcoalgebra R C)

Subcoalgebras have arbitrary suprema, computed on underlying submodules.

Equations

• TauCeti.Subcoalgebra.instCompleteSemilatticeSup = { toPartialOrder := TauCeti.Subcoalgebra.instPartialOrder, toSupSet := TauCeti.Subcoalgebra.instSupSet, isLUB_sSup := ⋯ }

theorem TauCeti.Subcoalgebra.sup_finite {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D E : Subcoalgebra R C) [Module.Finite R ↥D.toSubmodule] [Module.Finite R ↥E.toSubmodule] : Module.Finite R ↥(D ⊔ E).toSubmodule

The join of finitely generated subcoalgebras is finitely generated as an R-module.

instance TauCeti.Subcoalgebra.instFiniteSup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D E : Subcoalgebra R C) [Module.Finite R ↥D.toSubmodule] [Module.Finite R ↥E.toSubmodule] : Module.Finite R ↥(D ⊔ E).toSubmodule

The join of finitely generated subcoalgebras is finitely generated as an R-module.

@[simp]

theorem TauCeti.Subcoalgebra.finset_sup_toSubmodule {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} (s : Finset ι) (D : ι → Subcoalgebra R C) : (s.sup D).toSubmodule = s.sup fun (i : ι) => (D i).toSubmodule

The underlying submodule of a finite join of subcoalgebras is the finite join of the underlying submodules.

theorem TauCeti.Subcoalgebra.mem_finset_sup {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} {s : Finset ι} {D : ι → Subcoalgebra R C} {c : C} : c ∈ s.sup D ↔ ∃ (μ : (i : ι) → ↥(D i).toSubmodule), ∑ i ∈ s, ↑(μ i) = c

Membership in a finite join of subcoalgebras.

theorem TauCeti.Subcoalgebra.iSup_finite {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} [Finite ι] (D : ι → Subcoalgebra R C) (hD : ∀ (i : ι), Module.Finite R ↥(D i).toSubmodule) : Module.Finite R ↥(⨆ (i : ι), D i).toSubmodule

A finite supremum of finitely generated subcoalgebras is finitely generated as an R-module.

theorem TauCeti.Subcoalgebra.finset_sup_finite {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {ι : Type u_1} (s : Finset ι) (D : ι → Subcoalgebra R C) (hD : ∀ i ∈ s, Module.Finite R ↥(D i).toSubmodule) : Module.Finite R ↥(s.sup D).toSubmodule

A finite join of finitely generated subcoalgebras is finitely generated as an R-module.