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.

Equations

• TopCat.piπ α i = ContinuousMap.mk fun (f : ↑(TopCat.of ((i : ι) → ↑(α i)))) => f i

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

Equations

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

def TopCat.piFanIsLimit {ι : Type v} (α : ι → TopCatMax) : 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} (α : ι → TopCatMax) : ∏ α ≅ 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.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor α)) (TopCat.piFanIsLimit α)

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

Equations

• TopCat.sigmaι α i = ContinuousMap.mk (id (Sigma.mk i))

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

Equations

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

def TopCat.sigmaCofanIsColimit {ι : Type v} (β : ι → TopCatMax) : 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} (α : ι → TopCatMax) : ∐ α ≅ TopCat.of ((i : ι) × ↑(α i))

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

Equations

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

@[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.toPrefunctor.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.toPrefunctor.obj j).str

@[inline, reducible]

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

The first projection from the product.

Equations

• TopCat.prodFst = ContinuousMap.mk Prod.fst

@[inline, reducible]

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

The second projection from the product.

Equations

• TopCat.prodSnd = ContinuousMap.mk Prod.snd

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

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

Equations

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

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

The constructed binary fan is indeed a limit

Equations

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

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

• TopCat.prodIsoProd X Y = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair X Y)) (TopCat.prodBinaryFanIsLimit X Y)

@[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).toPrefunctor.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).toPrefunctor.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.

Equations

• TopCat.binaryCofan X Y = CategoryTheory.Limits.BinaryCofan.mk (ContinuousMap.mk Sum.inl) (ContinuousMap.mk Sum.inr)

def TopCat.binaryCofanIsColimit (X : TopCat) (Y : TopCat) : CategoryTheory.Limits.IsColimit (TopCat.binaryCofan X 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 ⇑(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))