# Products and coproducts in the category of topological spaces #

@[reducible, inline]
abbrev TopCat.piπ {ι : Type v} (α : ιTopCat) (i : ι) :
TopCat.of ((i : ι) → (α i)) α i

The projection from the product as a bundled continuous map.

Equations
• = { toFun := fun (f : (TopCat.of ((i : ι) → (α i)))) => f i, continuous_toFun := }
Instances For
@[simp]
theorem TopCat.piFan_pt {ι : Type v} (α : ιTopCat) :
().pt = TopCat.of ((i : ι) → (α i))
@[simp]
theorem TopCat.piFan_π_app {ι : Type v} (α : ιTopCat) (X : ) :
().app X = TopCat.piπ α X.as
def TopCat.piFan {ι : Type v} (α : ιTopCat) :

The explicit fan of a family of topological spaces given by the pi type.

Equations
Instances For
def TopCat.piFanIsLimit {ι : Type v} (α : ιTopCat) :

The constructed fan is indeed a limit

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.piIsoPi {ι : Type v} (α : ιTopCat) :
α TopCat.of ((i : ι) → (α i))

The product is homeomorphic to the product of the underlying spaces, equipped with the product topology.

Equations
• = .conePointUniqueUpToIso
Instances For
@[simp]
theorem TopCat.piIsoPi_inv_π_assoc {ι : Type v} (α : ιTopCat) (i : ι) {Z : TopCat} (h : α i Z) :
@[simp]
theorem TopCat.piIsoPi_inv_π {ι : Type v} (α : ιTopCat) (i : ι) :
@[simp]
theorem TopCat.piIsoPi_inv_π_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : (i : ι) → (α i)) :
(().inv x) = x i
@[simp]
theorem TopCat.piIsoPi_hom_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : ( α)) :
().hom x i = x
@[reducible, inline]
abbrev TopCat.sigmaι {ι : Type v} (α : ιTopCat) (i : ι) :
α i TopCat.of ((i : ι) × (α i))

The inclusion to the coproduct as a bundled continuous map.

Equations
• = { toFun := id (), continuous_toFun := }
Instances For
@[simp]
theorem TopCat.sigmaCofan_pt {ι : Type v} (α : ιTopCat) :
.pt = TopCat.of ((i : ι) × (α i))
@[simp]
theorem TopCat.sigmaCofan_ι_app {ι : Type v} (α : ιTopCat) (X : ) :
.app X = TopCat.sigmaι α X.as
def TopCat.sigmaCofan {ι : Type v} (α : ιTopCat) :

The explicit cofan of a family of topological spaces given by the sigma type.

Equations
Instances For
def TopCat.sigmaCofanIsColimit {ι : Type v} (β : ιTopCat) :

The constructed cofan is indeed a colimit

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.sigmaIsoSigma {ι : Type v} (α : ιTopCat) :
α TopCat.of ((i : ι) × (α i))

The coproduct is homeomorphic to the disjoint union of the topological spaces.

Equations
• = .coconePointUniqueUpToIso
Instances For
@[simp]
theorem TopCat.sigmaIsoSigma_hom_ι_assoc {ι : Type v} (α : ιTopCat) (i : ι) {Z : TopCat} (h : TopCat.of ((i : ι) × (α i)) Z) :
@[simp]
theorem TopCat.sigmaIsoSigma_hom_ι {ι : Type v} (α : ιTopCat) (i : ι) :
@[simp]
theorem TopCat.sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : (α i)) :
.hom () = i, x
@[simp]
theorem TopCat.sigmaIsoSigma_inv_apply {ι : Type v} (α : ιTopCat) (i : ι) (x : (α i)) :
.inv i, x =
theorem TopCat.induced_of_isLimit {J : Type v} {F : } (C : ) (hC : ) :
C.pt.str = ⨅ (j : J), TopologicalSpace.induced ((C.app j)) (F.obj j).str
theorem TopCat.limit_topology {J : Type v} (F : ) :
.str = ⨅ (j : J), TopologicalSpace.induced () (F.obj j).str
@[reducible, inline]
abbrev TopCat.prodFst {X : TopCat} {Y : TopCat} :
TopCat.of (X × Y) X

