Documentation

TauCeti.Topology.Category.TopCat.Quotient

Quotient projections in the category of topological spaces #

The canonical projection to the quotient by a setoid, bundled as a morphism in TopCat, and the open set of the quotient given by the image of an open set closed under the setoid.

source
def TauCeti.TopCat.quotientMk {X : Type u_1} [TopologicalSpace X] (s : Setoid X) :
↧X ⟶ ↧(Quotient s)

The continuous projection from a topological space to its quotient by a setoid.

Instances For
    source
    @[simp]
    theorem TauCeti.TopCat.quotientMk_apply {X : Type u_1} [TopologicalSpace X] (s : Setoid X) (x : X) :
    (CategoryTheory.ConcreteCategory.hom (quotientMk s)) x = ⟦x⟧

    The quotient projection sends a point to its equivalence class.

    source
    def TopologicalSpace.Opens.imageQuotientMk {X : Type u_1} [TopologicalSpace X] {s : Setoid X} (V : Opens X) (hV : ∀ ⦃w v : X⦄, w ∈ V → s w v → v ∈ V) :
    Opens (Quotient s)

    The image of an open set closed under s, as an open set of the quotient by s.

    Instances For
      source
      @[simp]
      theorem TopologicalSpace.Opens.coe_imageQuotientMk {X : Type u_1} [TopologicalSpace X] {s : Setoid X} (V : Opens X) (hV : ∀ ⦃w v : X⦄, w ∈ V → s w v → v ∈ V) :
      ↑(V.imageQuotientMk hV) = Quotient.mk s '' ↑V

      The carrier of V.imageQuotientMk hV is the image of V in the quotient.

      source
      theorem TopologicalSpace.Opens.mem_imageQuotientMk {X : Type u_1} [TopologicalSpace X] {s : Setoid X} (V : Opens X) (hV : ∀ ⦃w v : X⦄, w ∈ V → s w v → v ∈ V) {z : Quotient s} :
      z ∈ V.imageQuotientMk hV ↔ ∃ w ∈ V, ⟦w⟧ = z

      A point of the quotient lies in V.imageQuotientMk hV exactly when it is the class of a point of V.

      source
      @[simp]
      theorem TopologicalSpace.Opens.mk_mem_imageQuotientMk {X : Type u_1} [TopologicalSpace X] {s : Setoid X} (V : Opens X) (hV : ∀ ⦃w v : X⦄, w ∈ V → s w v → v ∈ V) {w : X} :
      ⟦w⟧ ∈ V.imageQuotientMk hV ↔ w ∈ V

      The class of a point lies in the image of an open set closed under s exactly when the point lies in that set.

      source
      @[simp]
      theorem TopologicalSpace.Opens.mem_map_imageQuotientMk {X : Type u_1} [TopologicalSpace X] {s : Setoid X} (V : Opens X) (hV : ∀ ⦃w v : X⦄, w ∈ V → s w v → v ∈ V) {w : X} :
      w ∈ (map (TauCeti.TopCat.quotientMk s)).obj (V.imageQuotientMk hV) ↔ w ∈ V

      The points over the image of an open set closed under s are the points of that set.