Products and coproducts in the category of topological spaces

@[inline, reducible]

abbrev TopCat.piπ {ι : Type v} (α : ι → TopCatMax) (i : ι) : TopCat.of ((i : ι) → ↑(α i)) ⟶ α i

The projection from the product as a bundled continuous map.

@[simp]

theorem TopCat.piFan_pt {ι : Type v} (α : ι → TopCatMax) : (TopCat.piFan α).pt = TopCat.of ((i : ι) → ↑(α i))

@[simp]

theorem TopCat.piFan_π_app {ι : Type v} (α : ι → TopCatMax) (X : CategoryTheory.Discrete ι) : (TopCat.piFan α).π.app X = TopCat.piπ α X.as

def TopCat.piFan {ι : Type v} (α : ι → TopCatMax) : CategoryTheory.Limits.Fan α

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

def TopCat.piFanIsLimit {ι : Type v} (α : ι → TopCatMax) : CategoryTheory.Limits.IsLimit (TopCat.piFan α)

The constructed fan is indeed a limit

def TopCat.piIsoPi {ι : Type v} (α : ι → TopCatMax) : ∏ α ≅ TopCat.of ((i : ι) → ↑(α i))

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

@[simp]

theorem TopCat.piIsoPi_inv_π_assoc {ι : Type v} (α : ι → TopCatMax) (i : ι) {Z : TopCatMax} (h : α i ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.piIsoPi α).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π α i) h) = CategoryTheory.CategoryStruct.comp (TopCat.piπ α i) h

@[simp]

theorem TopCat.piIsoPi_inv_π {ι : Type v} (α : ι → TopCatMax) (i : ι) : CategoryTheory.CategoryStruct.comp (TopCat.piIsoPi α).inv (CategoryTheory.Limits.Pi.π α i) = TopCat.piπ α i

@[simp]

theorem TopCat.piIsoPi_inv_π_apply {ι : Type v} (α : ι → TopCatMax) (i : ι) (x : (i : ι) → ↑(α i)) : ↑(CategoryTheory.Limits.Pi.π α i) (↑(TopCat.piIsoPi α).inv x) = x i

@[simp]

theorem TopCat.piIsoPi_hom_apply {ι : Type v} (α : ι → TopCatMax) (i : ι) (x : ↑(∏ α)) : ↑(TopCat.piIsoPi α).hom x i = ↑(CategoryTheory.Limits.Pi.π α i) x

@[inline, reducible]

abbrev TopCat.sigmaι {ι : Type v} (α : ι → TopCatMax) (i : ι) : α i ⟶ TopCat.of ((i : ι) × ↑(α i))

The inclusion to the coproduct as a bundled continuous map.

@[simp]

theorem TopCat.sigmaCofan_pt {ι : Type v} (α : ι → TopCatMax) : (TopCat.sigmaCofan α).pt = TopCat.of ((i : ι) × ↑(α i))

@[simp]

theorem TopCat.sigmaCofan_ι_app {ι : Type v} (α : ι → TopCatMax) (X : CategoryTheory.Discrete ι) : (TopCat.sigmaCofan α).ι.app X = TopCat.sigmaι α X.as

def TopCat.sigmaCofan {ι : Type v} (α : ι → TopCatMax) : CategoryTheory.Limits.Cofan α

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

def TopCat.sigmaCofanIsColimit {ι : Type v} (β : ι → TopCatMax) : CategoryTheory.Limits.IsColimit (TopCat.sigmaCofan β)

The constructed cofan is indeed a colimit

def TopCat.sigmaIsoSigma {ι : Type v} (α : ι → TopCatMax) : ∐ α ≅ TopCat.of ((i : ι) × ↑(α i))

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

@[simp]

theorem TopCat.sigmaIsoSigma_hom_ι_assoc {ι : Type v} (α : ι → TopCatMax) (i : ι) {Z : TopCatMax} (h : TopCat.of ((i : ι) × ↑(α i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i) (CategoryTheory.CategoryStruct.comp (TopCat.sigmaIsoSigma α).hom h) = CategoryTheory.CategoryStruct.comp (TopCat.sigmaι α i) h

@[simp]

theorem TopCat.sigmaIsoSigma_hom_ι {ι : Type v} (α : ι → TopCatMax) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i) (TopCat.sigmaIsoSigma α).hom = TopCat.sigmaι α i

@[simp]

theorem TopCat.sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ι → TopCatMax) (i : ι) (x : ↑(α i)) : ↑(TopCat.sigmaIsoSigma α).hom (↑(CategoryTheory.Limits.Sigma.ι α i) x) = { fst := i, snd := x }

@[simp]

theorem TopCat.sigmaIsoSigma_inv_apply {ι : Type v} (α : ι → TopCatMax) (i : ι) (x : ↑(α i)) : ↑(TopCat.sigmaIsoSigma α).inv { fst := i, snd := x } = ↑(CategoryTheory.Limits.Sigma.ι α i) x

theorem TopCat.induced_of_isLimit {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TopCatMax} (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C) : C.pt.str = ⨅ (j : J), TopologicalSpace.induced (↑(C.π.app j)) (F.obj j).str

theorem TopCat.limit_topology {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : (CategoryTheory.Limits.limit F).str = ⨅ (j : J), TopologicalSpace.induced (↑(CategoryTheory.Limits.limit.π F j)) (F.obj j).str

@[inline, reducible]

abbrev TopCat.prodFst {X : TopCat} {Y : TopCat} : TopCat.of (↑X × ↑Y) ⟶ X

The first projection from the product.

@[inline, reducible]

abbrev TopCat.prodSnd {X : TopCat} {Y : TopCat} : TopCat.of (↑X × ↑Y) ⟶ Y

The second projection from the product.

def TopCat.prodBinaryFan (X : TopCat) (Y : TopCat) : CategoryTheory.Limits.BinaryFan X Y

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

def TopCat.prodBinaryFanIsLimit (X : TopCat) (Y : TopCat) : CategoryTheory.Limits.IsLimit (TopCat.prodBinaryFan X Y)

The constructed binary fan is indeed a limit

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.

@[simp]

theorem TopCat.prodIsoProd_hom_fst_assoc (X : TopCat) (Y : TopCat) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.prodIsoProd X 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 (TopCat.prodIsoProd X 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 (TopCat.prodIsoProd X 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 (TopCat.prodIsoProd X Y).hom TopCat.prodSnd = CategoryTheory.Limits.prod.snd

@[simp]

theorem TopCat.prodIsoProd_hom_apply {X : TopCat} {Y : TopCat} (x : ↑(X ⨯ Y)) : ↑(TopCat.prodIsoProd X 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 (TopCat.prodIsoProd X 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 : (CategoryTheory.forget TopCat).obj (TopCat.of (↑X × ↑Y))) : ↑CategoryTheory.Limits.prod.fst (↑(TopCat.prodIsoProd X Y).inv x) = ↑TopCat.prodFst x

@[simp]

theorem TopCat.prodIsoProd_inv_fst (X : TopCat) (Y : TopCat) : CategoryTheory.CategoryStruct.comp (TopCat.prodIsoProd X 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 (TopCat.prodIsoProd X 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 : (CategoryTheory.forget TopCat).obj (TopCat.of (↑X × ↑Y))) : ↑CategoryTheory.Limits.prod.snd (↑(TopCat.prodIsoProd X Y).inv x) = ↑TopCat.prodSnd x

@[simp]

theorem TopCat.prodIsoProd_inv_snd (X : TopCat) (Y : TopCat) : CategoryTheory.CategoryStruct.comp (TopCat.prodIsoProd X 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) : Set.range ↑(CategoryTheory.Limits.prod.map f g) = ↑CategoryTheory.Limits.prod.fst ⁻¹' Set.range ↑f ∩ ↑CategoryTheory.Limits.prod.snd ⁻¹' Set.range ↑g

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) : Inducing ↑(CategoryTheory.Limits.prod.map f g)

theorem TopCat.embedding_prod_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Embedding ↑f) (hg : Embedding ↑g) : Embedding ↑(CategoryTheory.Limits.prod.map f g)

def TopCat.binaryCofan (X : TopCat) (Y : TopCat) : CategoryTheory.Limits.BinaryCofan X Y

The binary coproduct cofan in TopCat.

def TopCat.binaryCofanIsColimit (X : TopCat) (Y : TopCat) : CategoryTheory.Limits.IsColimit (TopCat.binaryCofan X Y)

The constructed binary coproduct cofan in TopCat is the coproduct.

theorem TopCat.binaryCofan_isColimit_iff {X : TopCat} {Y : TopCat} (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ OpenEmbedding ↑(CategoryTheory.Limits.BinaryCofan.inl c) ∧ OpenEmbedding ↑(CategoryTheory.Limits.BinaryCofan.inr c) ∧ IsCompl (Set.range ↑(CategoryTheory.Limits.BinaryCofan.inl c)) (Set.range ↑(CategoryTheory.Limits.BinaryCofan.inr c))