# mathlib3documentation

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.

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

The projection from the product as a bundled continous map.

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

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

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

The constructed fan is indeed a limit

Equations
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
@[simp]
theorem Top.pi_iso_pi_inv_π_assoc {ι : Type v} (α : ι Top) (i : ι) {X' : Top} (f' : α i X') :
.inv = i f'
@[simp]
theorem Top.pi_iso_pi_inv_π {ι : Type v} (α : ι Top) (i : ι) :
= i
@[simp]
theorem Top.pi_iso_pi_inv_π_apply {ι : Type v} (α : ι Top) (i : ι) (x : Π (i : ι), (α i)) :
(((Top.pi_iso_pi α).inv) x) = x i
@[simp]
theorem Top.pi_iso_pi_hom_apply {ι : Type v} (α : ι Top) (i : ι) (x : α) :
((Top.pi_iso_pi α).hom) x i = x
@[reducible]
def Top.sigma_ι {ι : Type v} (α : ι Top) (i : ι) :
α i Top.of (Σ (i : ι), (α i))

The inclusion to the coproduct as a bundled continous map.

def Top.sigma_cofan {ι : Type v} (α : ι Top) :

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

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

The constructed cofan is indeed a colimit

Equations
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
@[simp]
theorem Top.sigma_iso_sigma_hom_ι {ι : Type v} (α : ι Top) (i : ι) :
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_assoc {ι : Type v} (α : ι Top) (i : ι) {X' : Top} (f' : Top.of (Σ (i : ι), (α i)) X') :
= i f'
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_apply {ι : Type v} (α : ι Top) (i : ι) (x : (α i)) :
.hom) x) = i, x⟩
@[simp]
theorem Top.sigma_iso_sigma_inv_apply {ι : Type v} (α : ι Top) (i : ι) (x : (α i)) :
.inv) i, x⟩ =
theorem Top.induced_of_is_limit {J : Type v} {F : J Top}  :
theorem Top.limit_topology {J : Type v} (F : J Top) :
@[reducible]
def Top.prod_fst {X Y : Top} :

The first projection from the product.

@[reducible]
def Top.prod_snd {X Y : Top} :

The second projection from the product.

def Top.prod_binary_fan (X Y : Top) :

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

Equations

The constructed binary fan is indeed a limit

Equations
noncomputable def Top.prod_iso_prod (X Y : Top) :

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

Equations
@[simp]
theorem Top.prod_iso_prod_hom_fst (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_hom_fst_assoc (X Y : Top) {X' : Top} (f' : X X') :
@[simp]
theorem Top.prod_iso_prod_hom_snd (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_hom_snd_assoc (X Y : Top) {X' : Top} (f' : Y X') :
@[simp]
theorem Top.prod_iso_prod_hom_apply {X Y : Top} (x : (X Y)) :
@[simp]
theorem Top.prod_iso_prod_inv_fst_assoc (X Y : Top) {X' : Top} (f' : X X') :
=
@[simp]
theorem Top.prod_iso_prod_inv_fst (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_inv_snd (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_inv_snd_assoc (X Y : Top) {X' : Top} (f' : Y X') :
=
theorem Top.range_prod_map {W X Y Z : Top} (f : W Y) (g : X Z) :
theorem Top.inducing_prod_map {W X Y Z : Top} {f : W X} {g : Y Z} (hf : inducing f) (hg : inducing g) :
theorem Top.embedding_prod_map {W X Y Z : Top} {f : W X} {g : Y Z} (hf : embedding f) (hg : embedding g) :
@[protected]
def Top.binary_cofan (X Y : Top) :

The binary coproduct cofan in Top.

Equations

The constructed binary coproduct cofan in Top is the coproduct.

Equations