The first projection from the product.

Equations
• TopCat.prodFst = { toFun := Prod.fst, continuous_toFun := }
Instances For
@[reducible, inline]
abbrev TopCat.prodSnd {X : TopCat} {Y : TopCat} :
TopCat.of (X × Y) Y

The second projection from the product.

Equations
• TopCat.prodSnd = { toFun := Prod.snd, continuous_toFun := }
Instances For

The explicit binary cofan of X, Y given by X × Y.

Equations
Instances For

The constructed binary fan is indeed a limit

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.prodIsoProd (X : TopCat) (Y : TopCat) :
X Y TopCat.of (X × Y)

The homeomorphism between X ⨯ Y and the set-theoretic product of X and Y, equipped with the product topology.

Equations
• X.prodIsoProd Y = .conePointUniqueUpToIso (X.prodBinaryFanIsLimit Y)
Instances For
@[simp]
theorem TopCat.prodIsoProd_hom_fst_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : X Z) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodFst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
@[simp]
theorem TopCat.prodIsoProd_hom_fst (X : TopCat) (Y : TopCat) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodFst = CategoryTheory.Limits.prod.fst
@[simp]
theorem TopCat.prodIsoProd_hom_snd_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom (CategoryTheory.CategoryStruct.comp TopCat.prodSnd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
@[simp]
theorem TopCat.prodIsoProd_hom_snd (X : TopCat) (Y : TopCat) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodSnd = CategoryTheory.Limits.prod.snd
@[simp]
theorem TopCat.prodIsoProd_hom_apply {X : TopCat} {Y : TopCat} (x : (X Y)) :
(X.prodIsoProd Y).hom x = (CategoryTheory.Limits.prod.fst x, CategoryTheory.Limits.prod.snd x)
@[simp]
theorem TopCat.prodIsoProd_inv_fst_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : X Z) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp TopCat.prodFst h
theorem TopCat.prodIsoProd_inv_fst_apply (X : TopCat) (Y : TopCat) (x : .obj (TopCat.of (X × Y))) :
CategoryTheory.Limits.prod.fst ((X.prodIsoProd Y).inv x) = TopCat.prodFst x
@[simp]
theorem TopCat.prodIsoProd_inv_fst (X : TopCat) (Y : TopCat) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.fst = TopCat.prodFst
@[simp]
theorem TopCat.prodIsoProd_inv_snd_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp TopCat.prodSnd h
theorem TopCat.prodIsoProd_inv_snd_apply (X : TopCat) (Y : TopCat) (x : .obj (TopCat.of (X × Y))) :
CategoryTheory.Limits.prod.snd ((X.prodIsoProd Y).inv x) = TopCat.prodSnd x
@[simp]
theorem TopCat.prodIsoProd_inv_snd (X : TopCat) (Y : TopCat) :
CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.snd = TopCat.prodSnd
theorem TopCat.prod_topology {X : TopCat} {Y : TopCat} :
(X Y).str = TopologicalSpace.induced (CategoryTheory.Limits.prod.fst) X.str TopologicalSpace.induced (CategoryTheory.Limits.prod.snd) Y.str
theorem TopCat.range_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} (f : W Y) (g : X Z) :
= CategoryTheory.Limits.prod.fst ⁻¹' CategoryTheory.Limits.prod.snd ⁻¹'
theorem TopCat.inducing_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {f : W X} {g : Y Z} (hf : Inducing f) (hg : Inducing g) :
theorem TopCat.embedding_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {f : W X} {g : Y Z} (hf : ) (hg : ) :
def TopCat.binaryCofan (X : TopCat) (Y : TopCat) :

The binary coproduct cofan in TopCat.

Equations
Instances For

The constructed binary coproduct cofan in TopCat is the coproduct.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.binaryCofan_isColimit_iff {X : TopCat} {Y : TopCat} (c : ) :
OpenEmbedding c.inl OpenEmbedding c.inr IsCompl (Set.range c.inl) (Set.range c.inr)