Mathlib.Order.CompactlyGenerated.Basic

CompleteLattice.IsSupClosedCompact definition

: Prop

Full source

/-- A compactness property for a complete lattice is that any `sup`-closed non-empty subset
contains its `sSup`. -/
def IsSupClosedCompact : Prop :=
  ∀ (s : Set α) (_ : s.Nonempty), SupClosed s → sSupsSup s ∈ s

Sup-closed compactness for complete lattices

Informal description

A complete lattice $\alpha$ is called *sup-closed compact* if every nonempty sup-closed subset $s$ of $\alpha$ contains its supremum $\bigvee s$.

CompleteLattice.IsSupFiniteCompact definition

: Prop

Full source

/-- A compactness property for a complete lattice is that any subset has a finite subset with the
same `sSup`. -/
def IsSupFiniteCompact : Prop :=
  ∀ s : Set α, ∃ t : Finset α, ↑t ⊆ s ∧ sSup s = t.sup id

Sup-finite compactness for complete lattices

Informal description

A complete lattice $\alpha$ is called *sup-finite compact* if for every subset $s$ of $\alpha$, there exists a finite subset $t \subseteq s$ such that the supremum of $s$ is equal to the supremum of $t$.

CompleteLattice.IsCompactElement definition

{α : Type*} [CompleteLattice α] (k : α)

Full source

/-- An element `k` of a complete lattice is said to be compact if any set with `sSup`
above `k` has a finite subset with `sSup` above `k`.  Such an element is also called
"finite" or "S-compact". -/
def IsCompactElement {α : Type*} [CompleteLattice α] (k : α) :=
  ∀ s : Set α, k ≤ sSup s → ∃ t : Finset α, ↑t ⊆ s ∧ k ≤ t.sup id

Compact element in a complete lattice

Informal description

An element $k$ of a complete lattice $\alpha$ is called *compact* if for any subset $s \subseteq \alpha$ such that $k \leq \bigvee s$, there exists a finite subset $t \subseteq s$ such that $k \leq \bigvee t$.

CompleteLattice.isCompactElement_iff theorem

 {α : Type u} [CompleteLattice α] (k : α) :
  CompleteLattice.IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s

Full source

theorem isCompactElement_iff.{u} {α : Type u} [CompleteLattice α] (k : α) :
    CompleteLattice.IsCompactElementCompleteLattice.IsCompactElement k ↔
      ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t : Finset ι, k ≤ t.sup s := by
  classical
    constructor
    · intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
    · intro H s hs
      obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
      rw [Finset.sup_le_iff]
      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

Characterization of Compact Elements in Complete Lattices via Finite Suprema

Informal description

An element $k$ of a complete lattice $\alpha$ is compact if and only if for every indexed family $s : \iota \to \alpha$ such that $k \leq \bigsqcup_i s_i$, there exists a finite subset $t \subseteq \iota$ such that $k \leq \bigsqcup_{i \in t} s_i$.

CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le theorem

 (k : α) : IsCompactElement k ↔ ∀ s : Set α, s.Nonempty → DirectedOn (· ≤ ·) s → k ≤ sSup s → ∃ x : α, x ∈ s ∧ k ≤ x

Full source

/-- An element `k` is compact if and only if any directed set with `sSup` above
`k` already got above `k` at some point in the set. -/
theorem isCompactElement_iff_le_of_directed_sSup_le (k : α) :
    IsCompactElementIsCompactElement k ↔
      ∀ s : Set α, s.Nonempty → DirectedOn (· ≤ ·) s → k ≤ sSup s → ∃ x : α, x ∈ s ∧ k ≤ x := by
  classical
    constructor
    · intro hk s hne hdir hsup
      obtain ⟨t, ht⟩ := hk s hsup
      -- certainly every element of t is below something in s, since ↑t ⊆ s.
      have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
      obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
      exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
    · intro hk s hsup
      -- Consider the set of finite joins of elements of the (plain) set s.
      let S : Set α := { x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id }
      -- S is directed, nonempty, and still has sup above k.
      have dir_US : DirectedOn (· ≤ ·) S := by
        rintro x ⟨c, hc⟩ y ⟨d, hd⟩
        use x ⊔ y
        constructor
        · use c ∪ d
          constructor
          · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
          · simp only [hc.right, hd.right, Finset.sup_union]
        simp only [and_self_iff, le_sup_left, le_sup_right]
      have sup_S : sSup s ≤ sSup S := by
        apply sSup_le_sSup
        intro x hx
        use {x}
        simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true,
          Finset.sup_singleton, Set.singleton_subset_iff]
      have Sne : S.Nonempty := by
        suffices ⊥⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true,
          and_self_iff]
      -- Now apply the defn of compact and finish.
      obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
      obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
      use t
      exact ⟨htS, by rwa [← htsup]⟩

Characterization of Compact Elements via Directed Suprema in Complete Lattices

Informal description

An element $k$ in a complete lattice $\alpha$ is compact if and only if for every nonempty directed subset $s \subseteq \alpha$ with respect to the order $\leq$, if $k$ is less than or equal to the supremum of $s$, then there exists some element $x \in s$ such that $k \leq x$.

CompleteLattice.IsCompactElement.exists_finset_of_le_iSup theorem

 {k : α} (hk : IsCompactElement k) {ι : Type*} (f : ι → α) (h : k ≤ ⨆ i, f i) : ∃ s : Finset ι, k ≤ ⨆ i ∈ s, f i

Full source

