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.

Equations
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.

Equations
• = { toFun := fun (x : ().toTop) => match x with | (x, snd), property => x, continuous_toFun := }
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.

Equations
• = { toFun := fun (x : ().toTop) => match x with | (fst, y), property => y, continuous_toFun := }
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.

Equations
• = { toFun := fun (z : Z.toTop) => (a z, b z), , continuous_toFun := }
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) :
() = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (fun (val : CategoryTheory.Limits.WalkingPair) => ) j, naturality := }
@[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.

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

The explicit pullback cone is a limit cone.

Equations
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.

Equations
• = .conePointUniqueUpToIso
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.

Equations
Instances For
theorem CompHaus.pullback_fst_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
theorem CompHaus.pullback_snd_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X B) (g : Y B) :
def CompHaus.finiteCoproduct {α : Type w} [] (X : αCompHaus) :

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

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

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

Equations
• = { toFun := fun (x : (X a).toTop) => a, x, continuous_toFun := }
Instances For
def CompHaus.finiteCoproduct.desc {α : Type w} [] (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.

Equations
• = { toFun := fun (x : .toTop) => match x with | a, x => (e a) x, continuous_toFun := }
Instances For
@[simp]
theorem CompHaus.finiteCoproduct.ι_desc_assoc {α : Type w} [] (X : αCompHaus) {B : CompHaus} (e : (a : α) → X a B) (a : α) {Z : CompHaus} (h : B Z) :
@[simp]
theorem CompHaus.finiteCoproduct.ι_desc {α : Type w} [] (X : αCompHaus) {B : CompHaus} (e : (a : α) → X a B) (a : α) :
theorem CompHaus.finiteCoproduct.hom_ext {α : Type w} [] (X : αCompHaus) {B : CompHaus} (f : ) (g : ) (h : ∀ (a : α), ) :
f = g
@[reducible, inline]
abbrev CompHaus.finiteCoproduct.cofan {α : Type w} [] (X : αCompHaus) :

The coproduct cocone associated to the explicit finite coproduct.

Equations
Instances For
def CompHaus.finiteCoproduct.isColimit {α : Type w} [] (X : αCompHaus) :

The explicit finite coproduct cocone is a colimit cocone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CompHaus.coproductIsoCoproduct {α : Type w} [] (X : αCompHaus) :

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

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

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

Equations
Instances For
theorem CompHaus.finiteCoproduct.ι_injective {α : Type w} [] (X : αCompHaus) (a : α) :
theorem CompHaus.finiteCoproduct.ι_jointly_surjective {α : Type w} [] (X : αCompHaus) (R : .toTop) :
∃ (a : α) (r : (X a).toTop), R = r
theorem CompHaus.finiteCoproduct.ι_desc_apply {α : Type w} [] (X : αCompHaus) {B : CompHaus} {π : (a : α) → X a B} (a : α) (x : (X a)) :
( x) = (π a) x
Equations
• One or more equations did not get rendered due to their size.

A one-element space is terminal in CompHaus

Equations
Instances For
noncomputable def CompHaus.terminalIsoPUnit :

The isomorphism from an arbitrary terminal object of CompHaus to a one-element space.

Equations
Instances For