IsMaximalRecognizer

formal source

 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')
 196    (c₁ c₂ : C) (h : Indistinguishable r c₁ c₂) :
 197    -- If r' is finer than r, then r is also finer than r'
 198    -- meaning r and r' have exactly the same resolution cells
 199    IsFinerThan r' r → Indistinguishable r' c₁ c₂ := by
 200  intro hfiner
 201  exact hfiner c₁ c₂ h
 202
 203/-- If a maximal recognizer exists and another recognizer refines it,
 204    they induce the same equivalence relation. -/
 205theorem maximal_unique_setoid {E₁ E₂ : Type*}
 206    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 207    (hfiner : IsFinerThan r₂ r₁)
 208    (hmax : IsFinerThan r₂ r₁ → IsFinerThan r₁ r₂) :
 209    recognizerSetoid r₁ = recognizerSetoid r₂ := by
 210  ext c₁ c₂
 211  exact ⟨fun h => hfiner c₁ c₂ h, fun h => hmax hfiner c₁ c₂ h⟩
 212
 213/-! ## Section 7: Connection to the Complete Lattice
 214
 215The setoids on C form a complete lattice in Mathlib. The recognizer-induced
 216setoids form a sub-meet-semilattice (closed under finite meets via ⊗).