theorem IsCompactElement.exists_finset_of_le_iSup {k : α} (hk : IsCompactElement k) {ι : Type*}
    (f : ι → α) (h : k ≤ ⨆ i, f i) : ∃ s : Finset ι, k ≤ ⨆ i ∈ s, f i := by
  classical
    let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
    have h1 : DirectedOn (· ≤ ·) (Set.range g) := by
      rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
      exact
        ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_right⟩
    have h2 : k ≤ sSup (Set.range g) :=
      h.trans
        (iSup_le fun i =>
          le_sSup_of_le ⟨{i}, rfl⟩
            (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
    obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
      (isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g)
        h1 h2
    exact ⟨s, hs⟩

Compact elements are finitely approximated under suprema

Informal description

Let $k$ be a compact element in a complete lattice $\alpha$. For any indexed family of elements $f : \iota \to \alpha$ such that $k \leq \bigsqcup_{i \in \iota} f(i)$, there exists a finite subset $s \subseteq \iota$ such that $k \leq \bigsqcup_{i \in s} f(i)$.

CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt theorem

 {α : Type*} [CompleteLattice α] {k : α} (hk : IsCompactElement k) {s : Set α} (hemp : s.Nonempty)
  (hdir : DirectedOn (· ≤ ·) s) (hbelow : ∀ x ∈ s, x < k) : sSup s < k

Full source

/-- A compact element `k` has the property that any directed set lying strictly below `k` has
its `sSup` strictly below `k`. -/
theorem IsCompactElement.directed_sSup_lt_of_lt {α : Type*} [CompleteLattice α] {k : α}
    (hk : IsCompactElement k) {s : Set α} (hemp : s.Nonempty) (hdir : DirectedOn (· ≤ ·) s)
    (hbelow : ∀ x ∈ s, x < k) : sSup s < k := by
  rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
  by_contra h
  have sSup' : sSup s ≤ k := sSup_le s k fun s hs => (hbelow s hs).le
  replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
  obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le
  obtain hxk := hbelow x hxs
  exact hxk.ne (hxk.le.antisymm hkx)

Supremum of Directed Set Below Compact Element is Strictly Below It

Informal description

Let $\alpha$ be a complete lattice and $k \in \alpha$ be a compact element. For any nonempty directed subset $s \subseteq \alpha$ with respect to the order $\leq$, if every element $x \in s$ satisfies $x < k$, then the supremum of $s$ is strictly less than $k$, i.e., $\bigvee s < k$.

CompleteLattice.isCompactElement_finsetSup theorem

 {α β : Type*} [CompleteLattice α] {f : β → α} (s : Finset β) (h : ∀ x ∈ s, IsCompactElement (f x)) :
  IsCompactElement (s.sup f)

Full source

theorem isCompactElement_finsetSup {α β : Type*} [CompleteLattice α] {f : β → α} (s : Finset β)
    (h : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f) := by
  classical
    rw [isCompactElement_iff_le_of_directed_sSup_le]
    intro d hemp hdir hsup
    rw [← Function.id_comp f]
    rw [← Finset.sup_image]
    apply Finset.sup_le_of_le_directed d hemp hdir
    rintro x hx
    obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
    specialize h p hps
    rw [isCompactElement_iff_le_of_directed_sSup_le] at h
    specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
    simpa only [exists_prop]

Finite Supremum of Compact Elements is Compact in a Complete Lattice

Informal description

Let $\alpha$ be a complete lattice and $\beta$ be a type. For any function $f \colon \beta \to \alpha$ and any finite subset $s \subseteq \beta$, if every element $f(x)$ is compact for $x \in s$, then the supremum $\bigvee_{x \in s} f(x)$ is also a compact element in $\alpha$.

CompleteLattice.WellFoundedGT.isSupFiniteCompact theorem

[WellFoundedGT α] : IsSupFiniteCompact α

Full source

theorem WellFoundedGT.isSupFiniteCompact [WellFoundedGT α] :
    IsSupFiniteCompact α := fun s => by
  let S := { x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x }
  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩
  refine ⟨t, ht₁, (sSup_le _ _ fun y hy => ?_).antisymm ?_⟩
  · classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
  · rw [Finset.sup_id_eq_sSup]
    exact sSup_le_sSup ht₁

Well-founded complete lattices are sup-finite compact

Informal description

For any complete lattice $\alpha$ where the "greater than" relation $>$ is well-founded, the lattice is sup-finite compact. That is, for every subset $s \subseteq \alpha$, there exists a finite subset $t \subseteq s$ such that $\bigvee s = \bigvee t$.

CompleteLattice.IsSupFiniteCompact.isSupClosedCompact theorem

(h : IsSupFiniteCompact α) : IsSupClosedCompact α

Full source

theorem IsSupFiniteCompact.isSupClosedCompact (h : IsSupFiniteCompact α) :
    IsSupClosedCompact α := by
  intro s hne hsc; obtain ⟨t, ht₁, ht₂⟩ := h s; clear h
  rcases t.eq_empty_or_nonempty with h | h
  · subst h
    rw [Finset.sup_empty] at ht₂
    rw [ht₂]
    simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]
  · rw [ht₂]
    exact hsc.finsetSup_mem h ht₁

Sup-finite compactness implies sup-closed compactness in complete lattices

Informal description

If a complete lattice $\alpha$ is sup-finite compact, then it is also sup-closed compact. That is, if for every subset $s \subseteq \alpha$ there exists a finite subset $t \subseteq s$ such that $\bigvee s = \bigvee t$, then every nonempty sup-closed subset $s \subseteq \alpha$ contains its supremum $\bigvee s$.

CompleteLattice.IsSupClosedCompact.wellFoundedGT theorem

(h : IsSupClosedCompact α) : WellFoundedGT α

Full source

theorem IsSupClosedCompact.wellFoundedGT (h : IsSupClosedCompact α) :
    WellFoundedGT α where
  wf := by
    refine RelEmbedding.wellFounded_iff_no_descending_seq.mpr ⟨fun a => ?_⟩
    suffices sSupsSup (Set.range a) ∈ Set.range a by
      obtain ⟨n, hn⟩ := Set.mem_range.mp this
      have h' : sSup (Set.range a) < a (n + 1) := by
        change _ > _
        simp [← hn, a.map_rel_iff]
      apply lt_irrefl (a (n + 1))
      apply lt_of_le_of_lt _ h'
      apply le_sSup
      apply Set.mem_range_self
    apply h (Set.range a)
    · use a 37
      apply Set.mem_range_self
    · rintro x ⟨m, hm⟩ y ⟨n, hn⟩
      use m ⊔ n
      rw [← hm, ← hn]
      apply RelHomClass.map_sup a

Sup-closed compactness implies well-foundedness of $>$ in complete lattices

Informal description

If a complete lattice $\alpha$ is sup-closed compact, then the "greater than" relation $>$ on $\alpha$ is well-founded. That is, every nonempty subset of $\alpha$ has a minimal element with respect to $>$.

CompleteLattice.isSupFiniteCompact_iff_all_elements_compact theorem

: IsSupFiniteCompact α ↔ ∀ k : α, IsCompactElement k

Full source

theorem isSupFiniteCompact_iff_all_elements_compact :
    IsSupFiniteCompactIsSupFiniteCompact α ↔ ∀ k : α, IsCompactElement k := by
  refine ⟨fun h k s hs => ?_, fun h s => ?_⟩
  · obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
    use t, hts
    rwa [← htsup]
  · obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)
    have : sSup s = t.sup id := by
      suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
      simp only [id, Finset.sup_le_iff]
      intro x hx
      exact le_sSup _ _ (hts hx)
    exact ⟨t, hts, this⟩

