A free and properly discontinuous action induces a covering map.

ProperlyDiscontinuous_CoveringMap.lean

import Mathlib.Topology.Covering
import Mathlib.Topology.Instances.AddCircle

open Topology

variable {E X A : Type*} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A]

/- Note: WeaklyLocallyCompact + T2 actually implies LocallyCompact. -/
@[to_additive] lemma coveringMulAction_of_properlyDiscontinuousSMul {Γ T}
    [TopologicalSpace T] [SMul Γ T] (cont : ∀ g : Γ, Continuous (fun t : T ↦ g • t))
    [ProperlyDiscontinuousSMul Γ T] [WeaklyLocallyCompactSpace T] [T2Space T] (t : T) :
    ∃ U ∈ 𝓝 t, ∀ g : Γ, (g • ·) '' U ∩ U ≠ ∅ → g • t = t := by
  obtain ⟨V, V_cpt, V_nhd⟩ := exists_compact_mem_nhds t
  let Γ₀ := {g : Γ | (g • ·) '' V ∩ V ≠ ∅ ∧ g • t ≠ t}
  have : Γ₀.Finite := (finite_disjoint_inter_image (Γ := Γ) V_cpt V_cpt).subset (fun _ ↦ And.left)
  let W' := V \ (· • t) '' Γ₀
  have htW' : W' ∈ 𝓝 t := Filter.diff_mem V_nhd
    ((this.image _).isClosed.isOpen_compl.mem_nhds fun ⟨g, hg, hgt⟩ ↦ hg.2 hgt)
  obtain ⟨W, htW, hWW', cpt_W⟩ := local_compact_nhds htW'
  refine ⟨W \ ⋃ g ∈ Γ₀, (g • ·) ⁻¹' W, Filter.diff_mem htW <| ((this.isClosed_biUnion fun g _ ↦
    (cpt_W.isClosed).preimage <| cont g).isOpen_compl).mem_nhds fun h ↦ ?_, fun g hg ↦ ?_⟩
  · obtain ⟨g, hg, hgW⟩ := Set.mem_iUnion₂.mp h
    exact (hWW' hgW).2 ⟨g, hg, rfl⟩
  · by_contra hgt
    obtain ⟨t₀, ht₀⟩ := Set.nonempty_iff_ne_empty.mpr hg
    obtain ⟨t₁, ⟨-, ht₁⟩, rfl⟩ := ht₀.1
    refine ht₁ (Set.mem_iUnion₂.mpr ⟨g, ⟨Set.nonempty_iff_ne_empty.mp ?_, hgt⟩, ht₀.2.1⟩)
    obtain ⟨⟨t₂, ⟨ht₂, -⟩, ht₁₂⟩, ht₀, -⟩ := ht₀
    exact ⟨g • t₁, ⟨t₂, (hWW' ht₂).1, ht₁₂⟩, (hWW' ht₀).1⟩

/- already in mathlib -/
lemma continuousOn_prod_of_discrete_right [DiscreteTopology A] {f : X × A → E} {s : Set (X × A)} :
    ContinuousOn f s ↔ ∀ a, ContinuousOn (f ⟨·, a⟩) {x | (x, a) ∈ s} := by
  simp_rw [ContinuousOn, Prod.forall, ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete,
    Filter.prod_pure, ← Filter.map_inf_principal_preimage]; apply forall_swap

@[to_additive]
lemma QuotientMap.trivialization_of_mulAction {G} [TopologicalSpace G] [DiscreteTopology G]
    [Group G] [MulAction G E] (cont : ∀ g : G, Continuous (fun e : E ↦ g • e))
    {p : E → X} (hp : QuotientMap p) (hpG : ∀ {e₁ e₂}, p e₁ = p e₂ ↔ e₁ ∈ MulAction.orbit G e₂)
    (U : Set E) (hoU : IsOpen U) (hU : ∀ g : G, (g • ·) '' U ∩ U ≠ ∅ → g = 1) :
    ∃ t : Trivialization G p, t.baseSet = p '' U := by
  simp_rw [← Set.nonempty_iff_ne_empty] at hU
  have inj_U : U.InjOn p
  · intro e₁ h₁ e₂ h₂ he; obtain ⟨g, rfl⟩ := hpG.mp he
    rw [hU g ⟨_, ⟨e₂, h₂, rfl⟩, h₁⟩]; apply one_smul
  let source := ⋃ g : G, (g • ·) ⁻¹' U
  have h_source : ∀ e ∈ source, ∃! g : G, g • e ∈ U
  · intro e ⟨_, ⟨g, rfl⟩, hg⟩
    refine ⟨g, hg, fun g' hg' ↦ mul_inv_eq_one.mp (hU _ ⟨g' • e, ⟨g • e, hg, ?_⟩, hg'⟩)⟩
    dsimp only; rw [mul_smul, inv_smul_smul]
  have preim_im : ∀ V, p ⁻¹' (p '' V) = ⋃ g : G, (g • ·) ⁻¹' V
  · refine fun V ↦ subset_antisymm (fun e ⟨e', heU, he⟩ ↦ ?_) ?_
    · intro e ⟨_, ⟨g, rfl⟩, hg⟩; exact ⟨_, hg, hpG.mpr ⟨g, rfl⟩⟩
    · obtain ⟨g, rfl⟩ := hpG.mp he; exact ⟨_, ⟨g, rfl⟩, heU⟩
  have hpU : p '' U = p '' source
  · simp_rw [← preim_im, Set.image_preimage_eq_of_subset (Set.image_subset_range _ _)]
  choose g hgU uniq using h_source
  choose f hfU hpf using (fun x ↦ id : ∀ x ∈ p '' U, ∃ e ∈ U, p e = x)
  have hfU' : ∀ {g : G} {x} {hx : x ∈ p '' U}, g • g⁻¹ • f x hx ∈ U :=
    fun {g x hx} ↦ by rw [smul_inv_smul]; apply hfU
  have open_source : IsOpen source := isOpen_iUnion fun g ↦ hoU.preimage (cont g)
  have open_pU : IsOpen (p '' U) := by rw [← hp.isOpen_preimage, preim_im]; exact open_source
  classical
  let inv : X → E := fun x ↦ if hx : x ∈ p '' U then f x hx else (hp.surjective x).choose
  have inv_p : U.LeftInvOn inv p
  · intro e he; dsimp only; rw [dif_pos ⟨e, he, rfl⟩]
    exact inj_U (hfU _ ⟨e, he, rfl⟩) he (hpf _ _)
  have cont_inv : ContinuousOn inv (p '' U)
  · refine (continuousOn_open_iff open_pU).mpr fun V hoV ↦ hp.isOpen_preimage.mp ?_
    rw [Set.inter_comm, ← inv_p.image_inter', preim_im]
    exact isOpen_iUnion fun g ↦ (hoV.inter hoU).preimage (cont g)
  let F : LocalEquiv E (X × G); refine
    { toFun := fun e ↦ (p e, if he : e ∈ source then g e he else 1),
      invFun := fun x ↦ x.2⁻¹ • inv x.1,
      source := source,
      target := (p '' U) ×ˢ Set.univ,
      map_source' := fun e he ↦ ⟨hpU ▸ ⟨e, he, rfl⟩, trivial⟩,
      map_target' := fun x ⟨hx, _⟩ ↦ ?_,
      left_inv' := fun e he ↦ ?_,
      right_inv' := fun x hx ↦ ?_ }
  · dsimp only; rw [dif_pos hx]; exact ⟨_, ⟨x.2, rfl⟩, hfU'⟩
  · dsimp only; simp_rw [dif_pos he, hpU, dif_pos (Set.mem_image_of_mem p he), inv_smul_eq_iff]
    exact inj_U (hfU _ _) (hgU _ _) (by rw [hpf, hpG.mpr ⟨_, rfl⟩])
  · dsimp only; rw [dif_pos hx.1, dif_pos ⟨_, ⟨x.2, rfl⟩, hfU'⟩]
    exact Prod.ext (by rw [hpG.mpr ⟨_, rfl⟩, hpf]) (uniq _ _ _ hfU').symm
  let F : LocalHomeomorph E (X × G); refine
    { toLocalEquiv := F,
      open_source := open_source,
      open_target := open_pU.prod isOpen_univ,
      continuous_toFun := hp.continuous.continuousOn.prod (ContinuousAt.continuousOn
        fun e he ↦ continuous_const (b := g e he) |>.continuousAt.congr <| mem_nhds_iff.mpr
        ⟨(g e he • ·) ⁻¹' U, fun e' he' ↦ (uniq _ _ _ ?_).symm, hoU.preimage (cont _), hgU _ _⟩),
      continuous_invFun := ?_ }
  · have : e' ∈ F.source := ⟨_, ⟨_, rfl⟩, he'⟩
    dsimp only; rw [dif_pos this, ← uniq _ this _ he']; apply hgU
  · exact continuousOn_prod_of_discrete_right.mpr fun g ↦
      ((cont g⁻¹).comp_continuousOn cont_inv).congr_mono (fun x _ ↦ rfl) fun x ↦ And.left
  use { toLocalHomeomorph := F,
        baseSet := p '' U,
        open_baseSet := open_pU,
        source_eq := (preim_im U).symm,
        target_eq := rfl,
        proj_toFun := fun _ _ ↦ rfl }

@[to_additive] lemma QuotientMap.isCoveringMapOn_of_mulAction {G} [Group G] [MulAction G E]
    (cont : ∀ g : G, Continuous (fun e : E ↦ g • e))
    [ProperlyDiscontinuousSMul G E] [WeaklyLocallyCompactSpace E] [T2Space E]
    {p : E → X} (hp : QuotientMap p) (hpG : ∀ {e₁ e₂}, p e₁ = p e₂ ↔ e₁ ∈ MulAction.orbit G e₂) :
    IsCoveringMapOn p (p '' {e | MulAction.stabilizer G e = ⊥}) := by
  letI : TopologicalSpace G := ⊥; have : DiscreteTopology G := ⟨rfl⟩
  /- Is there a type synonym to put the discrete topology on a type? -/
  have : ∀ x ∈ p '' {e | MulAction.stabilizer G e = ⊥}, ∃ t : Trivialization G p, x ∈ t.baseSet
  · rintro x ⟨e, he, rfl⟩
    obtain ⟨U, heU, hU⟩ := coveringMulAction_of_properlyDiscontinuousSMul cont e
    have := hp.trivialization_of_mulAction cont hpG (interior U) isOpen_interior (fun g hg ↦ ?_)
    · obtain ⟨t, hpU⟩ := this; use t; rw [hpU]
      exact ⟨e, mem_interior_iff_mem_nhds.mpr heU, rfl⟩
    rw [← Subgroup.mem_bot, ← he]; apply hU; contrapose! hg; exact Set.subset_eq_empty
      (Set.inter_subset_inter (Set.image_subset _ interior_subset) interior_subset) hg
  choose t ht using this
  exact IsCoveringMapOn.mk _ _ (fun _ ↦ G) t ht

@[to_additive] lemma isCoveringMapOn_quotient_of_mulAction {G} [Group G] [MulAction G E]
    (cont : ∀ g : G, Continuous (fun e : E ↦ g • e))
    [ProperlyDiscontinuousSMul G E] [WeaklyLocallyCompactSpace E] [T2Space E] :
    IsCoveringMapOn (Quotient.mk _)
      ((Quotient.mk <| MulAction.orbitRel G E) '' {e | MulAction.stabilizer G e = ⊥}) :=
  QuotientMap.isCoveringMapOn_of_mulAction cont quotientMap_quotient_mk' Quotient.eq''

/- TODO: WeaklyLocallyCompactSpace can be removed; need to bypass ProperlyDiscontinuous for that,
  because ProperlyDiscontinuous → CoveringMap requires LocallyCompact.
  See also: https://math.stackexchange.com/a/1083696/12932 -/
@[to_additive] lemma Subgroup.isCoveringMap {G} [Group G] [TopologicalSpace G] [TopologicalGroup G]
    [T2Space G] [WeaklyLocallyCompactSpace G] (H : Subgroup G) [DiscreteTopology H] :
    IsCoveringMap (QuotientGroup.mk (s := H)) := by
  rw [isCoveringMap_iff_isCoveringMapOn_univ]
  convert ← isCoveringMapOn_quotient_of_mulAction _
  · refine Set.univ_subset_iff.mp fun g' _ ↦ ?_
    obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective g'
    exact ⟨g, eq_bot_iff.mpr fun g' hg' ↦
      Subtype.ext (MulOpposite.unop_injective <| mul_right_eq_self.mp hg'), rfl⟩
  · exact fun _ ↦ continuous_mul_right _
  · apply Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite
    apply Subgroup.tendsto_coe_cofinite_of_discrete
  all_goals infer_instance

theorem isCoveringMap_toAddCircle (p : ℝ) : IsCoveringMap ((↑) : ℝ → AddCircle p) :=
  AddSubgroup.isCoveringMap _