Basis of open_set

open_set_basis.lean

import category_theory.examples.topological_spaces
import order.lattice order.galois_connection
import category_theory.tactics.obviously

universes u v

open category_theory
open category_theory.examples

namespace open_set
open topological_space lattice

variables {X : Top.{v}}

local attribute [back] topological_space.is_open_inter
local attribute [back] is_open_union
local attribute [back] open_set.is_open

local attribute [back] set.subset_union_left
local attribute [back] set.subset_union_right

local attribute [back'] set.inter_subset_left
local attribute [back'] set.inter_subset_right

@[simp] instance : has_inter (open_set X) :=
{ inter := λ U V, ⟨ U.s ∩ V.s, by obviously ⟩ }

@[simp] instance : has_union (open_set X) :=
{ union := λ U V, ⟨ U.s ∪ V.s, by obviously ⟩ }

def interior (s : set X) : open_set X :=
{ s := interior s,
  is_open := is_open_interior }

def gc : galois_connection (@open_set.s X) interior :=
λ U s, ⟨λ h, interior_maximal h U.is_open, λ h, le_trans h interior_subset⟩

def gi : @galois_insertion (order_dual (set X)) (order_dual (open_set X)) _ _ interior (@open_set.s X) :=
{ choice := λ s _, interior s,
  gc := galois_connection.dual _ _ gc,
  le_l_u := λ _, interior_subset,
  choice_eq := λ _ _, rfl }

instance : partial_order (open_set X) :=
{ le_antisymm := λ U₁ U₂ _ _, by cases U₁; cases U₂; tidy,
   .. open_set.preorder }

instance open_set.lattice.complete_lattice.order_dual : complete_lattice (order_dual (open_set X)) :=
@galois_insertion.lift_complete_lattice (order_dual _) (order_dual _) _ interior (@open_set.s X) _ gi

lemma order_dual_order_dual {α : Type*} : order_dual (order_dual α) = α := rfl

instance : complete_lattice (open_set X) :=
begin
  have foo : complete_lattice (order_dual (order_dual (open_set X))),
  by apply_instance,
  rw order_dual_order_dual at foo,
  exact foo
end

@[simp] lemma top_s : (⊤ : open_set X).s = set.univ :=
begin
  refine le_antisymm (set.subset_univ _) (_),
  change set.univ ≤ (interior ⊤ : order_dual $ open_set X).s,
  dsimp [interior],
  convert le_of_eq interior_univ.symm,
end

@[simp] lemma Lub_s {Us : set (open_set X)} : (⨆ U ∈ Us, U).s = ⋃₀ (open_set.s '' Us) :=
begin
  sorry
end

def is_basis (B : set (open_set X)) : Prop := is_topological_basis (open_set.s '' B)

lemma is_basis_iff₁ {B : set (open_set X)} :
is_basis B ↔ ∀ U : open_set X, ∃ UI ⊆ B, U = ⨆ Ui ∈ UI, Ui :=
begin
  split,
  { intros hB U,
    sorry },
  { intro h,
    split,
    { sorry },
    split,
    { rcases h ⊤ with ⟨UI,hUI,H⟩,
      apply le_antisymm,
      { intros x hx, exact set.mem_univ x },
      { replace H := congr_arg (@open_set.s X) H,
        rw top_s at H, rw H,
        sorry } },
    { sorry } }
end

def univ : open_set X :=
{ s := set.univ,
  is_open := is_open_univ }

lemma is_basis_iff₂ {B : set (open_set X)} :
is_basis B ↔ ∀ {U : open_set X} {x : X}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ⊆ U :=
begin
split; intro h,
{ rintros ⟨sU, hU⟩ x hx,
  rcases h with ⟨h₁,h₂,h₃⟩,
  dsimp [examples.topological_space] at h₃,
  rw h₃ at hU,
  cases hU,
  { rcases hU_H with ⟨⟨U,H⟩,⟨H₁,H₂⟩⟩,
    dsimp at H₂, subst H₂,
    refine ⟨⟨U, H⟩, H₁, hx, set.subset.refl _⟩ },
  { change x ∈ set.univ at hx,
    rw [← h₂,set.mem_sUnion] at hx,
    rcases hx with ⟨sU,⟨⟨U,H⟩,⟨H₁,H₂⟩⟩,hx⟩,
    dsimp at H₂, subst H₂,
    refine ⟨⟨U, H⟩, H₁, hx, set.subset_univ _⟩ },
  { -- this should be proved by induction
    -- is there an induction principle for generated topologies in mathlib?
    sorry },
  {
    sorry } },
{ split,
  { rintros sU₁ ⟨U₁, hU₁⟩ sU₂ ⟨U₂, hU₂⟩ x hx,
    rw [← hU₁.right, ← hU₂.right] at hx ⊢,
    rcases @h (U₁ ∩ U₂) x hx with ⟨U', hU', ⟨H₁, H₂⟩⟩,
    refine ⟨U'.s, ⟨U', ⟨hU', rfl⟩⟩, ⟨H₁, H₂⟩⟩ },
  { split,
    { ext x, split; intro hx,
      { exact set.mem_univ x },
      { rcases @h open_set.univ x hx with ⟨U, hU, H₁, H₂⟩,
        refine set.mem_sUnion_of_mem H₁ ((set.mem_image _ _ _).mpr ⟨U, hU, rfl⟩) } },
    { apply le_antisymm,
      { intros U hU,
        -- let H := generate_open.sUnion {V | ∃ x ∈ U, V = (@h ⟨U,hU⟩ x)},
        -- tidy,
        sorry },
      { apply generate_from_le_iff_subset_is_open.mpr,
        rintros sU ⟨U, hU⟩,
        rw ← hU.right,
        exact U.is_open } } } }
end

end open_set