Equivalence of Sup-Finite Compactness and All Elements Being Compact in a Complete Lattice

Informal description

A complete lattice $\alpha$ is sup-finite compact if and only if every element $k \in \alpha$ is compact. That is, for every subset $s \subseteq \alpha$ there exists a finite subset $t \subseteq s$ such that $\bigvee s = \bigvee t$ if and only if for every element $k \in \alpha$ and every subset $s \subseteq \alpha$ with $k \leq \bigvee s$, there exists a finite subset $t \subseteq s$ such that $k \leq \bigvee t$.

CompleteLattice.wellFoundedGT_characterisations theorem

: List.TFAE [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k]

Full source

theorem wellFoundedGT_characterisations : List.TFAE
    [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k] := by
  tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _
  tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α
  tfae_have 3 → 1 := IsSupClosedCompact.wellFoundedGT α
  tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α
  tfae_finish

Characterization of Well-Founded Complete Lattices via Compactness Properties

Informal description

For a complete lattice $\alpha$, the following conditions are equivalent: 1. The "greater than" relation $>$ on $\alpha$ is well-founded. 2. $\alpha$ is sup-finite compact (i.e., for every subset $s \subseteq \alpha$, there exists a finite subset $t \subseteq s$ such that $\bigvee s = \bigvee t$). 3. $\alpha$ is sup-closed compact (i.e., every nonempty sup-closed subset $s \subseteq \alpha$ contains its supremum $\bigvee s$). 4. Every element $k \in \alpha$ is compact (i.e., for any subset $s \subseteq \alpha$ with $k \leq \bigvee s$, there exists a finite subset $t \subseteq s$ such that $k \leq \bigvee t$).

CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact theorem

: WellFoundedGT α ↔ IsSupFiniteCompact α

Full source

theorem wellFoundedGT_iff_isSupFiniteCompact :
    WellFoundedGTWellFoundedGT α ↔ IsSupFiniteCompact α :=
  (wellFoundedGT_characterisations α).out 0 1

Equivalence of Well-Foundedness and Sup-Finite Compactness in Complete Lattices

Informal description

For a complete lattice $\alpha$, the "greater than" relation $>$ is well-founded if and only if $\alpha$ is sup-finite compact. That is, every non-empty subset of $\alpha$ has a minimal element with respect to $>$ if and only if for every subset $s \subseteq \alpha$, there exists a finite subset $t \subseteq s$ such that $\bigvee s = \bigvee t$.

CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact theorem

: IsSupFiniteCompact α ↔ IsSupClosedCompact α

Full source

theorem isSupFiniteCompact_iff_isSupClosedCompact : IsSupFiniteCompactIsSupFiniteCompact α ↔ IsSupClosedCompact α :=
  (wellFoundedGT_characterisations α).out 1 2

Equivalence of Sup-Finite Compactness and Sup-Closed Compactness in Complete Lattices

Informal description

For a complete lattice $\alpha$, the following two conditions are equivalent: 1. $\alpha$ is sup-finite compact (i.e., for every subset $s \subseteq \alpha$, there exists a finite subset $t \subseteq s$ such that $\bigvee s = \bigvee t$). 2. $\alpha$ is sup-closed compact (i.e., every nonempty sup-closed subset $s \subseteq \alpha$ contains its supremum $\bigvee s$).

CompleteLattice.isSupClosedCompact_iff_wellFoundedGT theorem

: IsSupClosedCompact α ↔ WellFoundedGT α

Full source

theorem isSupClosedCompact_iff_wellFoundedGT :
    IsSupClosedCompactIsSupClosedCompact α ↔ WellFoundedGT α :=
  (wellFoundedGT_characterisations α).out 2 0

Equivalence of Sup-Closed Compactness and Well-Foundedness in Complete Lattices

Informal description

A complete lattice $\alpha$ is sup-closed compact if and only if the "greater than" relation $>$ on $\alpha$ is well-founded. Here, sup-closed compact means that every nonempty sup-closed subset $s \subseteq \alpha$ contains its supremum $\bigvee s$, and well-founded means that every non-empty subset of $\alpha$ has a minimal element with respect to $>$.

WellFoundedGT.finite_of_sSupIndep theorem

[WellFoundedGT α] {s : Set α} (hs : sSupIndep s) : s.Finite

Full source

theorem WellFoundedGT.finite_of_sSupIndep [WellFoundedGT α] {s : Set α}
    (hs : sSupIndep s) : s.Finite := by
  classical
    refine Set.not_infinite.mp fun contra => ?_
    obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
    replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
      have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
      obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
      exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
    obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
    replace hs : x ⊓ sSup s = ⊥ := by
      have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
      simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
    apply hx₁
    rw [← hs, eq_comm, inf_eq_left]
    exact le_sSup hx₀

Finiteness of Supremum Independent Sets in Well-Founded Complete Lattices

Informal description

Let $\alpha$ be a complete lattice where the "greater than" relation $>$ is well-founded. For any subset $s \subseteq \alpha$ that is supremum independent (i.e., for every $a \in s$, the element $a$ is disjoint from the supremum of $s \setminus \{a\}$), the set $s$ must be finite.

WellFoundedGT.finite_ne_bot_of_iSupIndep theorem

[WellFoundedGT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥}

Full source

theorem WellFoundedGT.finite_ne_bot_of_iSupIndep [WellFoundedGT α]
    {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥} := by
  refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
  exact WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range

Finiteness of Non-Bottom Indices in Supremum Independent Families in Well-Founded Complete Lattices

Informal description

Let $\alpha$ be a complete lattice where the "greater than" relation $>$ is well-founded. Given an indexed family of elements $t : \iota \to \alpha$ that is supremum independent, the set $\{i \mid t_i \neq \bot\}$ of indices corresponding to non-bottom elements is finite.

