Joins of subcomodules

This file adds suprema to the lightweight Subcomodule structure. The supremum of a family of subcomodules has underlying submodule the supremum of the underlying submodules; the coaction is stable because each summand lies in the inverse image under ρ of the tensor product of the larger submodule with the coalgebra. The universal property of the submodule supremum then gives the same containment for the join.

Main declarations

• Subcomodule.instCompleteSemilatticeSup: arbitrary suprema of subcomodules.
• Subcomodule.iSup_toSubmodule, Subcomodule.mem_iSup, Subcomodule.mem_sSup: characteristic API for arbitrary joins.
• Subcomodule.coe_iSup_of_directed, Subcomodule.mem_iSup_of_directed: a nonempty directed join has carrier equal to the union of the carriers.
• Subcomodule.sup_toSubmodule, Subcomodule.mem_sup: characteristic API for binary joins.
• Subcomodule.iSup_finite, Subcomodule.sup_finite, Subcomodule.finset_sup_finite: finite generation is preserved by finite joins.
• Subcomodule.map_sup, Subcomodule.map_iSup: images preserve joins.

References

The lattice construction is adapted from TauCeti.Algebra.Coalgebra.Subcoalgebra.Lattice, and the image-join lemmas follow the corresponding map API in TauCeti.Algebra.Coalgebra.Subcoalgebra.Map.

@[instance_reducible]

instance TauCeti.Subcomodule.instMax {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] : Max (Subcomodule R C M)

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

Equations

• TauCeti.Subcomodule.instMax = { max := fun (N P : TauCeti.Subcomodule R C M) => { carrier := N.toSubmodule ⊔ P.toSubmodule, coact_mem' := ⋯ } }

@[instance_reducible]

instance TauCeti.Subcomodule.instSupSet {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] : SupSet (Subcomodule R C M)

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

Equations

• TauCeti.Subcomodule.instSupSet = { sSup := fun (S : Set (TauCeti.Subcomodule R C M)) => { carrier := ⨆ (N : ↑S), (↑N).toSubmodule, coact_mem' := ⋯ } }

@[simp]

theorem TauCeti.Subcomodule.sup_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) : (N ⊔ P).toSubmodule = N.toSubmodule ⊔ P.toSubmodule

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

theorem TauCeti.Subcomodule.mem_sup {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} {m : M} : m ∈ N ⊔ P ↔ ∃ n ∈ N, ∃ p ∈ P, n + p = m

Membership in the join of two subcomodules.

@[instance_reducible]

instance TauCeti.Subcomodule.instSemilatticeSup {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] : SemilatticeSup (Subcomodule R C M)

Subcomodules 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.Subcomodule.sSup_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] (S : Set (Subcomodule R C M)) : (sSup S).toSubmodule = ⨆ (N : ↑S), (↑N).toSubmodule

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

theorem TauCeti.Subcomodule.mem_sSup {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] {S : Set (Subcomodule R C M)} {m : M} : m ∈ sSup S ↔ ∃ (f : ↑S →₀ M), (∀ (N : ↑S), f N ∈ ↑N) ∧ (f.sum fun (x : ↑S) (x_1 : M) => x_1) = m

Membership in the supremum of a set of subcomodules.

@[simp]

theorem TauCeti.Subcomodule.iSup_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] {ι : Sort u_1} (N : ι → Subcomodule R C M) : (⨆ (i : ι), N i).toSubmodule = ⨆ (i : ι), (N i).toSubmodule

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

theorem TauCeti.Subcomodule.mem_iSup {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 u_1} {N : ι → Subcomodule R C M} {m : M} : m ∈ ⨆ (i : ι), N i ↔ ∃ (f : ι →₀ M), (∀ (i : ι), f i ∈ N i) ∧ (f.sum fun (x : ι) (x_1 : M) => x_1) = m

Membership in the supremum of a family of subcomodules.

@[instance_reducible]

instance TauCeti.Subcomodule.instCompleteSemilatticeSup {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] : CompleteSemilatticeSup (Subcomodule R C M)

Subcomodules have arbitrary suprema, computed on underlying submodules.

Equations

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

@[simp]

theorem TauCeti.Subcomodule.coe_iSup_of_directed {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] {iota : Type u_1} [Nonempty iota] (N : iota → Subcomodule R C M) (hN : Directed (fun (x1 x2 : Subcomodule R C M) => x1 ≤ x2) N) : ↑(⨆ (i : iota), N i) = ⋃ (i : iota), ↑(N i)

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

@[simp]

theorem TauCeti.Subcomodule.mem_iSup_of_directed {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] {iota : Type u_1} [Nonempty iota] (N : iota → Subcomodule R C M) (hN : Directed (fun (x1 x2 : Subcomodule R C M) => x1 ≤ x2) N) {m : M} : m ∈ ⨆ (i : iota), N i ↔ ∃ (i : iota), m ∈ N i

An element belongs to a nonempty directed supremum of subcomodules exactly when it belongs to one member of the family.

@[simp]

theorem TauCeti.Subcomodule.coe_sSup_of_directedOn {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] {S : Set (Subcomodule R C M)} (hS : S.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Subcomodule R C M) => x1 ≤ x2) S) : ↑(sSup S) = ⋃ (N : ↑S), ↑↑N

