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

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

• CompHaus.pullback f g = CompHaus.of ↑{xy : ↑X.toTop × ↑Y.toTop | f xy.1 = g xy.2}

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

The projection from the pullback to the first component.

Equations

• CompHaus.pullback.fst f g = { toFun := fun (x : ↑(CompHaus.pullback f g).toTop) => match x with | ⟨(x, snd), property⟩ => x, continuous_toFun := ⋯ }

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

The projection from the pullback to the second component.

Equations

• CompHaus.pullback.snd f g = { toFun := fun (x : ↑(CompHaus.pullback f g).toTop) => match x with | ⟨(fst, y), property⟩ => y, continuous_toFun := ⋯ }

theorem CompHaus.pullback.condition_assoc {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) {Z : CompHaus} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CompHaus.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g h)

theorem CompHaus.pullback.condition {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (CompHaus.pullback.snd f g) g

def CompHaus.pullback.lift {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) {Z : CompHaus} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : Z ⟶ CompHaus.pullback f g

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

• CompHaus.pullback.lift f g a b w = { toFun := fun (z : ↑Z.toTop) => ⟨(a z, b z), ⋯⟩, continuous_toFun := ⋯ }

@[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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z : CompHaus} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHaus.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp a h

@[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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (CompHaus.pullback.lift f g a b w) (CompHaus.pullback.fst f g) = 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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z : CompHaus} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHaus.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (CompHaus.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp b h

@[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) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (CompHaus.pullback.lift f g a b w) (CompHaus.pullback.snd f g) = b

theorem CompHaus.pullback.hom_ext {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) {Z : CompHaus} (a : Z ⟶ CompHaus.pullback f g) (b : Z ⟶ CompHaus.pullback f g) (hfst : CategoryTheory.CategoryStruct.comp a (CompHaus.pullback.fst f g) = CategoryTheory.CategoryStruct.comp b (CompHaus.pullback.fst f g)) (hsnd : CategoryTheory.CategoryStruct.comp a (CompHaus.pullback.snd f g) = CategoryTheory.CategoryStruct.comp b (CompHaus.pullback.snd f g)) : a = b

@[simp]

theorem CompHaus.pullback.cone_π {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : (CompHaus.pullback.cone f g).π = { app := fun (j : CategoryTheory.Limits.WalkingCospan) => Option.rec (CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) f) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CompHaus.pullback.fst f g) (CompHaus.pullback.snd f g) val) j, naturality := ⋯ }

@[simp]

theorem CompHaus.pullback.cone_pt {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : (CompHaus.pullback.cone f g).pt = CompHaus.pullback f g

def CompHaus.pullback.cone {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : CategoryTheory.Limits.PullbackCone f g

The pullback cone whose cone point is the explicit pullback.

Equations

• CompHaus.pullback.cone f g = CategoryTheory.Limits.PullbackCone.mk (CompHaus.pullback.fst f g) (CompHaus.pullback.snd f g) ⋯

@[simp]

theorem CompHaus.pullback.isLimit_lift {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) (s : CategoryTheory.Limits.PullbackCone f g) : (CompHaus.pullback.isLimit f g).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) : CategoryTheory.Limits.IsLimit (CompHaus.pullback.cone f g)

The explicit pullback cone is a limit cone.

Equations

• CompHaus.pullback.isLimit f g = (CompHaus.pullback.cone f g).isLimitAux (fun (s : CategoryTheory.Limits.PullbackCone f g) => CompHaus.pullback.lift f g s.fst s.snd ⋯) ⋯ ⋯ ⋯

noncomputable def CompHaus.pullbackIsoPullback {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : CompHaus.pullback f g ≅ CategoryTheory.Limits.pullback f g

The isomorphism from the explicit pullback to the abstract pullback.

Equations

• CompHaus.pullbackIsoPullback f g = (CompHaus.pullback.isLimit f g).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan f g))

noncomputable def CompHaus.pullbackHomeoPullback {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : ↑(CompHaus.pullback f g).toTop ≃ₜ ↑(CategoryTheory.Limits.pullback f g).toTop

The homeomorphism from the explicit pullback to the abstract pullback.

Equations

• CompHaus.pullbackHomeoPullback f g = CompHausLike.homeoOfIso (CompHaus.pullbackIsoPullback f g)

theorem CompHaus.pullback_fst_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : CompHaus.pullback.fst f g = CategoryTheory.CategoryStruct.comp (CompHaus.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.fst f g)

theorem CompHaus.pullback_snd_eq {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) : CompHaus.pullback.snd f g = CategoryTheory.CategoryStruct.comp (CompHaus.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.snd f g)

def CompHaus.finiteCoproduct {α : Type w} [Finite α] (X : α → CompHaus) : CompHaus

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

Equations

• CompHaus.finiteCoproduct X = CompHaus.of ((a : α) × ↑(X a).toTop)

def CompHaus.finiteCoproduct.ι {α : Type w} [Finite α] (X : α → CompHaus) (a : α) : X a ⟶ CompHaus.finiteCoproduct X

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

Equations

• CompHaus.finiteCoproduct.ι X a = { toFun := fun (x : ↑(X a).toTop) => ⟨a, x⟩, continuous_toFun := ⋯ }

def CompHaus.finiteCoproduct.desc {α : Type w} [Finite α] (X : α → CompHaus) {B : CompHaus} (e : (a : α) → X a ⟶ B) : CompHaus.finiteCoproduct X ⟶ 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

• CompHaus.finiteCoproduct.desc X e = { toFun := fun (x : ↑(CompHaus.finiteCoproduct X).toTop) => match x with | ⟨a, x⟩ => (e a) x, continuous_toFun := ⋯ }

@[simp]

theorem CompHaus.finiteCoproduct.ι_desc_assoc {α : Type w} [Finite α] (X : α → CompHaus) {B : CompHaus} (e : (a : α) → X a ⟶ B) (a : α) {Z : CompHaus} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) (CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.desc X e) h) = CategoryTheory.CategoryStruct.comp (e a) h