WellFoundedGT.finite_of_iSupIndep theorem

[WellFoundedGT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι

Full source

theorem WellFoundedGT.finite_of_iSupIndep [WellFoundedGT α] {ι : Type*}
    {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι :=
  haveI := (WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
  Finite.of_injective_finite_range (ht.injective h_ne_bot)

Finiteness of Index Type for Supremum Independent Families in Well-Founded Complete Lattices

Informal description

Let $\alpha$ be a complete lattice where the "greater than" relation $>$ is well-founded. Given an indexed family of elements $t : \iota \to \alpha$ that is supremum independent (i.e., for each $i \in \iota$, $t_i$ is disjoint from $\bigsqcup_{j \neq i} t_j$) and satisfies $t_i \neq \bot$ for all $i \in \iota$, the index type $\iota$ is finite.

WellFoundedLT.finite_of_sSupIndep theorem

[WellFoundedLT α] {s : Set α} (hs : sSupIndep s) : s.Finite

Full source

theorem WellFoundedLT.finite_of_sSupIndep [WellFoundedLT α] {s : Set α}
    (hs : sSupIndep s) : s.Finite := by
  by_contra inf
  let e := (Infinite.diff inf <| finite_singleton ⊥).to_subtype.natEmbedding
  let a n := ⨆ i ≥ n, (e i).1
  have sup_le n : (e n).1 ⊔ a (n + 1) ≤ a n := sup_le_iff.mpr ⟨le_iSup₂_of_le n le_rfl le_rfl,
    iSup₂_le fun i hi ↦ le_iSup₂_of_le i (n.le_succ.trans hi) le_rfl⟩
  have lt n : a (n + 1) < a n := (Disjoint.right_lt_sup_of_left_ne_bot
    ((hs (e n).2.1).mono_right <| iSup₂_le fun i hi ↦ le_sSup ?_) (e n).2.2).trans_le (sup_le n)
  · exact (RelEmbedding.natGT a lt).not_wellFounded_of_decreasing_seq wellFounded_lt
  exact ⟨(e i).2.1, fun h ↦ n.lt_succ_self.not_le <| hi.trans_eq <| e.2 <| Subtype.val_injective h⟩

Finiteness of Supremum Independent Sets in Well-Founded Complete Lattices

Informal description

Let $\alpha$ be a complete lattice where the "less than" relation $<$ is well-founded. For any supremum independent set $s \subseteq \alpha$ (i.e., for every $a \in s$, the element $a$ is disjoint from the supremum of $s \setminus \{a\}$), the set $s$ is finite.

WellFoundedLT.finite_ne_bot_of_iSupIndep theorem

[WellFoundedLT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥}

Full source

theorem WellFoundedLT.finite_ne_bot_of_iSupIndep [WellFoundedLT α]
    {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥} := by
  refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
  exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

Finiteness of Non-Bottom Indices in Supremum Independent Families for Well-Founded Lattices

Informal description

Let $\alpha$ be a complete lattice with a well-founded strict less-than relation $<$. For any supremum independent family of elements $t : \iota \to \alpha$, the set $\{i \mid t_i \neq \bot\}$ of indices corresponding to non-bottom elements is finite.

WellFoundedLT.finite_of_iSupIndep theorem

[WellFoundedLT α] {ι : Type*} {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι

Full source

theorem WellFoundedLT.finite_of_iSupIndep [WellFoundedLT α] {ι : Type*}
    {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Finite ι :=
  haveI := (WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range).to_subtype
  Finite.of_injective_finite_range (ht.injective h_ne_bot)

Finiteness of Index Set for Non-Bottom Supremum Independent Families in Well-Founded Lattices

Informal description

Let $\alpha$ be a complete lattice with a well-founded strict less-than relation $<$. Given an indexed family of elements $t : \iota \to \alpha$ that is supremum independent (i.e., for every $i \in \iota$, $t_i$ is disjoint from the supremum of the remaining elements $\bigsqcup_{j \neq i} t_j$) and such that $t_i \neq \bot$ for all $i \in \iota$, the index set $\iota$ is finite.

IsCompactlyGenerated structure

(α : Type*) [CompleteLattice α]

Full source

/-- A complete lattice is said to be compactly generated if any
element is the `sSup` of compact elements. -/
class IsCompactlyGenerated (α : Type*) [CompleteLattice α] : Prop where
  /-- In a compactly generated complete lattice,
    every element is the `sSup` of some set of compact elements. -/
  exists_sSup_eq : ∀ x : α, ∃ s : Set α, (∀ x ∈ s, CompleteLattice.IsCompactElement x) ∧ sSup s = x

Compactly generated complete lattice

Informal description

A complete lattice $\alpha$ is said to be *compactly generated* if every element $b \in \alpha$ can be expressed as the supremum of all compact elements that are less than or equal to $b$. In other words, $b = \sup \{ c \in \alpha \mid \text{$c$ is compact and } c \leq b \}$. Equivalently, $\alpha$ is compactly generated if the supremum of all compact elements in $\alpha$ is the top element $\top$.

sSup_compact_le_eq theorem

(b) : sSup {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b

Full source

@[simp]
theorem sSup_compact_le_eq (b) :
    sSup { c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b } = b := by
  rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩
  exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)

Supremum of Compact Elements Below $b$ Equals $b$ in Compactly Generated Lattices

Informal description

For any element $b$ in a compactly generated complete lattice $\alpha$, the supremum of all compact elements $c \in \alpha$ satisfying $c \leq b$ is equal to $b$. In other words, \[ \sup \{ c \in \alpha \mid \text{$c$ is compact and } c \leq b \} = b. \]

sSup_compact_eq_top theorem

: sSup {a : α | CompleteLattice.IsCompactElement a} = ⊤

Full source

@[simp]
theorem sSup_compact_eq_top : sSup { a : α | CompleteLattice.IsCompactElement a } = ⊤ := by
  refine Eq.trans (congr rfl (Set.ext fun x => ?_)) (sSup_compact_le_eq ⊤)
  exact (and_iff_left le_top).symm

Supremum of Compact Elements Equals Top in Compactly Generated Lattices

Informal description

In a compactly generated complete lattice $\alpha$, the supremum of all compact elements is equal to the top element $\top$, i.e., \[ \sup \{ a \in \alpha \mid \text{$a$ is compact} \} = \top. \]

le_iff_compact_le_imp theorem

{a b : α} : a ≤ b ↔ ∀ c : α, CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b

Full source

theorem le_iff_compact_le_imp {a b : α} :
    a ≤ b ↔ ∀ c : α, CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b :=
  ⟨fun ab _ _ ca => le_trans ca ab, fun h => by
    rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]
    exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩⟩

Order Relation via Compact Elements in Compactly Generated Lattices

Informal description

For any elements $a$ and $b$ in a compactly generated complete lattice $\alpha$, the inequality $a \leq b$ holds if and only if for every compact element $c \in \alpha$, if $c \leq a$ then $c \leq b$.

DirectedOn.inf_sSup_eq theorem

(h : DirectedOn (· ≤ ·) s) : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

Full source

/-- This property is sometimes referred to as `α` being upper continuous. -/
theorem DirectedOn.inf_sSup_eq (h : DirectedOn (· ≤ ·) s) : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
  le_antisymm
    (by
      rw [le_iff_compact_le_imp]
      by_cases hs : s.Nonempty
      · intro c hc hcinf
        rw [le_inf_iff] at hcinf
        rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
        rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
        refine (le_inf hcinf.1 cd).trans (le_trans ?_ (le_iSup₂ d ds))
        rfl
      · rw [Set.not_nonempty_iff_eq_empty] at hs
        simp [hs])
    iSup_inf_le_inf_sSup

Meet Distributes Over Directed Suprema in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and $s \subseteq \alpha$ be a directed subset with respect to the order $\leq$. Then for any element $a \in \alpha$, the meet of $a$ with the supremum of $s$ equals the supremum of the meets of $a$ with each element of $s$. In symbols: \[ a \sqcap \bigvee s = \bigvee_{b \in s} (a \sqcap b). \]

DirectedOn.sSup_inf_eq theorem

(h : DirectedOn (· ≤ ·) s) : sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

Full source

/-- This property is sometimes referred to as `α` being upper continuous. -/
protected theorem DirectedOn.sSup_inf_eq (h : DirectedOn (· ≤ ·) s) :
    sSupsSup s ⊓ a = ⨆ b ∈ s, b ⊓ a := by
  simp_rw [inf_comm _ a, h.inf_sSup_eq]

Meet Distributes Over Directed Suprema (Dual Form)

Informal description

Let $\alpha$ be a complete lattice and $s \subseteq \alpha$ be a directed subset with respect to the order $\leq$. Then for any element $a \in \alpha$, the meet of the supremum of $s$ with $a$ equals the supremum of the meets of each element of $s$ with $a$. In symbols: \[ \bigvee s \sqcap a = \bigvee_{b \in s} (b \sqcap a). \]

Directed.inf_iSup_eq theorem

(h : Directed (· ≤ ·) f) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

Full source

protected theorem Directed.inf_iSup_eq (h : Directed (· ≤ ·) f) :
    (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i := by
  rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]

Meet Distributes Over Directed Suprema in Complete Lattices (Indexed Family Version)

Informal description

Let $\alpha$ be a complete lattice and $f : \iota \to \alpha$ be a directed family of elements with respect to the order $\leq$. Then for any element $a \in \alpha$, the meet of $a$ with the supremum of the family $f$ equals the supremum of the meets of $a$ with each element of $f$. In symbols: \[ a \sqcap \bigsqcup_i f_i = \bigsqcup_i (a \sqcap f_i). \]

Directed.iSup_inf_eq theorem

(h : Directed (· ≤ ·) f) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Full source

protected theorem Directed.iSup_inf_eq (h : Directed (· ≤ ·) f) :
    (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a := by
  rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]

Meet Distributes Over Directed Suprema in Complete Lattices (Indexed Family Version)

Informal description

Let $\alpha$ be a complete lattice and $f : \iota \to \alpha$ be a directed family of elements with respect to the order $\leq$. Then for any element $a \in \alpha$, the meet of the supremum of the family $f$ with $a$ equals the supremum of the meets of each element of $f$ with $a$. In symbols: \[ \left(\bigsqcup_i f_i\right) \sqcap a = \bigsqcup_i (f_i \sqcap a). \]

DirectedOn.disjoint_sSup_right theorem

(h : DirectedOn (· ≤ ·) s) : Disjoint a (sSup s) ↔ ∀ ⦃b⦄, b ∈ s → Disjoint a b

Full source

protected theorem DirectedOn.disjoint_sSup_right (h : DirectedOn (· ≤ ·) s) :
    DisjointDisjoint a (sSup s) ↔ ∀ ⦃b⦄, b ∈ s → Disjoint a b := by
  simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]

Disjointness of Element with Directed Supremum is Equivalent to Disjointness with All Elements in the Directed Set

Informal description

Let $\alpha$ be a complete lattice and $s \subseteq \alpha$ be a directed subset with respect to the order $\leq$. Then for any element $a \in \alpha$, $a$ is disjoint from the supremum of $s$ if and only if $a$ is disjoint from every element $b \in s$. In symbols: \[ a \perp \bigvee s \leftrightarrow \forall b \in s, a \perp b. \]

DirectedOn.disjoint_sSup_left theorem

(h : DirectedOn (· ≤ ·) s) : Disjoint (sSup s) a ↔ ∀ ⦃b⦄, b ∈ s → Disjoint b a

Full source

protected theorem DirectedOn.disjoint_sSup_left (h : DirectedOn (· ≤ ·) s) :
    DisjointDisjoint (sSup s) a ↔ ∀ ⦃b⦄, b ∈ s → Disjoint b a := by
  simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]

Disjointness of Directed Supremum with Element is Equivalent to Disjointness of All Elements in the Directed Set

Informal description

Let $\alpha$ be a complete lattice and $s \subseteq \alpha$ be a directed subset with respect to the order $\leq$. Then for any element $a \in \alpha$, the supremum of $s$ is disjoint from $a$ if and only if every element $b \in s$ is disjoint from $a$. In symbols: \[ \bigvee s \perp a \leftrightarrow \forall b \in s, b \perp a. \]

Directed.disjoint_iSup_right theorem

(h : Directed (· ≤ ·) f) : Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i)

Full source

protected theorem Directed.disjoint_iSup_right (h : Directed (· ≤ ·) f) :
    DisjointDisjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i) := by
  simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]

