maximal_recognizer_setoid_exists

formal source

 162
 163    This is the dual of Zorn's Lemma (existence of minimal elements):
 164    every chain has a lower bound (the infimum) ⟹ minimal element exists. -/
 165theorem maximal_recognizer_setoid_exists
 166    (P : Set (Setoid C))
 167    (hne : P.Nonempty)
 168    (hchain : ∀ (chain : Set (Setoid C)), chain ⊆ P → chain.Nonempty →
 169      IsChain (· ≤ ·) chain → ∃ lb ∈ P, ∀ s ∈ chain, lb ≤ s) :
 170    ∃ m ∈ P, ∀ s ∈ P, s ≤ m → m ≤ s := by
 171  -- Apply Zorn's Lemma in the ≤ order (where ≤ = "finer")
 172  -- We need: every chain has a lower bound → minimal element exists
 173  -- This is the standard dual Zorn formulation
 174  obtain ⟨m, hmP, hm⟩ := zorn_nonempty_partialOrder₀ P
 175    (fun chain hchain_sub hne_chain hchain_chain => by
 176      obtain ⟨lb, hlb_mem, hlb_bound⟩ := hchain chain.toSet hchain_sub
 177        ⟨hne_chain.some, hne_chain.some.2⟩
 178        (fun a ha b hb hab => hchain_chain ha.2 hb.2 (Subtype.coe_injective.ne hab))
 179      exact ⟨⟨lb, hlb_mem⟩, fun ⟨s, hs⟩ hs_chain => hlb_bound s hs_chain⟩)
 180    hne
 181  exact ⟨m, hmP, fun s hs hle => hm ⟨s, hs⟩ hle⟩
 182
 183/-! ## Section 6: Properties of Maximal Recognizers -/
 184
 185/-- A recognizer is *maximal* in a family if no other member properly refines it. -/
 186def IsMaximalRecognizer {E : Type*} (r : Recognizer C E)
 187    (family : ∀ (E' : Type*), Set (Recognizer C E')) : Prop :=
 188  ∀ (E' : Type*) (r' : Recognizer C E'), r' ∈ family E' →
 189    IsFinerThan r' r → IsFinerThan r r'
 190
 191/-- A maximal recognizer has the property that its resolution cells cannot
 192    be split by any other recognizer in the family. -/
 193theorem maximal_cells_unsplittable {E E' : Type*}
 194    (r : Recognizer C E) (r' : Recognizer C E')
 195    (hmax : IsFinerThan r' r → IsFinerThan r r')