mathlib3 documentation

topology.category.Top.limits.products

Products and coproducts in the category of topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[reducible]
def Top.pi_π {ι : Type v} (α : ι → Top) (i : ι) :
Top.of (Π (i : ι), ↥(α i)) ⟶ α i

The projection from the product as a bundled continous map.

source
@[simp]
theorem Top.pi_fan_X {ι : Type v} (α : ι → Top) :
(Top.pi_fan α).X = Top.of (Π (i : ι), ↥(α i))
source
def Top.pi_fan {ι : Type v} (α : ι → Top) :
category_theory.limits.fan α

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

Equations
source
@[simp]
theorem Top.pi_fan_π_app {ι : Type v} (α : ι → Top) (X : category_theory.discrete ι) :
(Top.pi_fan α).π.app X = Top.pi_π α X.as
source
def Top.pi_fan_is_limit {ι : Type v} (α : ι → Top) :
category_theory.limits.is_limit (Top.pi_fan α)

The constructed fan is indeed a limit

Equations
source
noncomputable def Top.pi_iso_pi {ι : Type v} (α : ι → Top) :
∏ α ≅ Top.of (Π (i : ι), ↥(α i))

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

Equations
source
@[simp]
theorem Top.pi_iso_pi_inv_π_assoc {ι : Type v} (α : ι → Top) (i : ι) {X' : Top} (f' : α i ⟶ X') :
(Top.pi_iso_pi α).inv ≫ category_theory.limits.pi.π α i ≫ f' = Top.pi_π α i ≫ f'
source
@[simp]
theorem Top.pi_iso_pi_inv_π {ι : Type v} (α : ι → Top) (i : ι) :
(Top.pi_iso_pi α).inv ≫ category_theory.limits.pi.π α i = Top.pi_π α i
source
@[simp]
theorem Top.pi_iso_pi_inv_π_apply {ι : Type v} (α : ι → Top) (i : ι) (x : Π (i : ι), ↥(α i)) :
⇑(category_theory.limits.pi.π α i) (⇑((Top.pi_iso_pi α).inv) x) = x i
source
@[simp]
theorem Top.pi_iso_pi_hom_apply {ι : Type v} (α : ι → Top) (i : ι) (x : ↥∏ α) :
⇑((Top.pi_iso_pi α).hom) x i = ⇑(category_theory.limits.pi.π α i) x
source
@[reducible]
def Top.sigma_ι {ι : Type v} (α : ι → Top) (i : ι) :
α i ⟶ Top.of (Σ (i : ι), ↥(α i))

The inclusion to the coproduct as a bundled continous map.

source
def Top.sigma_cofan {ι : Type v} (α : ι → Top) :
category_theory.limits.cofan α

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

Equations
source
@[simp]
theorem Top.sigma_cofan_X {ι : Type v} (α : ι → Top) :
(Top.sigma_cofan α).X = Top.of (Σ (i : ι), ↥(α i))
source
@[simp]
theorem Top.sigma_cofan_ι_app {ι : Type v} (α : ι → Top) (X : category_theory.discrete ι) :
(Top.sigma_cofan α).ι.app X = Top.sigma_ι α X.as
source
def Top.sigma_cofan_is_colimit {ι : Type v} (α : ι → Top) :
category_theory.limits.is_colimit (Top.sigma_cofan α)

The constructed cofan is indeed a colimit

Equations
source
noncomputable def Top.sigma_iso_sigma {ι : Type v} (α : ι → Top) :
∐ α ≅ Top.of (Σ (i : ι), ↥(α i))

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

Equations
source
@[simp]
theorem Top.sigma_iso_sigma_hom_ι {ι : Type v} (α : ι → Top) (i : ι) :
category_theory.limits.sigma.ι α i ≫ (Top.sigma_iso_sigma α).hom = Top.sigma_ι α i
source
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_assoc {ι : Type v} (α : ι → Top) (i : ι) {X' : Top} (f' : Top.of (Σ (i : ι), ↥(α i)) ⟶ X') :
category_theory.limits.sigma.ι α i ≫ (Top.sigma_iso_sigma α).hom ≫ f' = Top.sigma_ι α i ≫ f'
source
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_apply {ι : Type v} (α : ι → Top) (i : ι) (x : ↥(α i)) :
⇑((Top.sigma_iso_sigma α).hom) (⇑(category_theory.limits.sigma.ι α i) x) = ⟨i, x⟩
source
@[simp]
theorem Top.sigma_iso_sigma_inv_apply {ι : Type v} (α : ι → Top) (i : ι) (x : ↥(α i)) :
⇑((Top.sigma_iso_sigma α).inv) ⟨i, x⟩ = ⇑(category_theory.limits.sigma.ι α i) x
source
theorem Top.induced_of_is_limit {J : Type v} [category_theory.small_category J] {F : J ⥤ Top} (C : category_theory.limits.cone F) (hC : category_theory.limits.is_limit C) :
C.X.topological_space = ⨅ (j : J), topological_space.induced ⇑(C.π.app j) (F.obj j).topological_space
source
theorem Top.limit_topology {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
(category_theory.limits.limit F).topological_space = ⨅ (j : J), topological_space.induced ⇑(category_theory.limits.limit.π F j) (F.obj j).topological_space
source
@[reducible]
def Top.prod_fst {X Y : Top} :
Top.of (↥X × ↥Y) ⟶ X

The first projection from the product.

source
@[reducible]
def Top.prod_snd {X Y : Top} :
Top.of (↥X × ↥Y) ⟶ Y

The second projection from the product.

source
def Top.prod_binary_fan (X Y : Top) :
category_theory.limits.binary_fan X Y

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

Equations
source
def Top.prod_binary_fan_is_limit (X Y : Top) :
category_theory.limits.is_limit (X.prod_binary_fan Y)

The constructed binary fan is indeed a limit

Equations
source
noncomputable def Top.prod_iso_prod (X Y : Top) :
X ⨯ Y ≅ Top.of (↥X × ↥Y)

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

Equations
source
@[simp]
theorem Top.prod_iso_prod_hom_fst (X Y : Top) :
(X.prod_iso_prod Y).hom ≫ Top.prod_fst = category_theory.limits.prod.fst
source
@[simp]
theorem Top.prod_iso_prod_hom_fst_assoc (X Y : Top) {X' : Top} (f' : X ⟶ X') :
(X.prod_iso_prod Y).hom ≫ Top.prod_fst ≫ f' = category_theory.limits.prod.fst ≫ f'
source
@[simp]
theorem Top.prod_iso_prod_hom_snd (X Y : Top) :
(X.prod_iso_prod Y).hom ≫ Top.prod_snd = category_theory.limits.prod.snd
source
@[simp]
theorem Top.prod_iso_prod_hom_snd_assoc (X Y : Top) {X' : Top} (f' : Y ⟶ X') :
(X.prod_iso_prod Y).hom ≫ Top.prod_snd ≫ f' = category_theory.limits.prod.snd ≫ f'
source
@[simp]
theorem Top.prod_iso_prod_hom_apply {X Y : Top} (x : ↥(X ⨯ Y)) :
⇑((X.prod_iso_prod Y).hom) x = (⇑category_theory.limits.prod.fst x, ⇑category_theory.limits.prod.snd x)
source
@[simp]
theorem Top.prod_iso_prod_inv_fst_apply (X Y : Top) (x : ↥(Top.of (↥X × ↥Y))) :
⇑category_theory.limits.prod.fst (⇑((X.prod_iso_prod Y).inv) x) = ⇑Top.prod_fst x
source
@[simp]
theorem Top.prod_iso_prod_inv_fst_assoc (X Y : Top) {X' : Top} (f' : X ⟶ X') :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.fst ≫ f' = Top.prod_fst ≫ f'
source
@[simp]
theorem Top.prod_iso_prod_inv_fst (X Y : Top) :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.fst = Top.prod_fst
source
@[simp]
theorem Top.prod_iso_prod_inv_snd (X Y : Top) :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.snd = Top.prod_snd
source
@[simp]
theorem Top.prod_iso_prod_inv_snd_apply (X Y : Top) (x : ↥(Top.of (↥X × ↥Y))) :
⇑category_theory.limits.prod.snd (⇑((X.prod_iso_prod Y).inv) x) = ⇑Top.prod_snd x
source
@[simp]
theorem Top.prod_iso_prod_inv_snd_assoc (X Y : Top) {X' : Top} (f' : Y ⟶ X') :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.snd ≫ f' = Top.prod_snd ≫ f'
source
theorem Top.prod_topology {X Y : Top} :
(X ⨯ Y).topological_space = topological_space.induced ⇑category_theory.limits.prod.fst X.topological_space ⊓ topological_space.induced ⇑category_theory.limits.prod.snd Y.topological_space
source
theorem Top.range_prod_map {W X Y Z : Top} (f : W ⟶ Y) (g : X ⟶ Z) :
set.range ⇑(category_theory.limits.prod.map f g) = ⇑category_theory.limits.prod.fst ⁻¹' set.range ⇑f ∩ ⇑category_theory.limits.prod.snd ⁻¹' set.range ⇑g
source
theorem Top.inducing_prod_map {W X Y Z : Top} {f : W ⟶ X} {g : Y ⟶ Z} (hf : inducing ⇑f) (hg : inducing ⇑g) :
inducing ⇑(category_theory.limits.prod.map f g)
source
theorem Top.embedding_prod_map {W X Y Z : Top} {f : W ⟶ X} {g : Y ⟶ Z} (hf : embedding ⇑f) (hg : embedding ⇑g) :
embedding ⇑(category_theory.limits.prod.map f g)
source
@[protected]
def Top.binary_cofan (X Y : Top) :
category_theory.limits.binary_cofan X Y

The binary coproduct cofan in Top.

Equations
source
def Top.binary_cofan_is_colimit (X Y : Top) :
category_theory.limits.is_colimit (X.binary_cofan Y)

The constructed binary coproduct cofan in Top is the coproduct.

Equations
source
theorem Top.binary_cofan_is_colimit_iff {X Y : Top} (c : category_theory.limits.binary_cofan X Y) :
nonempty (category_theory.limits.is_colimit c) ↔ open_embedding ⇑(c.inl) ∧ open_embedding ⇑(c.inr) ∧ is_compl (set.range ⇑(c.inl)) (set.range ⇑(c.inr))