Disjointness with Directed Supremum is Equivalent to Disjointness with All Elements in the Directed Family

Informal description

Let $\alpha$ be a complete lattice and $f : \iota \to \alpha$ be a directed family of elements with respect to the order $\leq$. Then for any element $a \in \alpha$, $a$ is disjoint from the supremum of the family $f$ if and only if $a$ is disjoint from every element $f_i$ in the family. In symbols: \[ a \perp \bigsqcup_i f_i \leftrightarrow \forall i, a \perp f_i. \]

Directed.disjoint_iSup_left theorem

(h : Directed (· ≤ ·) f) : Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a

Full source

protected theorem Directed.disjoint_iSup_left (h : Directed (· ≤ ·) f) :
    DisjointDisjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a := by
  simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]

Disjointness of Directed Supremum with Element is Equivalent to Disjointness of All Elements in the Directed Family

Informal description

Let $\alpha$ be a complete lattice and $f : \iota \to \alpha$ be a directed family of elements with respect to the order $\leq$. Then for any element $a \in \alpha$, the supremum of the family $f$ is disjoint from $a$ if and only if every element $f_i$ in the family is disjoint from $a$. In symbols: \[ \left(\bigsqcup_i f_i\right) \perp a \leftrightarrow \forall i, f_i \perp a. \]

