ProCGroups.InverseSystems.Utilities
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
import
- Mathlib.Topology.Homeomorph.Lemmas
noncomputable def homeoOfBijectiveCompactToT2
{X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
[CompactSpace X] [T2Space Y] {f : X → Y} (hf : Continuous f)
(hbij : Function.Bijective f) :
X ≃ₜ Y :=
homeoOfEquivCompactToT2 (f := Equiv.ofBijective f hbij) hfA continuous bijection from a compact space to a Hausdorff space is a homeomorphism.
theorem exists_upperBound_finset (hdir : Directed (· ≤ ·) (id : I → I)) :
∀ s : Finset I, s.Nonempty → ∃ j, ∀ i ∈ s, i ≤ jShow proof
by
classical
intro s
refine Finset.induction_on s ?_ ?_
· intro hs
rcases hs with ⟨i, hi⟩
simp only [Finset.notMem_empty] at hi
· intro a s ha ih hs
by_cases hs' : s.Nonempty
· rcases ih hs' with ⟨j, hj⟩
rcases hdir a j with ⟨k, hak, hjk⟩
refine ⟨k, ?_⟩
intro i hi
rw [Finset.mem_insert] at hi
rcases hi with rfl | hi
· exact hak
· exact (hj i hi).trans hjk
· have hs'' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs'
subst hs''
refine ⟨a, ?_⟩
intro i hi
simp only [insert_empty_eq, Finset.mem_singleton] at hi
simp only [hi, le_refl]Proof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□