# Documentation

Mathlib.Topology.Category.CompHaus.Limits

# Explicit limits and colimits #

This file collects some constructions of explicit limits and colimits in CompHaus, which may be useful due to their definitional properties.

So far, we have the following:

• Explicit pullbacks, defined in the "usual" way as a subset of the product.
• Explicit finite coproducts, defined as a disjoint union.
def CompHaus.pullback {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :

The pullback of two morphisms f,g in CompHaus, constructed explicitly as the set of pairs (x,y) such that f x = g y, with the topology induced by the product.

Instances For
def CompHaus.pullback.fst {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
X

The projection from the pullback to the first component.

Instances For
def CompHaus.pullback.snd {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
Y

The projection from the pullback to the second component.

Instances For
theorem CompHaus.pullback.condition_assoc {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (h : B Z) :
theorem CompHaus.pullback.condition {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
def CompHaus.pullback.lift {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (a : Z X) (b : Z Y) :
Z

Construct a morphism to the explicit pullback given morphisms to the factors which are compatible with the maps to the base. This is essentially the universal property of the pullback.

Instances For
@[simp]
theorem CompHaus.pullback.lift_fst_assoc {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (a : Z X) (b : Z Y) {Z : CompHaus} (h : X Z) :
@[simp]
theorem CompHaus.pullback.lift_fst {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (a : Z X) (b : Z Y) :
= a
@[simp]
theorem CompHaus.pullback.lift_snd_assoc {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (a : Z X) (b : Z Y) {Z : CompHaus} (h : Y Z) :
@[simp]
theorem CompHaus.pullback.lift_snd {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (a : Z X) (b : Z Y) :
= b
theorem CompHaus.pullback.hom_ext {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) {Z : CompHaus} (a : Z ) (b : Z ) (hfst : ) (hsnd : ) :
a = b
@[simp]
theorem CompHaus.pullback.cone_π {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
().π = CategoryTheory.NatTrans.mk fun j => Option.rec () (fun val => ) j
@[simp]
theorem CompHaus.pullback.cone_pt {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
().pt =
def CompHaus.pullback.cone {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :

The pullback cone whose cone point is the explicit pullback.

Instances For
@[simp]
theorem CompHaus.pullback.isLimit_lift {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) (s : ) :
def CompHaus.pullback.isLimit {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :

The explicit pullback cone is a limit cone.

Instances For
noncomputable def CompHaus.pullbackIsoPullback {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :

The isomorphism from the explicit pullback to the abstract pullback.

Instances For
noncomputable def CompHaus.pullbackHomeoPullback {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
().toTop ≃ₜ ().toTop

The homeomorphism from the explicit pullback to the abstract pullback.

Instances For
theorem CompHaus.pullback_fst_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
= CategoryTheory.CategoryStruct.comp ().hom CategoryTheory.Limits.pullback.fst
theorem CompHaus.pullback_snd_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
= CategoryTheory.CategoryStruct.comp ().hom CategoryTheory.Limits.pullback.snd
def CompHaus.finiteCoproduct {α : Type} [] (X : αCompHaus) :

The coproduct of a finite family of objects in CompHaus, constructed as the disjoint union with its usual topology.

Instances For
def CompHaus.finiteCoproduct.ι {α : Type} [] (X : αCompHaus) (a : α) :

The inclusion of one of the factors into the explicit finite coproduct.

Instances For
def CompHaus.finiteCoproduct.desc {α : Type} [] (X : αCompHaus) {B : CompHaus} (e : (a : α) → X a B) :

To construct a morphism from the explicit finite coproduct, it suffices to specify a morphism from each of its factors. This is essentially the universal property of the coproduct.

Instances For
@[simp]
theorem CompHaus.finiteCoproduct.ι_desc_assoc {α : Type} [] (X : αCompHaus) {B : CompHaus} (e : (a : α) → X a B) (a : α) {Z : CompHaus} (h : B Z) :
@[simp]
theorem CompHaus.finiteCoproduct.ι_desc {α : Type} [] (X : αCompHaus) {B : CompHaus} (e : (a : α) → X a B) (a : α) :
theorem CompHaus.finiteCoproduct.hom_ext {α : Type} [] (X : αCompHaus) {B : CompHaus} (f : ) (g : ) (h : ∀ (a : α), ) :
f = g
@[simp]
theorem CompHaus.finiteCoproduct.cocone_ι {α : Type} [] (X : αCompHaus) :
= CategoryTheory.Discrete.natTrans fun x => match x with | { as := a } =>
@[simp]
theorem CompHaus.finiteCoproduct.cocone_pt {α : Type} [] (X : αCompHaus) :
def CompHaus.finiteCoproduct.cocone {α : Type} [] (X : αCompHaus) :

The coproduct cocone associated to the explicit finite coproduct.

Instances For
@[simp]
theorem CompHaus.finiteCoproduct.isColimit_desc {α : Type} [] (X : αCompHaus) :
= CompHaus.finiteCoproduct.desc (fun a => X a) fun a => s.app { as := a }
def CompHaus.finiteCoproduct.isColimit {α : Type} [] (X : αCompHaus) :

The explicit finite coproduct cocone is a colimit cocone.

Instances For
noncomputable def CompHaus.coproductIsoCoproduct {α : Type} [] (X : αCompHaus) :

The isomorphism from the explicit finite coproducts to the abstract coproduct.

Instances For
theorem CompHaus.Sigma.ι_comp_toFiniteCoproduct {α : Type} [] (X : αCompHaus) (a : α) :
noncomputable def CompHaus.coproductHomeoCoproduct {α : Type} [] (X : αCompHaus) :
().toTop ≃ₜ ( X).toTop

The homeomorphism from the explicit finite coproducts to the abstract coproduct.

Instances For
theorem CompHaus.finiteCoproduct.ι_injective {α : Type} [] (X : αCompHaus) (a : α) :
theorem CompHaus.finiteCoproduct.ι_jointly_surjective {α : Type} [] (X : αCompHaus) (R : ().toTop) :
a r, R = ↑() r
theorem CompHaus.finiteCoproduct.ι_desc_apply {α : Type} [] (X : αCompHaus) {B : CompHaus} {π : (a : α) → X a B} (a : α) (x : ().obj (X a)) :
↑() (↑() x) = ↑(π a) x