inf_sSup_eq_iSup_inf_sup_finset theorem

: a ⊓ sSup s = ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ t.sup id

Full source

/-- This property is equivalent to `α` being upper continuous. -/
theorem inf_sSup_eq_iSup_inf_sup_finset :
    a ⊓ sSup s = ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ t.sup id :=
  le_antisymm
    (by
      rw [le_iff_compact_le_imp]
      intro c hc hcinf
      rw [le_inf_iff] at hcinf
      rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
      refine (le_inf hcinf.1 ht2).trans (le_trans ?_ (le_iSup₂ t ht1))
      rfl)
    (iSup_le fun t =>
      iSup_le fun h => inf_le_inf_left _ ((Finset.sup_id_eq_sSup t).symm ▸ sSup_le_sSup h))

Inf-Sup Distributivity via Finite Approximations in Complete Lattices

Informal description

For any element $a$ in a complete lattice $\alpha$ and any subset $s \subseteq \alpha$, the infimum of $a$ with the supremum of $s$ is equal to the supremum of the infima of $a$ with the suprema of all finite subsets of $s$. In other words: \[ a \sqcap \bigvee s = \bigsqcup_{\substack{t \subseteq s \\ t \text{ finite}}} (a \sqcap \bigvee t) \]

sSupIndep_iff_finite theorem

{s : Set α} : sSupIndep s ↔ ∀ t : Finset α, ↑t ⊆ s → sSupIndep (↑t : Set α)

Full source

theorem sSupIndep_iff_finite {s : Set α} :
    sSupIndepsSupIndep s ↔
      ∀ t : Finset α, ↑t ⊆ s → sSupIndep (↑t : Set α) :=
  ⟨fun hs _ ht => hs.mono ht, fun h a ha => by
    rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot]
    intro t
    rw [iSup_eq_bot, Finset.sup_id_eq_sSup]
    intro ht
    classical
      have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
      · rwa [Finset.coe_insert, Set.insert_diff_self_of_not_mem] at h'
        exact fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a)
      · rw [Finset.coe_insert, Set.insert_subset_iff]
        exact ⟨ha, Set.Subset.trans ht diff_subset⟩⟩

Supremum Independence via Finite Subsets: $s$ is supremum independent $\leftrightarrow$ all finite $t \subseteq s$ are supremum independent

Informal description

A set $s$ in a complete lattice $\alpha$ is supremum independent if and only if every finite subset $t \subseteq s$ is supremum independent. In other words, $s$ is supremum independent precisely when all its finite subsets are supremum independent.

iSupIndep_iff_supIndep_of_injOn theorem

{ι : Type*} {f : ι → α} (hf : InjOn f {i | f i ≠ ⊥}) : iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Full source

lemma iSupIndep_iff_supIndep_of_injOn {ι : Type*} {f : ι → α}
    (hf : InjOn f {i | f i ≠ ⊥}) :
    iSupIndepiSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f := by
  refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  classical
  rw [← Finset.sup_erase_bot]
  set t := s.erase ⊥
  replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
  have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t := by
    ext a
    simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq, Finset.mem_insert, true_or, not_true,
      Finset.erase_insert_eq_erase, not_and, Finset.mem_image, t]
    refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
    obtain ⟨j, hj, rfl⟩ := hs has
    exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
  rw [← this, Finset.sup_image]
  specialize h (insert i (t.preimage _ hf))
  rw [Finset.supIndep_iff_disjoint_erase] at h
  exact h i (Finset.mem_insert_self i _)

Characterization of Supremum Independence via Finite Restrictions for Injective Non-Bottom Elements

Informal description

Let $\alpha$ be a complete lattice and $f : \iota \to \alpha$ be a function. If $f$ is injective on the set $\{i \mid f(i) \neq \bot\}$, then $f$ is supremum independent if and only if for every finite subset $s \subseteq \iota$, the restriction of $f$ to $s$ is supremum independent on $s$.

sSupIndep_iUnion_of_directed theorem

{η : Type*} {s : η → Set α} (hs : Directed (· ⊆ ·) s) (h : ∀ i, sSupIndep (s i)) : sSupIndep (⋃ i, s i)

Full source

