Quotients gluing only finitely many points

Let s be an equivalence relation on a topological space X which identifies only points of a finite set t: whenever s x y holds with x ≠ y, the point x lies in t. The quotient Quotient s glues finitely many finite sets of points of X together and leaves the rest of X untouched.

The basic example is the topological carrier of a nodal curve: it is the quotient of the normalization by the relation identifying each node flag with its partner. If σ is the involution of the normalization exchanging paired flags and fixing every other point, this is the relation Equiv.Perm.SameCycle.setoid σ, and t is the finite set of points moved by σ (Equiv.Perm.SameCycle.eq_of_left supplies the hypothesis below). The results of this file say that this quotient is a reasonable space: it is Hausdorff when the normalization is, and away from the glued points it is an open copy of the complement of the flags.

Main results

• Setoid.isClosed_setOf_rel: the relation is a closed subset of X × X when X is Hausdorff.
• Setoid.isClosedMap_quotient_mk: the quotient map is closed when X is T₁.
• Setoid.t2Space_quotient: the quotient is Hausdorff when X is.
• Setoid.isOpenEmbedding_domRestrict_quotient_mk: the quotient map restricted to the complement of t is an open embedding when X is T₁; Setoid.image_quotient_mk_compl from TauCeti.Topology.Constructions.Basic identifies its image with the complement of the image of t. This specializes Setoid.isOpenEmbedding_domRestrict_quotient_mk_of_isOpen from the same file.

Compactness of the quotient of a compact space is Mathlib's Quotient.compactSpace.

theorem Setoid.isClosed_setOf_rel {X : Type u_1} (s : Setoid X) {t : Set X} [TopologicalSpace X] (ht : t.Finite) (hst : ∀ ⦃x y : X⦄, s x y → x ≠ y → x ∈ t) [T2Space X] : IsClosed {p : X × X | s p.1 p.2}

If an equivalence relation on a Hausdorff space identifies only points of a finite set, then it is a closed subset of the product.

theorem Setoid.isClosedMap_quotient_mk {X : Type u_1} (s : Setoid X) {t : Set X} [TopologicalSpace X] (ht : t.Finite) (hst : ∀ ⦃x y : X⦄, s x y → x ≠ y → x ∈ t) [T1Space X] : IsClosedMap (Quotient.mk s)

If an equivalence relation on a T₁ space identifies only points of a finite set, then the quotient map is closed.

theorem Setoid.t2Space_quotient {X : Type u_1} (s : Setoid X) {t : Set X} [TopologicalSpace X] (ht : t.Finite) (hst : ∀ ⦃x y : X⦄, s x y → x ≠ y → x ∈ t) [T2Space X] : T2Space (Quotient s)

If an equivalence relation on a Hausdorff space identifies only points of a finite set, then the quotient space is Hausdorff.

theorem Setoid.isOpenEmbedding_domRestrict_quotient_mk {X : Type u_1} (s : Setoid X) {t : Set X} [TopologicalSpace X] (ht : t.Finite) (hst : ∀ ⦃x y : X⦄, s x y → x ≠ y → x ∈ t) [T1Space X] : Topology.IsOpenEmbedding (tᶜ.domRestrict (Quotient.mk s))

If an equivalence relation on a T₁ space identifies only points of a finite set t, then the quotient map restricted to the complement of t is an open embedding.