instSemilatticeSupSubtypeSmallMem

English

There is a canonical semilattice structure on the set of finitely generated submodules, where the join is given by the sum of submodules.

Русский

Существует каноническая полупрямая структура на множестве конечнопорожденных подмодулей, где наибольшая верхняя граница задаётся их суммой.

LaTeX

$$$\text{SemilatticeSup} \{P : \text{Submodule} R M \;\vert\; P \text{ finitely generated}\}$ with join given by sum$$

Lean4

instance : SemilatticeSup { P : Submodule R M // Small.{u} P }
    where
  sup := fun P Q ↦ ⟨P.val ⊔ Q.val, small_sup (smallP := P.property) (smallQ := Q.property)⟩
  le_sup_left := fun P Q ↦ by rw [← Subtype.coe_le_coe]; exact le_sup_left
  le_sup_right := fun P Q ↦ by rw [← Subtype.coe_le_coe]; exact le_sup_right
  sup_le := fun _ _ _ hPR hQR ↦ by
    rw [← Subtype.coe_le_coe] at hPR hQR ⊢
    exact sup_le hPR hQR

Похожие утверждения