import Mathlib
open Set SetRel Filter
def UniformSpace.generateFrom {α : Type*} (u : Filter (α × α)) : UniformSpace α :=
.ofCore {
uniformity := {
sets := {s | ∃ seq : Nat → SetRel α α, seq 0 = s ∧
∀ i, (seq i).IsRefl ∧ (seq i).symmetrize ∈ u ∧ seq (i + 1) ○ seq (i + 1) ⊆ seq i}
univ_sets := ⟨fun _ => Set.univ, by simp [isRefl_univ, SetRel.symmetrize]⟩
sets_of_superset := by
intro s t hs hst
obtain ⟨seq, rfl, hseq⟩ := hs
refine ⟨fun n => n.casesOn t fun n => seq (n + 1), rfl, fun i => ?_⟩
cases i with
| zero =>
obtain ⟨_, hu, h⟩ := hseq 0
exact ⟨isRefl_mono hst, mem_of_superset hu (SetRel.symmetrize_mono hst), h.trans hst⟩
| succ i => exact hseq (i + 1)
inter_sets := by
intro s t hs ht
obtain ⟨seqs, rfl, hseqs⟩ := hs
obtain ⟨seqt, rfl, hseqt⟩ := ht
refine ⟨fun n => seqs n ∩ seqt n, rfl, fun i => ⟨?_, ?_, ?_⟩⟩
· exact @SetRel.isRefl_inter α (seqs i) (seqt i) (hseqs i).1 (hseqt i).1
· have hs := (hseqs i).2.1
have ht := (hseqt i).2.1
simp_all [SetRel.symmetrize, SetRel.inv]
· exact subset_inter
((comp_subset_comp inter_subset_left inter_subset_left).trans (hseqs i).2.2)
((comp_subset_comp inter_subset_right inter_subset_right).trans (hseqt i).2.2)
}
refl s hs := hs.elim fun seq hseq => @SetRel.id_subset α s (hseq.1 ▸ (hseq.2 0).1)
symm := by
intro s hs
obtain ⟨seq, rfl, hseq⟩ := hs
refine ⟨fun n => (seq n).inv, rfl, fun i => ⟨?_, ?_, ?_⟩⟩
· apply id_subset_iff.1
simpa using inv_mono (id_subset_iff.2 (hseq i).1)
· simpa [SetRel.symmetrize, and_comm] using (hseq i).2.1
· simpa using inv_mono (hseq i).2.2
comp := by
intro s hs
obtain ⟨seq, rfl, hseq⟩ := hs
refine mem_of_superset (mem_lift' ?_) (hseq 0).2.2
exact ⟨fun n => seq (n + 1), rfl, fun i => hseq (i + 1)⟩
}
theorem UniformSpace.mem_uniformity_generateFrom {α : Type*} (u : Filter (α × α))
(s : SetRel α α) : s ∈ @uniformity α (.generateFrom u) ↔
∃ seq : Nat → SetRel α α, seq 0 = s ∧
∀ i, (seq i).IsRefl ∧ (seq i).symmetrize ∈ u ∧ seq (i + 1) ○ seq (i + 1) ⊆ seq i := .rfl
theorem UniformSpace.gc_generateFrom_uniformity {α : Type*} :
GaloisConnection UniformSpace.generateFrom (@uniformity α) := by
apply GaloisConnection.monotone_intro
· simp [Monotone, UniformSpace.le_def]
· intro a b hab s hs
rw [UniformSpace.mem_uniformity_generateFrom] at hs ⊢
obtain ⟨seq, hs, hseq⟩ := hs
exact ⟨seq, hs, fun i => ⟨(hseq i).1, hab (hseq i).2.1, (hseq i).2.2⟩⟩
· intro a s hs
rw [UniformSpace.mem_uniformity_generateFrom] at hs
obtain ⟨seq, rfl, hseq⟩ := hs
exact mem_of_superset (hseq 0).2.1 symmetrize_subset_self
· intro _ s hs
rw [UniformSpace.mem_uniformity_generateFrom]
let seq (n : Nat) : (uniformity α).sets :=
n.rec ⟨s, hs⟩ fun _ ih => ⟨_, (comp_mem_uniformity_sets ih.2).choose_spec.1⟩
refine ⟨fun n => (seq n).1, rfl, fun i => ⟨?_, ?_, ?_⟩⟩
· exact id_subset_iff.1 (refl_le_uniformity (seq i).2)
· exact symmetrize_mem_uniformity (seq i).2
· exact (comp_mem_uniformity_sets (seq i).2).choose_spec.2
def UniformSpace.gi_generateFrom_uniformity {α : Type*} :
GaloisInsertion UniformSpace.generateFrom (@uniformity α) where
choice u hu := .ofCore {
uniformity := u
refl := (@refl_le_uniformity α (.generateFrom u)).trans hu
symm := le_antisymm hu (UniformSpace.gc_generateFrom_uniformity.le_u_l u) ▸
(@tendsto_swap_uniformity α (.generateFrom u))
comp := le_antisymm hu (UniformSpace.gc_generateFrom_uniformity.le_u_l u) ▸
(@comp_le_uniformity α (.generateFrom u))
}
gc := UniformSpace.gc_generateFrom_uniformity
le_l_u _ _ hs := hs.elim fun _ hseq =>
hseq.1 ▸ mem_of_superset (hseq.2 0).2.1 symmetrize_subset_self
choice_eq u hu := UniformSpace.ext
(le_antisymm (UniformSpace.gc_generateFrom_uniformity.le_u_l u) hu)