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.

@[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 ι) :

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') :
@[simp]
theorem Top.pi_iso_pi_inv_π {ι : Type v} (α : ι Top) (i : ι) :
@[simp]
theorem Top.pi_iso_pi_inv_π_apply {ι : Type v} (α : ι Top) (i : ι) (x : Π (i : ι), (α i)) :
@[simp]
theorem Top.pi_iso_pi_hom_apply {ι : Type v} (α : ι Top) (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.

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

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

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]
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_assoc {ι : Type v} (α : ι Top) (i : ι) {X' : Top} (f' : Top.of (Σ (i : ι), (α i)) X') :
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_apply {ι : Type v} (α : ι Top) (i : ι) (x : (α i)) :
@[simp]
theorem Top.sigma_iso_sigma_inv_apply {ι : Type v} (α : ι Top) (i : ι) (x : (α i)) :
@[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.

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
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) :