The carrier of the supremum of a nonempty directed set of subcomodules is the union of its carriers.

@[simp]

theorem TauCeti.Subcomodule.mem_sSup_of_directedOn {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] {S : Set (Subcomodule R C M)} (hS : S.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Subcomodule R C M) => x1 ≤ x2) S) {m : M} : m ∈ sSup S ↔ ∃ N ∈ S, m ∈ N

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

theorem TauCeti.Subcomodule.sup_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 P : Subcomodule R C M) [Module.Finite R ↥N.toSubmodule] [Module.Finite R ↥P.toSubmodule] : Module.Finite R ↥(N ⊔ P).toSubmodule

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

instance TauCeti.Subcomodule.instFiniteSup {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) [Module.Finite R ↥N.toSubmodule] [Module.Finite R ↥P.toSubmodule] : Module.Finite R ↥(N ⊔ P).toSubmodule

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

@[simp]

theorem TauCeti.Subcomodule.finset_sup_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] {ι : Type u_1} (s : Finset ι) (N : ι → Subcomodule R C M) : (s.sup N).toSubmodule = s.sup fun (i : ι) => (N i).toSubmodule

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

theorem TauCeti.Subcomodule.mem_finset_sup {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 u_1} {s : Finset ι} {N : ι → Subcomodule R C M} {m : M} : m ∈ s.sup N ↔ ∃ (μ : (i : ι) → ↥(N i).toSubmodule), ∑ i ∈ s, ↑(μ i) = m

Membership in a finite join of subcomodules.

theorem TauCeti.Subcomodule.iSup_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] {ι : Sort u_2} [Finite ι] (N : ι → Subcomodule R C M) (hN : ∀ (i : ι), Module.Finite R ↥(N i).toSubmodule) : Module.Finite R ↥(⨆ (i : ι), N i).toSubmodule

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

theorem TauCeti.Subcomodule.finset_sup_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] {ι : Type u_1} (s : Finset ι) (N : ι → Subcomodule R C M) (hN : ∀ i ∈ s, Module.Finite R ↥(N i).toSubmodule) : Module.Finite R ↥(s.sup N).toSubmodule

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

@[simp]

theorem TauCeti.Subcomodule.map_sup {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' : Type u_2} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] (f : Comodule.Hom R C M M') (N P : Subcomodule R C M) : (N ⊔ P).map f = N.map f ⊔ P.map f

The image of a binary join is the binary join of the images.

@[simp]

theorem TauCeti.Subcomodule.map_iSup {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' : Type u_2} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] {ι : Sort u_3} (f : Comodule.Hom R C M M') (N : ι → Subcomodule R C M) : (⨆ (i : ι), N i).map f = ⨆ (i : ι), (N i).map f

The image of a supremum is the supremum of the images.

@[simp]

theorem TauCeti.Subcomodule.map_finset_sup {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 u_1} {M' : Type u_2} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] (s : Finset ι) (f : Comodule.Hom R C M M') (N : ι → Subcomodule R C M) : (s.sup N).map f = s.sup fun (i : ι) => (N i).map f

The image of a finite join is the finite join of the images.