Quotients by setoids and fibre products of topological spaces

This file adds to Mathlib's quotient-topology API for Quotient.mk s, where s : Setoid X, and to the topology of the fibre product Function.Pullback f g, a subspace of the product.

Main results

• Setoid.image_quotient_mk_compl: if s identifies only points of t, the quotient map sends the complement of t onto the complement of the image of t.
• Setoid.isOpen_image_quotient_mk: the image of an open set closed under s is open.
• Setoid.isOpenEmbedding_domRestrict_quotient_mk_of_isOpen: the quotient map restricted to an open set whose points are related only to themselves is an open embedding.
• Function.Pullback.continuous_fst, Function.Pullback.continuous_snd: the projections of the fibre product are continuous.
• ContinuousMap.pullbackFst, ContinuousMap.pullbackSnd: the projections of the fibre product, bundled as continuous maps.

theorem Setoid.image_quotient_mk_compl {X : Type u_1} (s : Setoid X) {t : Set X} (hst : ∀ ⦃x y : X⦄, s x y → x ≠ y → x ∈ t) : Quotient.mk s '' tᶜ = (Quotient.mk s '' t)ᶜ

If an equivalence relation identifies only points of a set t, then the quotient map sends the complement of t onto the complement of the image of t.

theorem Setoid.isOpen_image_quotient_mk {X : Type u_1} (s : Setoid X) [TopologicalSpace X] {U : Set X} (hU : IsOpen U) (hsat : ∀ ⦃x y : X⦄, x ∈ U → s x y → y ∈ U) : IsOpen (Quotient.mk s '' U)

The image in Quotient s of an open set closed under the relation s is open.

theorem Setoid.isOpenEmbedding_domRestrict_quotient_mk_of_isOpen {X : Type u_1} (s : Setoid X) [TopologicalSpace X] {U : Set X} (hU : IsOpen U) (hfix : ∀ ⦃x y : X⦄, x ∈ U → s x y → x = y) : Topology.IsOpenEmbedding (U.domRestrict (Quotient.mk s))

If every point of an open set U is related by s only to itself, then the quotient map restricted to U is an open embedding.

theorem Function.Pullback.continuous_fst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Z] {f : X → Y} {g : Z → Y} : Continuous fst

The projection X ×_Y Z → X is continuous.

theorem Function.Pullback.continuous_snd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Z] {f : X → Y} {g : Z → Y} : Continuous snd

The projection X ×_Y Z → Z is continuous.

def ContinuousMap.pullbackFst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Z] (f : X → Y) (g : Z → Y) : C(Function.Pullback f g, X)

The projection X ×_Y Z → X, bundled as a continuous map.

def ContinuousMap.pullbackSnd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Z] (f : X → Y) (g : Z → Y) : C(Function.Pullback f g, Z)

The projection X ×_Y Z → Z, bundled as a continuous map.

@[simp]

theorem ContinuousMap.coe_pullbackFst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Z] (f : X → Y) (g : Z → Y) : ⇑(pullbackFst f g) = Function.Pullback.fst

@[simp]

theorem ContinuousMap.coe_pullbackSnd {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Z] (f : X → Y) (g : Z → Y) : ⇑(pullbackSnd f g) = Function.Pullback.snd