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.

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.

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.

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.

@[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).π = CategoryTheory.NatTrans.mk fun j => Option.rec (CategoryTheory.CategoryStruct.comp (CompHaus.pullback.fst f g) f) (fun val => CategoryTheory.Limits.WalkingPair.rec (CompHaus.pullback.fst f g) (CompHaus.pullback.snd f g) val) j

@[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.

@[simp]

theorem CompHaus.pullback.isLimit_lift {X : CompHaus} {Y : CompHaus} {B : CompHaus} (f : X ⟶ B) (g : Y ⟶ B) (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.IsLimit.lift (CompHaus.pullback.isLimit f g) s = CompHaus.pullback.lift f g (CategoryTheory.Limits.PullbackCone.fst s) (CategoryTheory.Limits.PullbackCone.snd s) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.fst s) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.snd s) g)

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.

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.

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.

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

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

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

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

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

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

def CompHaus.finiteCoproduct.desc {α : Type} [Fintype α] (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.

@[simp]

theorem CompHaus.finiteCoproduct.ι_desc_assoc {α : Type} [Fintype α] (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} [Fintype α] (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} [Fintype α] (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

@[simp]

theorem CompHaus.finiteCoproduct.cocone_ι {α : Type} [Fintype α] (X : α → CompHaus) : (CompHaus.finiteCoproduct.cocone X).ι = CategoryTheory.Discrete.natTrans fun x => match x with | { as := a } => CompHaus.finiteCoproduct.ι X a

@[simp]

theorem CompHaus.finiteCoproduct.cocone_pt {α : Type} [Fintype α] (X : α → CompHaus) : (CompHaus.finiteCoproduct.cocone X).pt = CompHaus.finiteCoproduct X

def CompHaus.finiteCoproduct.cocone {α : Type} [Fintype α] (X : α → CompHaus) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor X)

The coproduct cocone associated to the explicit finite coproduct.

@[simp]

theorem CompHaus.finiteCoproduct.isColimit_desc {α : Type} [Fintype α] (X : α → CompHaus) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor X)) : CategoryTheory.Limits.IsColimit.desc (CompHaus.finiteCoproduct.isColimit X) s = CompHaus.finiteCoproduct.desc (fun a => X a) fun a => s.ι.app { as := a }

def CompHaus.finiteCoproduct.isColimit {α : Type} [Fintype α] (X : α → CompHaus) : CategoryTheory.Limits.IsColimit (CompHaus.finiteCoproduct.cocone X)

The explicit finite coproduct cocone is a colimit cocone.

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

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

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

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

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

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

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

theorem CompHaus.finiteCoproduct.ι_desc_apply {α : Type} [Fintype α] (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