@[simp]

theorem CompHaus.finiteCoproduct.ι_desc {α : Type w} [Finite α] (X : α → CompHaus) {B : CompHaus} (e : (a : α) → X a ⟶ B) (a : α) : CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) (CompHaus.finiteCoproduct.desc X e) = e a

theorem CompHaus.finiteCoproduct.hom_ext {α : Type w} [Finite α] (X : α → CompHaus) {B : CompHaus} (f : CompHaus.finiteCoproduct X ⟶ B) (g : CompHaus.finiteCoproduct X ⟶ B) (h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (CompHaus.finiteCoproduct.ι X a) g) : f = g

@[reducible, inline]

abbrev CompHaus.finiteCoproduct.cofan {α : Type w} [Finite α] (X : α → CompHaus) : CategoryTheory.Limits.Cofan X

The coproduct cocone associated to the explicit finite coproduct.

Equations

• CompHaus.finiteCoproduct.cofan X = CategoryTheory.Limits.Cofan.mk (CompHaus.finiteCoproduct X) (CompHaus.finiteCoproduct.ι X)

def CompHaus.finiteCoproduct.isColimit {α : Type w} [Finite α] (X : α → CompHaus) : CategoryTheory.Limits.IsColimit (CompHaus.finiteCoproduct.cofan X)

The explicit finite coproduct cocone is a colimit cocone.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CompHaus.coproductIsoCoproduct {α : Type w} [Finite α] (X : α → CompHaus) : CompHaus.finiteCoproduct X ≅ ∐ X

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

Equations

• CompHaus.coproductIsoCoproduct X = (CompHaus.finiteCoproduct.isColimit X).coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor X))

theorem CompHaus.Sigma.ι_comp_toFiniteCoproduct {α : Type w} [Finite α] (X : α → CompHaus) (a : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X a) (CompHaus.coproductIsoCoproduct X).inv = CompHaus.finiteCoproduct.ι X a

noncomputable def CompHaus.coproductHomeoCoproduct {α : Type w} [Finite α] (X : α → CompHaus) : ↑(CompHaus.finiteCoproduct X).toTop ≃ₜ ↑(∐ X).toTop

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

Equations

• CompHaus.coproductHomeoCoproduct X = CompHausLike.homeoOfIso (CompHaus.coproductIsoCoproduct X)

theorem CompHaus.finiteCoproduct.ι_injective {α : Type w} [Finite α] (X : α → CompHaus) (a : α) : Function.Injective ⇑(CompHaus.finiteCoproduct.ι X a)

theorem CompHaus.finiteCoproduct.ι_jointly_surjective {α : Type w} [Finite α] (X : α → CompHaus) (R : ↑(CompHaus.finiteCoproduct X).toTop) : ∃ (a : α) (r : ↑(X a).toTop), R = (CompHaus.finiteCoproduct.ι X a) r

theorem CompHaus.finiteCoproduct.ι_desc_apply {α : Type w} [Finite α] (X : α → CompHaus) {B : CompHaus} {π : (a : α) → X a ⟶ B} (a : α) (x : (CategoryTheory.forget CompHaus).obj (X a)) : (CompHaus.finiteCoproduct.desc X π) ((CompHaus.finiteCoproduct.ι X a) x) = (π a) x

instance CompHaus.instPreservesFiniteCoproductsTopCatCompHausToTop : CategoryTheory.Limits.PreservesFiniteCoproducts compHausToTop

Equations

• One or more equations did not get rendered due to their size.

instance CompHaus.instFinitaryExtensive : CategoryTheory.FinitaryExtensive CompHaus

Equations

• CompHaus.instFinitaryExtensive = ⋯

def CompHaus.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (CompHaus.of PUnit.{u + 1} )

A one-element space is terminal in CompHaus

Equations

• CompHaus.isTerminalPUnit = CategoryTheory.Limits.IsTerminal.ofUnique (CompHaus.of PUnit.{u + 1} )

noncomputable def CompHaus.terminalIsoPUnit : ⊤_ CompHaus ≅ CompHaus.of PUnit.{u + 1}

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

Equations

• CompHaus.terminalIsoPUnit = CategoryTheory.Limits.terminalIsTerminal.uniqueUpToIso CompHaus.isTerminalPUnit