Mathlib/Order/Closure.lean

Mathlib · fixed commit 360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56

Fixed original declaration · Raw UTF-8 source · Back to the referring Card

1/-2Copyright (c) 2020 Bhavik Mehta. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Bhavik Mehta, Yaël Dillies5-/6module78public import Mathlib.Data.Set.BooleanAlgebra9public import Mathlib.Data.SetLike.Basic10public import Mathlib.Order.Hom.Basic1112/-!13# Closure operators between preorders1415We define (bundled) closure operators on a preorder as monotone (increasing), extensive16(inflationary) and idempotent functions.17We define closed elements for the operator as elements which are fixed by it.1819Lower adjoints to a function between preorders `u : β → α` allow to generalise closure operators to20situations where the closure operator we are dealing with naturally decomposes as `u ∘ l` where `l`21is a worthy function to have on its own. Typical examples include22`l : Set G → Subgroup G := Subgroup.closure`, `u : Subgroup G → Set G := (↑)`, where `G` is a group.23This shows there is a close connection between closure operators, lower adjoints and Galois24connections/insertions: every Galois connection induces a lower adjoint which itself induces a25closure operator by composition (see `GaloisConnection.lowerAdjoint` and26`LowerAdjoint.closureOperator`), and every closure operator on a partial order induces a Galois27insertion from the set of closed elements to the underlying type (see `ClosureOperator.gi`).2829## Main definitions3031* `ClosureOperator`: A closure operator is a monotone function `f : α → α` such that32  `∀ x, x ≤ f x` and `∀ x, f (f x) = f x`.33* `LowerAdjoint`: A lower adjoint to `u : β → α` is a function `l : α → β` such that `l` and `u`34  form a Galois connection.3536## Implementation details3738Although `LowerAdjoint` is technically a generalisation of `ClosureOperator` (by defining39`toFun := id`), it is desirable to have both as otherwise `id`s would be carried all over the40place when using concrete closure operators such as `ConvexHull`.4142`LowerAdjoint` really is a semibundled `structure` version of `GaloisConnection`.4344## References4546* https://en.wikipedia.org/wiki/Closure_operator#Closure_operators_on_partially_ordered_sets47-/4849@[expose] public section5051open Set5253/-! ### Closure operator -/545556variable (α : Type*) {ι : Sort*} {κ : ι → Sort*}5758/-- A closure operator on the preorder `α` is a monotone function which is extensive (every `x`59is less than its closure) and idempotent. -/60structure ClosureOperator [Preorder α] extends α →o α where61  /-- An element is less than or equal its closure -/62  le_closure' : ∀ x, x ≤ toFun x63  /-- Closures are idempotent -/64  idempotent' : ∀ x, toFun (toFun x) = toFun x65  /-- Predicate for an element to be closed.6667  By default, this is defined as `c.IsClosed x := (c x = x)` (see `isClosed_iff`).68  We allow an override to fix definitional equalities. -/69  IsClosed (x : α) : Prop := toFun x = x70  isClosed_iff {x : α} : IsClosed x ↔ toFun x = x := by aesop7172namespace ClosureOperator7374instance [Preorder α] : FunLike (ClosureOperator α) α α where75  coe c := c.176  coe_injective := by rintro ⟨⟩ ⟨⟩ h; obtain rfl := DFunLike.ext' h; congr with x; simp_all7778instance [Preorder α] : OrderHomClass (ClosureOperator α) α α where79  map_rel f _ _ h := f.mono h8081initialize_simps_projections ClosureOperator (toFun → apply, IsClosed → isClosed)828384/-- If `c` is a closure operator on `α` and `e` an order-isomorphism85between `α` and `β` then `e ∘ c ∘ e⁻¹` is a closure operator on `β`. -/86@[simps apply]87def conjBy {α β} [Preorder α] [Preorder β] (c : ClosureOperator α)88    (e : α ≃o β) : ClosureOperator β where89  toFun := e.conj c90  IsClosed b := c.IsClosed (e.symm b)91  monotone' _ _ h :=92    (map_le_map_iff e).mpr <| c.monotone <| (map_le_map_iff e.symm).mpr h93  le_closure' _ := e.symm_apply_le.mp (c.le_closure' _)94  idempotent' _ :=95    congrArg e <| Eq.trans (congrArg c (e.symm_apply_apply _)) (c.idempotent' _)96  isClosed_iff := Iff.trans c.isClosed_iff e.eq_symm_apply9798lemma conjBy_refl {α} [Preorder α] (c : ClosureOperator α) :99    c.conjBy (OrderIso.refl α) = c := rfl100101lemma conjBy_trans {α β γ} [Preorder α] [Preorder β] [Preorder γ]102    (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α) :103    c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂ := rfl104105section Preorder106107variable [Preorder α]108109/-- The identity function as a closure operator. -/110@[simps!]111def id : ClosureOperator α where112  toOrderHom := OrderHom.id113  le_closure' _ := le_rfl114  idempotent' _ := rfl115  IsClosed _ := True116117instance : Inhabited (ClosureOperator α) :=118  ⟨id α⟩119120variable {α} (c : ClosureOperator α)121122@[ext]123theorem ext : ∀ c₁ c₂ : ClosureOperator α, (∀ x, c₁ x = c₂ x) → c₁ = c₂ :=124  DFunLike.ext125126@[gcongr, mono]127theorem monotone : Monotone c :=128  c.monotone'129130/-- Every element is less than its closure. This property is sometimes referred to as extensivity or131inflationarity. -/132theorem le_closure (x : α) : x ≤ c x :=133  c.le_closure' x134135@[simp]136theorem idempotent (x : α) : c (c x) = c x :=137  c.idempotent' x138139@[simp] lemma isClosed_closure (x : α) : c.IsClosed (c x) := c.isClosed_iff.2 <| c.idempotent x140141/-- The type of elements closed under a closure operator. -/142abbrev Closeds := {x // c.IsClosed x}143144/-- Send an element to a closed element (by taking the closure). -/145def toCloseds (x : α) : c.Closeds := ⟨c x, c.isClosed_closure x⟩146147variable {c} {x y : α}148149theorem IsClosed.closure_eq : c.IsClosed x → c x = x := c.isClosed_iff.1150151/-- The set of closed elements for `c` is exactly its range. -/152theorem setOf_isClosed_eq_range_closure : {x | c.IsClosed x} = Set.range c := by153  ext x; exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩154155theorem le_closure_iff : x ≤ c y ↔ c x ≤ c y :=156  ⟨fun h ↦ c.idempotent y ▸ c.monotone h, (c.le_closure x).trans⟩157158@[simp]159theorem IsClosed.closure_le_iff (hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y := by160  rw [← hy.closure_eq, ← le_closure_iff]161162lemma closure_min (hxy : x ≤ y) (hy : c.IsClosed y) : c x ≤ y := hy.closure_le_iff.2 hxy163164lemma closure_isGLB (x : α) : IsGLB { y | x ≤ y ∧ c.IsClosed y } (c x) where165  left _ := and_imp.mpr closure_min166  right _ h := h ⟨c.le_closure x, c.isClosed_closure x⟩167168end Preorder169170section PartialOrder171172variable {α} [PartialOrder α] {c : ClosureOperator α} {x y : α}173174/-- Constructor for a closure operator using the weaker idempotency axiom: `f (f x) ≤ f x`. -/175@[simps]176def mk' (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ x, x ≤ f x) (hf₃ : ∀ x, f (f x) ≤ f x) :177    ClosureOperator α where178  toFun := f179  monotone' := hf₁180  le_closure' := hf₂181  idempotent' x := (hf₃ x).antisymm (hf₁ (hf₂ x))182183/-- Convenience constructor for a closure operator using the weaker minimality axiom:184`x ≤ f y → f x ≤ f y`, which is sometimes easier to prove in practice. -/185@[simps]186def mk₂ (f : α → α) (hf : ∀ x, x ≤ f x) (hmin : ∀ ⦃x y⦄, x ≤ f y → f x ≤ f y) :187    ClosureOperator α where188  toFun := f189  monotone' _ y hxy := hmin (hxy.trans (hf y))190  le_closure' := hf191  idempotent' _ := (hmin le_rfl).antisymm (hf _)192193/-- Construct a closure operator from an inflationary function `f` and a "closedness" predicate `p`194witnessing minimality of `f x` among closed elements greater than `x`. -/195@[simps!]196def ofPred (f : α → α) (p : α → Prop) (hf : ∀ x, x ≤ f x) (hfp : ∀ x, p (f x))197    (hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y) : ClosureOperator α where198  __ := mk₂ f hf fun _ y hxy => hmin hxy (hfp y)199  IsClosed := p200  isClosed_iff := ⟨fun hx ↦ (hmin le_rfl hx).antisymm <| hf _, fun hx ↦ hx ▸ hfp _⟩201202theorem isClosed_iff_closure_le : c.IsClosed x ↔ c x ≤ x :=203  ⟨fun h ↦ h.closure_eq.le, fun h ↦ c.isClosed_iff.2 <| h.antisymm <| c.le_closure x⟩204205theorem ext_isClosed (c₁ c₂ : ClosureOperator α)206    (h : ∀ x, c₁.IsClosed x ↔ c₂.IsClosed x) : c₁ = c₂ :=207  ext c₁ c₂ <| fun x => IsGLB.unique (c₁.closure_isGLB x) <| by simpa [h] using c₂.closure_isGLB x208209/-- A closure operator is equal to the closure operator obtained by feeding `c.closed` into the210`ofPred` constructor. -/211theorem eq_ofPred_closed (c : ClosureOperator α) :212    c = ofPred c c.IsClosed c.le_closure c.isClosed_closure fun _ _ ↦ closure_min := by213  ext214  simp215216end PartialOrder217218variable {α}219220section OrderTop221222variable [PartialOrder α] [OrderTop α] (c : ClosureOperator α)223224@[simp]225theorem closure_top : c ⊤ = ⊤ :=226  le_top.antisymm (c.le_closure _)227228@[simp] lemma isClosed_top : c.IsClosed ⊤ := c.isClosed_iff.2 c.closure_top229230end OrderTop231232theorem closure_inf_le [SemilatticeInf α] (c : ClosureOperator α) (x y : α) :233    c (x ⊓ y) ≤ c x ⊓ c y :=234  c.monotone.map_inf_le _ _235236section SemilatticeSup237238variable [SemilatticeSup α] (c : ClosureOperator α)239240theorem closure_sup_closure_le (x y : α) : c x ⊔ c y ≤ c (x ⊔ y) :=241  c.monotone.le_map_sup _ _242243theorem closure_sup_closure_left (x y : α) : c (c x ⊔ y) = c (x ⊔ y) :=244  le_antisymm245    (le_closure_iff.1 (sup_le (c.monotone le_sup_left) (le_sup_right.trans (c.le_closure _))))246    (by grw [← c.le_closure x])247248theorem closure_sup_closure_right (x y : α) : c (x ⊔ c y) = c (x ⊔ y) := by249  rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]250251theorem closure_sup_closure (x y : α) : c (c x ⊔ c y) = c (x ⊔ y) := by252  rw [closure_sup_closure_left, closure_sup_closure_right]253254end SemilatticeSup255256section CompleteLattice257258variable [CompleteLattice α] (c : ClosureOperator α)259260/-- Define a closure operator from a predicate that's preserved under infima. -/261@[simps!]262def ofCompletePred (p : α → Prop) (hsinf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : ClosureOperator α :=263  ofPred (fun a ↦ ⨅ b : {b // a ≤ b ∧ p b}, b) p264    (fun a ↦ by simp +contextual)265    (fun _ ↦ hsinf _ <| forall_mem_range.2 fun b ↦ b.2.2)266    (fun _ b hab hb ↦ iInf_le_of_le ⟨b, hab, hb⟩ le_rfl)267268theorem sInf_isClosed {c : ClosureOperator α} {S : Set α}269    (H : ∀ x ∈ S, c.IsClosed x) : c.IsClosed (sInf S) :=270  isClosed_iff_closure_le.mpr <| le_of_le_of_eq c.monotone.map_sInf_le <|271    Eq.trans (biInf_congr (c.isClosed_iff.mp <| H · ·)) sInf_eq_iInf.symm272273@[simp]274theorem closure_iSup_closure (f : ι → α) : c (⨆ i, c (f i)) = c (⨆ i, f i) :=275  le_antisymm (le_closure_iff.1 <| iSup_le fun i => c.monotone <| le_iSup f i) <|276    c.monotone <| iSup_mono fun _ => c.le_closure _277278@[simp]279theorem closure_iSup₂_closure (f : ∀ i, κ i → α) :280    c (⨆ (i) (j), c (f i j)) = c (⨆ (i) (j), f i j) :=281  le_antisymm (le_closure_iff.1 <| iSup₂_le fun i j => c.monotone <| le_iSup₂ i j) <|282    c.monotone <| iSup₂_mono fun _ _ => c.le_closure _283284end CompleteLattice285286end ClosureOperator287288set_option linter.style.whitespace false in -- manual alignment is not recognised289/-- Conjugating `ClosureOperators` on `α` and on `β` by a fixed isomorphism290`e : α ≃o β` gives an equivalence `ClosureOperator α ≃ ClosureOperator β`. -/291@[simps apply symm_apply]292def OrderIso.equivClosureOperator {α β} [Preorder α] [Preorder β] (e : α ≃o β) :293    ClosureOperator α ≃ ClosureOperator β where294  toFun     c := c.conjBy e295  invFun    c := c.conjBy e.symm296  left_inv  c := Eq.trans (c.conjBy_trans _ _).symm297                 <| Eq.trans (congrArg _ e.self_trans_symm) c.conjBy_refl298  right_inv c := Eq.trans (c.conjBy_trans _ _).symm299                 <| Eq.trans (congrArg _ e.symm_trans_self) c.conjBy_refl300301/-! ### Lower adjoint -/302303304variable {α} {β : Type*}305306/-- A lower adjoint of `u` on the preorder `α` is a function `l` such that `l` and `u` form a Galois307connection. It allows us to define closure operators whose output does not match the input. In308practice, `u` is often `(↑) : β → α`. -/309structure LowerAdjoint [Preorder α] [Preorder β] (u : β → α) where310  /-- The underlying function -/311  toFun : α → β312  /-- The underlying function is a lower adjoint. -/313  gc' : GaloisConnection toFun u314315namespace LowerAdjoint316317variable (α)318319/-- The identity function as a lower adjoint to itself. -/320@[simps]321protected def id [Preorder α] : LowerAdjoint (id : α → α) where322  toFun x := x323  gc' := GaloisConnection.id324325variable {α}326327instance [Preorder α] : Inhabited (LowerAdjoint (id : α → α)) :=328  ⟨LowerAdjoint.id α⟩329330section Preorder331332variable [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u)333334instance : CoeFun (LowerAdjoint u) fun _ => α → β where coe := toFun335336theorem gc : GaloisConnection l u :=337  l.gc'338339@[ext]340theorem ext : ∀ l₁ l₂ : LowerAdjoint u, (l₁ : α → β) = (l₂ : α → β) → l₁ = l₂341  | ⟨l₁, _⟩, ⟨l₂, _⟩, h => by342    congr343344@[gcongr, mono]345theorem monotone : Monotone (u ∘ l) :=346  l.gc.monotone_u.comp l.gc.monotone_l347348/-- Every element is less than its closure. This property is sometimes referred to as extensivity or349inflationarity. -/350theorem le_closure (x : α) : x ≤ u (l x) :=351  l.gc.le_u_l _352353end Preorder354355section PartialOrder356357variable [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u)358359/-- Every lower adjoint induces a closure operator given by the composition. This is the partial360order version of the statement that every adjunction induces a monad. -/361@[simps]362def closureOperator : ClosureOperator α where363  toFun x := u (l x)364  monotone' := l.monotone365  le_closure' := l.le_closure366  idempotent' x := l.gc.u_l_u_eq_u (l x)367368theorem idempotent (x : α) : u (l (u (l x))) = u (l x) :=369  l.closureOperator.idempotent _370371theorem le_closure_iff (x y : α) : x ≤ u (l y) ↔ u (l x) ≤ u (l y) :=372  l.closureOperator.le_closure_iff373374end PartialOrder375376section Preorder377378variable [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u)379380/-- An element `x` is closed for `l : LowerAdjoint u` if it is a fixed point: `u (l x) = x` -/381def closed : Set α := {x | u (l x) = x}382383theorem mem_closed_iff (x : α) : x ∈ l.closed ↔ u (l x) = x :=384  Iff.rfl385386theorem closure_eq_self_of_mem_closed {x : α} (h : x ∈ l.closed) : u (l x) = x :=387  h388389end Preorder390391section PartialOrder392393variable [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u)394395theorem mem_closed_iff_closure_le (x : α) : x ∈ l.closed ↔ u (l x) ≤ x :=396  l.closureOperator.isClosed_iff_closure_le397398@[simp]399theorem closure_is_closed (x : α) : u (l x) ∈ l.closed :=400  l.idempotent x401402/-- The set of closed elements for `l` is the range of `u ∘ l`. -/403theorem closed_eq_range_close : l.closed = Set.range (u ∘ l) :=404  l.closureOperator.setOf_isClosed_eq_range_closure405406/-- Send an `x` to an element of the set of closed elements (by taking the closure). -/407def toClosed (x : α) : l.closed :=408  ⟨u (l x), l.closure_is_closed x⟩409410@[simp]411theorem closure_le_closed_iff_le (x : α) {y : α} (hy : y ∈ l.closed) : u (l x) ≤ y ↔ x ≤ y :=412  (show l.closureOperator.IsClosed y from hy).closure_le_iff413414end PartialOrder415416theorem closure_top [PartialOrder α] [OrderTop α] [Preorder β] {u : β → α} (l : LowerAdjoint u) :417    u (l ⊤) = ⊤ :=418  l.closureOperator.closure_top419420theorem closure_inf_le [SemilatticeInf α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :421    u (l (x ⊓ y)) ≤ u (l x) ⊓ u (l y) :=422  l.closureOperator.closure_inf_le x y423424section SemilatticeSup425426variable [SemilatticeSup α] [Preorder β] {u : β → α} (l : LowerAdjoint u)427428theorem closure_sup_closure_le (x y : α) : u (l x) ⊔ u (l y) ≤ u (l (x ⊔ y)) :=429  l.closureOperator.closure_sup_closure_le x y430431theorem closure_sup_closure_left (x y : α) : u (l (u (l x) ⊔ y)) = u (l (x ⊔ y)) :=432  l.closureOperator.closure_sup_closure_left x y433434theorem closure_sup_closure_right (x y : α) : u (l (x ⊔ u (l y))) = u (l (x ⊔ y)) :=435  l.closureOperator.closure_sup_closure_right x y436437theorem closure_sup_closure (x y : α) : u (l (u (l x) ⊔ u (l y))) = u (l (x ⊔ y)) :=438  l.closureOperator.closure_sup_closure x y439440end SemilatticeSup441442section CompleteLattice443444variable [CompleteLattice α] [Preorder β] {u : β → α} (l : LowerAdjoint u)445446theorem closure_iSup_closure (f : ι → α) : u (l (⨆ i, u (l (f i)))) = u (l (⨆ i, f i)) :=447  l.closureOperator.closure_iSup_closure _448449theorem closure_iSup₂_closure (f : ∀ i, κ i → α) :450    u (l <| ⨆ (i) (j), u (l <| f i j)) = u (l <| ⨆ (i) (j), f i j) :=451  l.closureOperator.closure_iSup₂_closure _452453end CompleteLattice454455-- Lemmas for `LowerAdjoint ((↑) : α → Set β)`, where `SetLike α β`456section CoeToSet457458variable [SetLike α β]459460section Preorder461462variable [Preorder α] (l : LowerAdjoint ((↑) : α → Set β))463464theorem subset_closure (s : Set β) : s ⊆ l s :=465  l.le_closure s466467theorem notMem_of_notMem_closure {s : Set β} {P : β} (hP : P ∉ l s) : P ∉ s := fun h =>468  hP (subset_closure _ s h)469470theorem le_iff_subset (s : Set β) (S : α) : l s ≤ S ↔ s ⊆ S :=471  l.gc s S472473theorem mem_iff (s : Set β) (x : β) : x ∈ l s ↔ ∀ S : α, s ⊆ S → x ∈ S := by474  simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]475  exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩476477theorem closure_union_closure_subset (x y : α) : (l x : Set β) ∪ l y ⊆ l (x ∪ y) :=478  l.closure_sup_closure_le x y479480@[simp]481theorem closure_union_closure_left (x y : α) : l (l x ∪ y) = l (x ∪ y) :=482  SetLike.coe_injective (l.closure_sup_closure_left x y)483484@[simp]485theorem closure_union_closure_right (x y : α) : l (x ∪ l y) = l (x ∪ y) :=486  SetLike.coe_injective (l.closure_sup_closure_right x y)487488theorem closure_union_closure (x y : α) : l (l x ∪ l y) = l (x ∪ y) := by489  rw [closure_union_closure_right, closure_union_closure_left]490491@[simp]492theorem closure_iUnion_closure (f : ι → α) : l (⋃ i, l (f i)) = l (⋃ i, f i) :=493  SetLike.coe_injective <| l.closure_iSup_closure _494495@[simp]496theorem closure_iUnion₂_closure (f : ∀ i, κ i → α) :497    l (⋃ (i) (j), l (f i j)) = l (⋃ (i) (j), f i j) :=498  SetLike.coe_injective <| l.closure_iSup₂_closure _499500end Preorder501502section PartialOrder503504variable [PartialOrder α] (l : LowerAdjoint ((↑) : α → Set β))505506theorem eq_of_le {s : Set β} {S : α} (h₁ : s ⊆ S) (h₂ : S ≤ l s) : l s = S :=507  ((l.le_iff_subset _ _).2 h₁).antisymm h₂508509end PartialOrder510511end CoeToSet512513end LowerAdjoint514515/-! ### Translations between `GaloisConnection`, `LowerAdjoint`, `ClosureOperator` -/516517/-- Every Galois connection induces a lower adjoint. -/518@[simps]519def GaloisConnection.lowerAdjoint [Preorder α] [Preorder β] {l : α → β} {u : β → α}520    (gc : GaloisConnection l u) : LowerAdjoint u where521  toFun := l522  gc' := gc523524/-- Every Galois connection induces a closure operator given by the composition. This is the partial525order version of the statement that every adjunction induces a monad. -/526@[simps!]527def GaloisConnection.closureOperator [PartialOrder α] [Preorder β] {l : α → β} {u : β → α}528    (gc : GaloisConnection l u) : ClosureOperator α :=529  gc.lowerAdjoint.closureOperator530531/-- The set of closed elements has a Galois insertion to the underlying type. -/532def ClosureOperator.gi [PartialOrder α] (c : ClosureOperator α) :533    GaloisInsertion c.toCloseds (↑) where534  choice x hx := ⟨x, isClosed_iff_closure_le.2 hx⟩535  gc _ y := y.2.closure_le_iff536  le_l_u _ := c.le_closure _537  choice_eq x hx := le_antisymm (c.le_closure x) hx538539/-- The Galois insertion associated to a closure operator can be used to reconstruct the closure540operator.541Note that the inverse in the opposite direction does not hold in general. -/542@[simp]543theorem closureOperator_gi_self [PartialOrder α] (c : ClosureOperator α) :544    c.gi.gc.closureOperator = c := by545  ext x546  rfl