English
Let P be a semilattice with join, directed by ≥. For any two ideals I and J of P, their join in the lattice of ideals is the downward-closed set of all x ≤ i ⊔ j with i ∈ I and j ∈ J, i.e., I ⊔ J = { x ∈ P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j }.
Русский
Пусть P — полупорядоченное множество с операцией соединения ⊔ и направлено по ≥. Для любых идеалов I и J множества P их объединение в решётке идеалов равно нисходящему замыканию по элементам i ⊔ j с i ∈ I, j ∈ J: I ⊔ J = { x ∈ P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j }.
LaTeX
$$$ \forall I,J \in \mathrm{Ideal}(P),\ I \lor J = \{ x \in P \mid \exists i \in I, \exists j \in J, x \le i \lor j \}.$$$
Lean4
/-- The supremum of two ideals of a co-directed order is the union of the down sets of the pointwise
supremum of `I` and `J`. -/
instance : Max (Ideal P) :=
⟨fun I J ↦
{ carrier := {x | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}
nonempty' := by
obtain ⟨w, h⟩ := inter_nonempty I J
exact ⟨w, w, h.1, w, h.2, le_sup_left⟩
directed' := fun x ⟨xi, _, xj, _, _⟩ y ⟨yi, _, yj, _, _⟩ ↦
⟨x ⊔ y,
⟨xi ⊔ yi, sup_mem ‹_› ‹_›, xj ⊔ yj, sup_mem ‹_› ‹_›,
sup_le
(calc
x ≤ xi ⊔ xj := ‹_›
_ ≤ xi ⊔ yi ⊔ (xj ⊔ yj) := sup_le_sup le_sup_left le_sup_left)
(calc
y ≤ yi ⊔ yj := ‹_›
_ ≤ xi ⊔ yi ⊔ (xj ⊔ yj) := sup_le_sup le_sup_right le_sup_right)⟩,
le_sup_left, le_sup_right⟩
lower' := fun _ _ h ⟨yi, hi, yj, hj, hxy⟩ ↦ ⟨yi, hi, yj, hj, h.trans hxy⟩ }⟩
