QuotientTopology.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Geometry of the component quotient

The quotient is a homeomorphism on the original open domain and has connected inverse images of continua. Together with MooreReduction, this proves the topological quotient lemma of the Koebe manuscript, conditional on the precisely stated published Moore input.

theorem OAI.CircleDomainRigidity.homeomorph_of_component_collapse line 19

Source documentation

A component-collapse quotient restricts to a homeomorphism on the domain.

theorem homeomorph_of_component_collapse
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    (G : Set X) (hG : IsOpen G) (π : X → Y) (hc : Continuous π)
    (hcl : IsClosedMap π) (hs : Function.Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) :
    IsOpen (π '' G) ∧ ∃ e : G ≃ₜ (π '' G), ∀ x, (e x).val = π x.val := by
…

theorem OAI.CircleDomainRigidity.connected_fibers_of_component_collapse line 52

Source documentation

All fibers of a component-collapse quotient are connected.

theorem connected_fibers_of_component_collapse
    {X Y : Type*} [TopologicalSpace X] (G : Set X) (π : X → Y)
    (hs : Function.Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) :
    ∀ y, IsConnected (π ⁻¹' {y}) := by
…

theorem OAI.CircleDomainRigidity.quotientSphere_of_moore line 86

Source documentation

The complete quotient lemma: only the sphere realization is supplied by Moore's published theorem; all other conclusions are derived here.

theorem quotientSphere_of_moore (hMoore : MooreSphereDecomposition)
    {G : Set Sphere} (hopen : IsOpen G) (hconn : IsConnected G) :
    ∃ π : Sphere → Sphere, Continuous π ∧ IsClosedMap π ∧ Function.Surjective π ∧
      (∀ x y, π x = π y ↔
        x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) ∧
      IsOpen (π '' G) ∧ (∃ e : G ≃ₜ (π '' G), ∀ x, (e x).val = π x.val) ∧
      IsCompact (π '' G)ᶜ ∧ IsTotallyDisconnected (π '' G)ᶜ ∧
      (∀ K : Set Sphere, IsClosed K → IsConnected K → IsConnected (π ⁻¹' K)) := by
…

Mentions: OAI.CircleDomainRigidity.MooreSphereDecomposition, OAI.CircleDomainRigidity.Sphere