theorem sSupIndep_iUnion_of_directed {η : Type*} {s : η → Set α}
    (hs : Directed (· ⊆ ·) s) (h : ∀ i, sSupIndep (s i)) :
    sSupIndep (⋃ i, s i) := by
  by_cases hη : Nonempty η
  · rw [sSupIndep_iff_finite]
    intro t ht
    obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht
    obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset
    exact (h i).mono
        (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
  · rintro a ⟨_, ⟨i, _⟩, _⟩
    exfalso
    exact hη ⟨i⟩

Directed Union Preserves Supremum Independence in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and $\{s_i\}_{i \in \eta}$ be a directed family of subsets of $\alpha$ with respect to inclusion. If each $s_i$ is supremum independent, then their union $\bigcup_{i \in \eta} s_i$ is also supremum independent.

iSupIndep_sUnion_of_directed theorem

{s : Set (Set α)} (hs : DirectedOn (· ⊆ ·) s) (h : ∀ a ∈ s, sSupIndep a) : sSupIndep (⋃₀ s)

Full source

theorem iSupIndep_sUnion_of_directed {s : Set (Set α)} (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, sSupIndep a) : sSupIndep (⋃₀ s) := by
  rw [Set.sUnion_eq_iUnion]
  exact sSupIndep_iUnion_of_directed hs.directed_val (by simpa using h)

Directed Union Preserves Supremum Independence in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice and $s$ be a directed family of subsets of $\alpha$ with respect to inclusion. If every subset in $s$ is supremum independent, then the union $\bigcup₀ s$ is also supremum independent.

CompleteLattice.isCompactlyGenerated_of_wellFoundedGT theorem

[h : WellFoundedGT α] : IsCompactlyGenerated α

Full source

theorem isCompactlyGenerated_of_wellFoundedGT [h : WellFoundedGT α] :
    IsCompactlyGenerated α := by
  rw [wellFoundedGT_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h
  -- x is the join of the set of compact elements {x}
  exact ⟨fun x => ⟨{x}, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩

Well-founded complete lattices are compactly generated

Informal description

If a complete lattice $\alpha$ has a well-founded "greater than" relation $>$, then $\alpha$ is compactly generated. That is, every element $b \in \alpha$ can be expressed as the supremum of all compact elements that are less than or equal to $b$.

CompleteLattice.Iic_coatomic_of_compact_element theorem

{k : α} (h : IsCompactElement k) : IsCoatomic (Set.Iic k)

Full source

/-- A compact element `k` has the property that any `b < k` lies below a "maximal element below
`k`", which is to say `[⊥, k]` is coatomic. -/
theorem Iic_coatomic_of_compact_element {k : α} (h : IsCompactElement k) :
    IsCoatomic (Set.Iic k) := by
  constructor
  rintro ⟨b, hbk⟩
  obtain rfl | H := eq_or_ne b k
  · left; ext; simp only [Set.Iic.coe_top, Subtype.coe_mk]
  right
  have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)
  · refine ⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩
    cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le
    exact lt_irrefl _ hck
  · intro S SC cC I _
    by_cases hS : S.Nonempty
    · refine ⟨sSup S, h.directed_sSup_lt_of_lt hS cC.directedOn SC, ?_⟩
      intro; apply le_sSup
    exact
      ⟨b, lt_of_le_of_ne hbk H, by
        simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
          forall_prop_of_false, not_false_iff]⟩

Coatomicity of the Interval Below a Compact Element in a Complete Lattice

Informal description

For any compact element $k$ in a complete lattice $\alpha$, the interval $(-\infty, k]$ is coatomic, meaning that for every element $x < k$ in this interval, there exists a coatom $m$ (a maximal element strictly below $k$) such that $x \leq m < k$.

CompleteLattice.coatomic_of_top_compact theorem

(h : IsCompactElement (⊤ : α)) : IsCoatomic α

Full source

theorem coatomic_of_top_compact (h : IsCompactElement (⊤ : α)) : IsCoatomic α :=
  (@OrderIso.IicTop α _ _).isCoatomic_iff.mp (Iic_coatomic_of_compact_element h)

Coatomicity from Compactness of Top Element in Complete Lattices

Informal description

If the top element $\top$ of a complete lattice $\alpha$ is compact, then $\alpha$ is coatomic. That is, for every element $x \neq \top$ in $\alpha$, there exists a coatom $m$ (a maximal element strictly below $\top$) such that $x \leq m < \top$.

isAtomic_of_complementedLattice instance

[ComplementedLattice α] : IsAtomic α

Full source

