English
If T is T2, locally compact, and the action is continuous and properly discontinuous, then the quotient by the action is T2.
Русский
Если T — пространство T2 и локально компактное, и действие непрерывно и правильно дискретно, то фактор-пространство по действию тоже T2.
LaTeX
$$$T2Space (Quotient (MulAction.orbitRel \Gamma T))$$$
Lean4
/-- The quotient by a discontinuous group action of a locally compact t2 space is t2. -/
@[to_additive /-- The quotient by a discontinuous group action of a locally compact t2
space is t2. -/
]
instance (priority := 100) t2Space_of_properlyDiscontinuousSMul_of_t2Space [T2Space T] [LocallyCompactSpace T]
[ContinuousConstSMul Γ T] [ProperlyDiscontinuousSMul Γ T] : T2Space (Quotient (MulAction.orbitRel Γ T)) :=
by
letI := MulAction.orbitRel Γ T
set Q := Quotient (MulAction.orbitRel Γ T)
rw [t2Space_iff_nhds]
let f : T → Q := Quotient.mk'
have f_op : IsOpenMap f := isOpenMap_quotient_mk'_mul
rintro ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀)
change ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), _
have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt Quotient.sound hxy.symm :)
obtain ⟨K₀, hK₀, K₀_in⟩ := exists_compact_mem_nhds x₀
obtain ⟨L₀, hL₀, L₀_in⟩ := exists_compact_mem_nhds y₀
let bad_Γ_set := {γ : Γ | (γ • ·) '' K₀ ∩ L₀ ≠ ∅}
have bad_Γ_finite : bad_Γ_set.Finite := finite_disjoint_inter_image (Γ := Γ) hK₀ hL₀
choose u v hu hv u_v_disjoint using fun γ => t2_separation_nhds (hγx₀y₀ γ)
let U₀₀ := ⋂ γ ∈ bad_Γ_set, (γ • ·) ⁻¹' u γ
let U₀ := U₀₀ ∩ K₀
let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ
let V₀ := V₀₀ ∩ L₀
have U_nhds : f '' U₀ ∈ 𝓝 (f x₀) :=
by
refine f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => ?_) K₀_in)
exact (continuous_const_smul _).continuousAt (hu γ)
have V_nhds : f '' V₀ ∈ 𝓝 (f y₀) :=
f_op.image_mem_nhds (inter_mem ((biInter_mem bad_Γ_finite).mpr fun γ _ => hv γ) L₀_in)
refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, MulAction.disjoint_image_image_iff.2 ?_⟩
rintro x ⟨x_in_U₀₀, x_in_K₀⟩ γ
by_cases H : γ ∈ bad_Γ_set
· exact fun h => (u_v_disjoint γ).le_bot ⟨mem_iInter₂.mp x_in_U₀₀ γ H, mem_iInter₂.mp h.1 γ H⟩
· rintro ⟨-, h'⟩
simp only [bad_Γ_set, image_smul, Classical.not_not, mem_setOf_eq, Ne] at H
exact eq_empty_iff_forall_notMem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩
