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

• TopCat.piπ α i = { toFun := fun (f : ↑(TopCat.of ((i : ι) → ↑(α i)))) => f i, continuous_toFun := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• TopCat.piFan α = CategoryTheory.Limits.Fan.mk (TopCat.of ((i : ι) → ↑(α i))) (TopCat.piπ α)

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

The constructed fan is indeed a limit

Equations

• One or more equations did not get rendered due to their size.

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

• TopCat.piIsoPi α = (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor α)).conePointUniqueUpToIso (TopCat.piFanIsLimit α)

@[simp]

theorem TopCat.piIsoPi_inv_π_assoc {ι : Type v} (α : ι → TopCat) (i : ι) {Z : TopCat} (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} (α : ι → TopCat) (i : ι) : CategoryTheory.CategoryStruct.comp (TopCat.piIsoPi α).inv (CategoryTheory.Limits.Pi.π α i) = TopCat.piπ α i

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

theorem TopCat.piIsoPi_hom_apply {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(∏ᶜ α)) : (TopCat.piIsoPi α).hom x i = (CategoryTheory.Limits.Pi.π α 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

• TopCat.sigmaι α i = { toFun := id (Sigma.mk i), continuous_toFun := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• TopCat.sigmaCofan α = CategoryTheory.Limits.Cofan.mk (TopCat.of ((i : ι) × ↑(α i))) (TopCat.sigmaι α)

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

The constructed cofan is indeed a colimit

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• TopCat.sigmaIsoSigma α = (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor α)).coconePointUniqueUpToIso (TopCat.sigmaCofanIsColimit α)

@[simp]

theorem TopCat.sigmaIsoSigma_hom_ι_assoc {ι : Type v} (α : ι → TopCat) (i : ι) {Z : TopCat} (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} (α : ι → TopCat) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι α i) (TopCat.sigmaIsoSigma α).hom = TopCat.sigmaι α i

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

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

theorem TopCat.induced_of_isLimit {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TopCat} (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 TopCat) : (CategoryTheory.Limits.limit F).str = ⨅ (j : J), TopologicalSpace.induced (⇑(CategoryTheory.Limits.limit.π F j)) (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 := ⋯ }

@[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 := ⋯ }

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

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

Equations

• X.prodBinaryFan Y = CategoryTheory.Limits.BinaryFan.mk TopCat.prodFst TopCat.prodSnd

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

The constructed binary fan is indeed a limit

Equations

• X.prodBinaryFanIsLimit Y = { lift := fun (S : CategoryTheory.Limits.BinaryFan X Y) => { toFun := fun (s : ↑S.pt) => (S.fst s, S.snd s), continuous_toFun := ⋯ }, fac := ⋯, uniq := ⋯ }

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 = (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair X Y)).conePointUniqueUpToIso (X.prodBinaryFanIsLimit Y)

@[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

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 : (CategoryTheory.forget TopCat).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 : (CategoryTheory.forget TopCat).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) : 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.

Equations

• X.binaryCofan Y = CategoryTheory.Limits.BinaryCofan.mk { toFun := Sum.inl, continuous_toFun := ⋯ } { toFun := Sum.inr, continuous_toFun := ⋯ }

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

The constructed binary coproduct cofan in TopCat is the coproduct.

Equations

• One or more equations did not get rendered due to their size.

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