instance (priority := 100) isAtomic_of_complementedLattice [ComplementedLattice α] : IsAtomic α :=
  ⟨fun b => by
    by_cases h : { c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
    · left
      rw [← sSup_compact_le_eq b, sSup_eq_bot]
      exact h
    · rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩
      right
      have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
      rw [← isAtomic_iff_isCoatomic] at hc'
      haveI := hc'
      obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
      · exfalso
        apply hcbot
        simp only [Subtype.ext_iff, Set.Iic.coe_bot, Subtype.coe_mk] at con
        exact con
      rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac
      exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩⟩

Complemented Lattices are Atomic

Informal description

Every complemented lattice is atomic. That is, in a complemented lattice $\alpha$ (a bounded lattice where every element has a complement), every non-bottom element has an atom below it.

isAtomistic_of_complementedLattice instance

[ComplementedLattice α] : IsAtomistic α

Full source

/-- See [Lemma 5.1][calugareanu]. -/
instance (priority := 100) isAtomistic_of_complementedLattice [ComplementedLattice α] :
    IsAtomistic α :=
  CompleteLattice.isAtomistic_iff.2 fun b =>
    ⟨{ a | IsAtom a ∧ a ≤ b }, by
      symm
      have hle : sSup { a : α | IsAtom a ∧ a ≤ b } ≤ b := sSup_le fun _ => And.right
      apply (lt_or_eq_of_le hle).resolve_left _
      intro con
      obtain ⟨c, hc⟩ := exists_isCompl (⟨sSup { a : α | IsAtom a ∧ a ≤ b }, hle⟩ : Set.Iic b)
      obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c
      · exact ne_of_lt con (Subtype.ext_iff.1 (eq_top_of_isCompl_bot hc))
      · apply ha.1
        rw [eq_bot_iff]
        apply le_trans (le_inf _ hac) hc.disjoint.le_bot
        rw [← Subtype.coe_le_coe, Subtype.coe_mk]
        exact le_sSup ⟨ha.of_isAtom_coe_Iic, a.2⟩, fun _ => And.left⟩

Complemented Lattices are Atomistic

Informal description

Every complemented lattice is atomistic. That is, in a complemented lattice $\alpha$ (a bounded lattice where every element has a complement), every element is the supremum of a set of atoms.

exists_sSupIndep_isCompl_sSup_atoms theorem

 (h : sSup {a : α | IsAtom a} = ⊤) (b : α) : ∃ s : Set α, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a

Full source

/-- In an atomic lattice, every element `b` has a complement of the form `sSup s`, where each
element of `s` is an atom. See also `complementedLattice_of_sSup_atoms_eq_top`. -/
theorem exists_sSupIndep_isCompl_sSup_atoms (h : sSup { a : α | IsAtom a } = ⊤) (b : α) :
    ∃ s : Set α, sSupIndep s ∧
    IsCompl b (sSup s) ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a := by
  -- porting note(https://github.com/leanprover-community/mathlib4/issues/5732):
  -- `obtain` chokes on the placeholder.
  have zorn := zorn_subset
    (S := {s : Set α | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a})
    fun c hc1 hc2 =>
      ⟨⋃₀ c,
        ⟨iSupIndep_sUnion_of_directed hc2.directedOn fun s hs => (hc1 hs).1, ?_,
          fun a ⟨s, sc, as⟩ => (hc1 sc).2.2 a as⟩,
        fun _ => Set.subset_sUnion_of_mem⟩
  swap
  · rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
    · rintro _ ⟨s, hs, rfl⟩
      exact (hc1 hs).2.1
    · rw [directedOn_image]
      exact hc2.directedOn.mono @fun s t => sSup_le_sSup
  simp_rw [maximal_subset_iff] at zorn
  obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn
  refine ⟨s, s_ind, ⟨b_inf_Sup_s, ?_⟩, s_atoms⟩
  rw [codisjoint_iff_le_sup, ← h, sSup_le_iff]
  intro a ha
  rw [← inf_eq_left]
  refine (ha.le_iff.mp inf_le_left).resolve_left fun con => ha.1 ?_
  rw [← con, eq_comm, inf_eq_left]
  refine (le_sSup ?_).trans le_sup_right
  rw [← disjoint_iff] at con
  have a_dis_Sup_s : Disjoint a (sSup s) := con.mono_right le_sup_right
  rw [s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left]
  · exact Set.mem_union_right _ (Set.mem_singleton _)
  · rw [sSup_union, sSup_singleton]
    exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm
  · rw [Set.mem_union, Set.mem_singleton_iff] at hx
    obtain rfl | xa := eq_or_ne x a
    · simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
      exact con.mono_right ((sSup_le_sSup Set.diff_subset).trans le_sup_right)
    · have h : (s ∪ {a}) \ {x} = s \ {x}s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_diff_of_not_mem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa
      rw [h, sSup_union, sSup_singleton]
      apply
        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
          (a_dis_Sup_s.mono_right _).symm
      rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
  · rw [Set.mem_union, Set.mem_singleton_iff] at hx
    obtain hx | rfl := hx
    · exact s_atoms x hx
    · exact ha

Existence of Complement as Supremum of Independent Atoms in Atomistic Lattices

Informal description

Let $\alpha$ be a complete lattice where the supremum of all atoms is the top element $\top$. Then for any element $b \in \alpha$, there exists a supremum-independent set $s \subseteq \alpha$ such that: 1. $b$ and $\sup s$ are complements (i.e., $b \sqcup (\sup s) = \top$ and $b \sqcap (\sup s) = \bot$), 2. Every element of $s$ is an atom.

exists_sSupIndep_of_sSup_atoms_eq_top theorem

 (h : sSup {a : α | IsAtom a} = ⊤) : ∃ s : Set α, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a

Full source

theorem exists_sSupIndep_of_sSup_atoms_eq_top (h : sSup { a : α | IsAtom a } = ⊤) :
    ∃ s : Set α, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a :=
  let ⟨s, s_ind, s_top, s_atoms⟩ := exists_sSupIndep_isCompl_sSup_atoms h ⊥
  ⟨s, s_ind, eq_top_of_isCompl_bot s_top.symm, s_atoms⟩

Existence of Independent Atom Set with Supremum Top in Atomistic Lattices

Informal description

Let $\alpha$ be a complete lattice where the supremum of all atoms is the top element $\top$. Then there exists a supremum-independent set $s \subseteq \alpha$ such that: 1. $\sup s = \top$, 2. Every element of $s$ is an atom.

complementedLattice_of_sSup_atoms_eq_top theorem

(h : sSup {a : α | IsAtom a} = ⊤) : ComplementedLattice α

Full source

/-- See [Theorem 6.6][calugareanu]. -/
theorem complementedLattice_of_sSup_atoms_eq_top (h : sSup { a : α | IsAtom a } = ⊤) :
    ComplementedLattice α :=
  ⟨fun b =>
    let ⟨s, _, s_top, _⟩ := exists_sSupIndep_isCompl_sSup_atoms h b
    ⟨sSup s, s_top⟩⟩

Complemented Lattice from Supremum of Atoms Being Top

Informal description

Let $\alpha$ be a complete lattice where the supremum of all atoms is the top element $\top$. Then $\alpha$ is a complemented lattice, meaning every element has a complement.

complementedLattice_of_isAtomistic theorem

[IsAtomistic α] : ComplementedLattice α

Full source

/-- See [Theorem 6.6][calugareanu]. -/
theorem complementedLattice_of_isAtomistic [IsAtomistic α] : ComplementedLattice α :=
  complementedLattice_of_sSup_atoms_eq_top sSup_atoms_eq_top

Atomistic Lattices are Complemented

Informal description

Every atomistic lattice $\alpha$ is complemented. That is, for every element $x \in \alpha$, there exists an element $y \in \alpha$ such that $x \sqcup y = \top$ and $x \sqcap y = \bot$, where $\sqcup$ and $\sqcap$ denote the join and meet operations respectively, and $\top$ and $\bot$ are the top and bottom elements of the lattice.

complementedLattice_iff_isAtomistic theorem

: ComplementedLattice α ↔ IsAtomistic α

Full source

theorem complementedLattice_iff_isAtomistic : ComplementedLatticeComplementedLattice α ↔ IsAtomistic α := by
  constructor <;> intros
  · exact isAtomistic_of_complementedLattice
  · exact complementedLattice_of_isAtomistic

Complemented Lattice Characterization via Atomistic Property

Informal description

A complete lattice $\alpha$ is a complemented lattice if and only if it is atomistic. That is, every element in $\alpha$ has a complement if and only if every element in $\alpha$ is the supremum of a set of atoms.

Mathlib.Order.CompactlyGenerated.Basic

Main definitions

Main results

References

Tags