feat(topology/bornology/order): complete lattice of bornologies, generated bornology

[ADedecker]

---

[PatrickMassot]

Anatole, did you consider doing the Galois insertion first and get the complete lattice structure from there? It would start with

import topology.bornology.basic

noncomputable theory

open filter function set

namespace bornology

variables {α β γ : Type*} {b₁ b₂ : bornology α} {s t u v : set α}

-- Put the next four lemmas in bornology.basic

lemma _root_.set.finite.mem_cobounded [b : bornology α] (h : finite s) : sᶜ ∈ cobounded α  :=
begin
  apply le_cofinite α,
  change finite sᶜᶜ,
  simpa using h
end

lemma _root_.set.finite.is_cobounded [b : bornology α] (h : finite s) : is_cobounded sᶜ  :=
h.mem_cobounded

lemma _root_.set.finite.is_bounded [b : bornology α] (h : finite s) : is_bounded s  :=
h.mem_cobounded

lemma cobounded_injective : injective (@cobounded α) :=
λ b₁ b₂ h, by ext; rw h

instance : partial_order (bornology α) := partial_order.lift
  (_ : bornology α → order_dual (filter α)) cobounded_injective

protected lemma le_def : b₁ ≤ b₂ ↔ b₂.cobounded ≤ b₁.cobounded := iff.rfl

protected lemma le_iff : b₁ ≤ b₂ ↔ (∀ s, @is_bounded _ b₁ s → @is_bounded _ b₂ s) :=
begin
  rw [bornology.le_def, ← @comap_id α (@cobounded _ b₂), comap_cobounded_le_iff],
  simp
end

def generate (S : set $ set α) : bornology α :=
{ cobounded := filter.cofinite ⊓ generate (compl '' S),
  le_cofinite := inf_le_left }

variables (α)

lemma gc_generate : 
  galois_connection bornology.generate (λ b : bornology α, {s | @is_bounded α b s}) := 
begin
  intros S b,
  change b.cobounded ≤ _ ⊓  _ ↔ _,
  simp only [le_inf_iff, @le_cofinite α b, true_and, set.le_eq_subset],
  split ; intros h t t_in,
  { exact h (generate_sets.basic ⟨t, t_in, rfl⟩) },
  { induction t_in with V V_in V W V_in hVW hV V W V_in W_in hV hW ; clear t,
    { rw ← compl_compl V,
      apply h,
      rcases V_in with ⟨W, H, rfl⟩,
      erw compl_compl,
      exact H },
    { simp },
    { exact mem_of_superset hV hVW },
    { exact inter_mem hV hW } }
end

lemma monotone_generate : monotone (bornology.generate : set (set α) → bornology α) :=
(gc_generate α).monotone_l

lemma mem_cobounded_iff_of_le {α : Type*} {S : set (set α)} 
  (hS : {s : set α | @is_bounded α (generate S) s} ≤ S) {t : set α} : 
  t ∈ (generate S).cobounded ↔ t ∈ compl '' S :=
begin
  split,
  { letI := generate S,
    intro ht,
    exact ⟨tᶜ, hS (is_bounded_compl_iff.mpr ht), compl_compl t⟩ },
  { rintros ⟨u, u_in, rfl⟩,
    exact mem_inf_of_right (generate_sets.basic ⟨u, u_in, rfl⟩) }
end

lemma gi_generate : 
  galois_insertion bornology.generate (λ b: bornology α, {s | @is_bounded α b s}) := 
{ choice := λ S hS, { cobounded := { sets := compl '' S,
      univ_sets := ⟨∅, hS (@is_bounded_empty α $ generate S), compl_empty⟩,
      sets_of_superset := begin
        simp_rw ← mem_cobounded_iff_of_le hS,
        apply mem_of_superset
      end,
      inter_sets := begin
        simp_rw ← mem_cobounded_iff_of_le hS,
        apply inter_mem
      end },
    le_cofinite := begin
        letI := bornology.generate S,
        rintros t (ht : finite tᶜ),      
        exact ⟨tᶜ, hS ht.is_bounded, compl_compl t⟩
      end },
  gc := gc_generate α,
  le_l_u := begin
    intros b t ht,
    letI := b,
    exact mem_inf_of_right (generate_sets.basic ⟨tᶜ, is_bounded_compl_iff.mpr ht, compl_compl t⟩)
  end,
  choice_eq := begin
    intros S hS,
    ext,
    rw mem_cobounded_iff_of_le hS,
    exact iff.rfl
  end }

instance : complete_lattice (bornology α) :=
(gi_generate α).lift_complete_lattice

lemma is_bounded_Inf_iff {B : set (bornology α)} :
  @is_bounded _ (Inf B) s ↔ ∀ b ∈ B, @is_bounded _ b s :=
begin
  rw show @is_bounded α (Inf B) s ↔ s ∈ ⋂ b ∈ B, {s | @is_bounded α b s}, 
    from set.ext_iff.mp (gc_generate α).u_Inf s,
  simp
end
end bornology

[ADedecker]

I'm tagging this as Work in Progress because I'd like to have answers to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bornology/near/277637053 before going back to this.

[j-loreaux]

@ADedecker did you get the answers you were looking for?