Created
October 6, 2023 09:01
-
-
Save alreadydone/40333872e072abc8125dd95d20f07f2c to your computer and use it in GitHub Desktop.
A free and properly discontinuous action induces a covering map.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 _ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment