feat(topology/sets/closeds): The coframe of closed sets (#15338)

`coframe (closeds α)`.

src/data/set/lattice.lean

@@ -756,6 +756,12 @@ by simp only [inter_Union]
 lemma Union₂_inter (s : Π i, κ i → set α) (t : set α) : (⋃ i j, s i j) ∩ t = ⋃ i j, s i j ∩ t :=
 by simp_rw Union_inter
 
+lemma union_Inter₂ (s : set α) (t : Π i, κ i → set α) : s ∪ (⋂ i j, t i j) = ⋂ i j, s ∪ t i j :=
+by simp_rw union_Inter
+
+lemma Inter₂_union (s : Π i, κ i → set α) (t : set α) : (⋂ i j, s i j) ∪ t = ⋂ i j, s i j ∪ t :=
+by simp_rw Inter_union
+
 theorem mem_sUnion_of_mem {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :
   x ∈ ⋃₀ S :=
 ⟨t, ht, hx⟩

src/topology/sets/closeds.lean

@@ -17,7 +17,7 @@ For a topological space `α`,
 * `clopens α`: The type of clopen sets.
 -/
 
-open set
+open order order_dual set
 
 variables {ι α β : Type*} [topological_space α] [topological_space β]
 
@@ -43,14 +43,30 @@ lemma closed (s : closeds α) : is_closed (s : set α) := s.closed'
 
 @[simp] lemma coe_mk (s : set α) (h) : (mk s h : set α) = s := rfl
 
-instance : has_sup (closeds α) := ⟨λ s t, ⟨s ∪ t, s.closed.union t.closed⟩⟩
-instance : has_inf (closeds α) := ⟨λ s t, ⟨s ∩ t, s.closed.inter t.closed⟩⟩
-instance : has_top (closeds α) := ⟨⟨univ, is_closed_univ⟩⟩
-instance : has_bot (closeds α) := ⟨⟨∅, is_closed_empty⟩⟩
-
-instance : distrib_lattice (closeds α) :=
-set_like.coe_injective.distrib_lattice _ (λ _ _, rfl) (λ _ _, rfl)
-instance : bounded_order (closeds α) := bounded_order.lift (coe : _ → set α) (λ _ _, id) rfl rfl
+/-- The closure of a set, as an element of `closeds`. -/
+protected def closure (s : set α) : closeds α := ⟨closure s, is_closed_closure⟩
+
+lemma gc : galois_connection closeds.closure (coe : closeds α → set α) :=
+λ s U, ⟨subset_closure.trans, λ h, closure_minimal h U.closed⟩
+
+/-- The galois coinsertion between sets and opens. -/
+def gi : galois_insertion (@closeds.closure α _) coe :=
+{ choice := λ s hs, ⟨s, closure_eq_iff_is_closed.1 $ hs.antisymm subset_closure⟩,
+  gc := gc,
+  le_l_u := λ _, subset_closure,
+  choice_eq := λ s hs, set_like.coe_injective $ subset_closure.antisymm hs }
+
+instance : complete_lattice (closeds α) :=
+complete_lattice.copy (galois_insertion.lift_complete_lattice gi)
+/- le  -/ _ rfl
+/- top -/ ⟨univ, is_closed_univ⟩ rfl
+/- bot -/ ⟨∅, is_closed_empty⟩ (set_like.coe_injective closure_empty.symm)
+/- sup -/ (λ s t, ⟨s ∪ t, s.2.union t.2⟩)
+  (funext $ λ s, funext $ λ t, set_like.coe_injective (s.2.union t.2).closure_eq.symm)
+/- inf -/ (λ s t, ⟨s ∩ t, s.2.inter t.2⟩) rfl
+/- Sup -/ _ rfl
+/- Inf -/ (λ S, ⟨⋂ s ∈ S, ↑s, is_closed_bInter $ λ s _, s.2⟩)
+  (funext $ λ S, set_like.coe_injective Inf_image.symm)
 
 /-- The type of closed sets is inhabited, with default element the empty set. -/
 instance : inhabited (closeds α) := ⟨⊥⟩
@@ -59,6 +75,7 @@ instance : inhabited (closeds α) := ⟨⊥⟩
 @[simp, norm_cast] lemma coe_inf (s t : closeds α) : (↑(s ⊓ t) : set α) = s ∩ t := rfl
 @[simp, norm_cast] lemma coe_top : (↑(⊤ : closeds α) : set α) = univ := rfl
 @[simp, norm_cast] lemma coe_bot : (↑(⊥ : closeds α) : set α) = ∅ := rfl
+@[simp, norm_cast] lemma coe_Inf {S : set (closeds α)} : (↑(Inf S) : set α) = ⋂ i ∈ S, ↑i := rfl
 
 @[simp, norm_cast] lemma coe_finset_sup (f : ι → closeds α) (s : finset ι) :
   (↑(s.sup f) : set α) = s.sup (coe ∘ f) :=
@@ -68,6 +85,29 @@ map_finset_sup (⟨⟨coe, coe_sup⟩, coe_bot⟩ : sup_bot_hom (closeds α) (se
   (↑(s.inf f) : set α) = s.inf (coe ∘ f) :=
 map_finset_inf (⟨⟨coe, coe_inf⟩, coe_top⟩ : inf_top_hom (closeds α) (set α)) _ _
 
+lemma infi_def {ι} (s : ι → closeds α) : (⨅ i, s i) = ⟨⋂ i, s i, is_closed_Inter $ λ i, (s i).2⟩ :=
+by { ext, simp only [infi, coe_Inf, bInter_range], refl }
+
+@[simp] lemma infi_mk {ι} (s : ι → set α) (h : ∀ i, is_closed (s i)) :
+  (⨅ i, ⟨s i, h i⟩ : closeds α) = ⟨⋂ i, s i, is_closed_Inter h⟩ :=
+by simp [infi_def]
+
+@[simp, norm_cast] lemma coe_infi {ι} (s : ι → closeds α) :
+  ((⨅ i, s i : closeds α) : set α) = ⋂ i, s i :=
+by simp [infi_def]
+
+@[simp] lemma mem_infi {ι} {x : α} {s : ι → closeds α} : x ∈ infi s ↔ ∀ i, x ∈ s i :=
+by simp [←set_like.mem_coe]
+
+@[simp] lemma mem_Inf {S : set (closeds α)} {x : α} : x ∈ Inf S ↔ ∀ s ∈ S, x ∈ s :=
+by simp_rw [Inf_eq_infi, mem_infi]
+
+instance : coframe (closeds α) :=
+{ Inf := Inf,
+  infi_sup_le_sup_Inf := λ a s,
+    (set_like.coe_injective $ by simp only [coe_sup, coe_infi, coe_Inf, set.union_Inter₂]).le,
+  ..closeds.complete_lattice }
+
 end closeds
 
 /-- The complement of a closed set as an open set. -/

src/topology/sets/opens.lean

@@ -82,7 +82,7 @@ complete_lattice.copy (galois_coinsertion.lift_complete_lattice gi)
 /- sup -/ (λ U V, ⟨↑U ∪ ↑V, U.2.union V.2⟩) rfl
 /- inf -/ (λ U V, ⟨↑U ∩ ↑V, U.2.inter V.2⟩)
   (funext $ λ U, funext $ λ V, ext (U.2.inter V.2).interior_eq.symm)
-/- Sup -/ _ rfl
+/- Sup -/ (λ S, ⟨⋃ s ∈ S, ↑s, is_open_bUnion $ λ s _, s.2⟩) (funext $ λ S, ext Sup_image.symm)
 /- Inf -/ _ rfl
 
 lemma le_def {U V : opens α} : U ≤ V ↔ (U : set α) ≤ (V : set α) := iff.rfl
@@ -93,8 +93,7 @@ lemma le_def {U V : opens α} : U ≤ V ↔ (U : set α) ≤ (V : set α) := iff
 @[simp, norm_cast] lemma coe_sup (s t : opens α) : (↑(s ⊔ t) : set α) = s ∪ t := rfl
 @[simp, norm_cast] lemma coe_bot : ((⊥ : opens α) : set α) = ∅ := rfl
 @[simp, norm_cast] lemma coe_top : ((⊤ : opens α) : set α) = set.univ := rfl
-@[simp, norm_cast] lemma coe_Sup {S : set (opens α)} : (↑(Sup S) : set α) = ⋃ i ∈ S, ↑i :=
-(@gc α _).l_Sup
+@[simp, norm_cast] lemma coe_Sup {S : set (opens α)} : (↑(Sup S) : set α) = ⋃ i ∈ S, ↑i := rfl
 
 @[simp, norm_cast] lemma coe_finset_sup (f : ι → opens α) (s : finset ι) :
   (↑(s.sup f) : set α) = s.sup (coe ∘ f) :=
@@ -120,7 +119,8 @@ by { ext, simp only [supr, coe_Sup, bUnion_range], refl }
   (⨆ i, ⟨s i, h i⟩ : opens α) = ⟨⋃ i, s i, is_open_Union h⟩ :=
 by { rw supr_def, simp }
 
-@[simp] lemma supr_s {ι} (s : ι → opens α) : ((⨆ i, s i : opens α) : set α) = ⋃ i, s i :=
+@[simp, norm_cast] lemma coe_supr {ι} (s : ι → opens α) :
+  ((⨆ i, s i : opens α) : set α) = ⋃ i, s i :=
 by simp [supr_def]
 
 @[simp] theorem mem_supr {ι} {x : α} {s : ι → opens α} : x ∈ supr s ↔ ∃ i, x ∈ s i :=
@@ -132,7 +132,7 @@ by simp_rw [Sup_eq_supr, mem_supr]
 instance : frame (opens α) :=
 { Sup := Sup,
   inf_Sup_le_supr_inf := λ a s,
-    (ext $ by simp only [coe_inf, supr_s, coe_Sup, set.inter_Union₂]).le,
+    (ext $ by simp only [coe_inf, coe_supr, coe_Sup, set.inter_Union₂]).le,
   ..opens.complete_lattice }
 
 lemma open_embedding_of_le {U V : opens α} (i : U ≤ V) :

src/topology/sheaves/sheaf_condition/equalizer_products.lean

@@ -232,9 +232,9 @@ begin
     exact
     F.map_iso (iso.op
     { hom := hom_of_le
-      (by simp only [supr_s, supr_mk, le_def, subtype.coe_mk, set.le_eq_subset, set.image_Union]),
+      (by simp only [coe_supr, supr_mk, le_def, subtype.coe_mk, set.le_eq_subset, set.image_Union]),
       inv := hom_of_le
-      (by simp only [supr_s, supr_mk, le_def, subtype.coe_mk, set.le_eq_subset,
+      (by simp only [coe_supr, supr_mk, le_def, subtype.coe_mk, set.le_eq_subset,
                      set.image_Union]) }), },
   { ext ⟨j⟩,
     dunfold fork.ι, -- Ugh, it is unpleasant that we need this.

src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

@@ -420,10 +420,13 @@ def inter_union_pullback_cone_lift : s.X ⟶ F.1.obj (op (U ∪ V)) :=
 begin
   let ι : ulift.{v} walking_pair → opens X := λ j, walking_pair.cases_on j.down U V,
   have hι : U ∪ V = supr ι,
-  { ext, split,
+  { ext,
+    rw [opens.coe_supr, set.mem_Union],
+    split,
     { rintros (h|h),
-    exacts [⟨_,⟨_,⟨⟨walking_pair.left⟩,rfl⟩,rfl⟩,h⟩, ⟨_,⟨_,⟨⟨walking_pair.right⟩,rfl⟩,rfl⟩,h⟩] },
-    { rintros ⟨_,⟨_,⟨⟨⟨⟩⟩,⟨⟩⟩,⟨⟩⟩,z⟩, exacts [or.inl z, or.inr z] } },
+      exacts [⟨⟨walking_pair.left⟩, h⟩, ⟨⟨walking_pair.right⟩, h⟩] },
+    { rintro ⟨⟨_ | _⟩, h⟩,
+      exacts [or.inl h, or.inr h] } },
   refine (F.1.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 ι).some.lift
     ⟨s.X, { app := _, naturality' := _ }⟩ ≫ F.1.map (eq_to_hom hι).op,
   { apply opposite.rec,
@@ -464,10 +467,13 @@ def is_limit_pullback_cone : is_limit (inter_union_pullback_cone F U V) :=
 begin
   let ι : ulift.{v} walking_pair → opens X := λ ⟨j⟩, walking_pair.cases_on j U V,
   have hι : U ∪ V = supr ι,
-  { ext, split,
+  { ext,
+    rw [opens.coe_supr, set.mem_Union],
+    split,
     { rintros (h|h),
-    exacts [⟨_,⟨_,⟨⟨walking_pair.left⟩,rfl⟩,rfl⟩,h⟩, ⟨_,⟨_,⟨⟨walking_pair.right⟩,rfl⟩,rfl⟩,h⟩] },
-    { rintros ⟨_,⟨_,⟨⟨⟨⟩⟩,⟨⟩⟩,⟨⟩⟩,z⟩, exacts [or.inl z, or.inr z] } },
+      exacts [⟨⟨walking_pair.left⟩, h⟩, ⟨⟨walking_pair.right⟩, h⟩] },
+    { rintro ⟨⟨_ | _⟩, h⟩,
+      exacts [or.inl h, or.inr h] } },
   apply pullback_cone.is_limit_aux',
   intro s,
   use inter_union_pullback_cone_lift F U V s,