Explicit limits and colimits

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

Main definitions

• HasExplicitFiniteCoproducts: A typeclass describing the property that forming all finite disjoint unions is stable under the property P.

  • Given this property, we deduce that CompHausLike P has finite coproducts and the inclusion functors to other CompHausLike P' and to TopCat preserve them.

• HasExplicitPullbacks: A typeclass describing the property that forming all "explicit pullbacks" is stable under the property P. Here, explicit pullbacks are defined as a subset of the product.

  • Given this property, we deduce that CompHausLike P has pullbacks and the inclusion functors to other CompHausLike P' and to TopCat preserve them.
  • We also define a variant HasExplicitPullbacksOfInclusions which is says that explicit pullbacks along inclusion maps into finite disjoint unions exist. Stonean has this property but not the stronger one.

Main results

• Given [HasExplicitPullbacksOfInclusions P] (which is implied by [HasExplicitPullbacks P]), we provide an instance FinitaryExtensive (CompHausLike P).

@[reducible, inline]

abbrev CompHausLike.HasExplicitFiniteCoproduct {P : TopCat → Prop} {α : Type w} (X : α → CompHausLike P) : Prop

A typeclass describing the property that forming the disjoint union is stable under the property P.

def CompHausLike.finiteCoproduct {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] : CompHausLike P

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

def CompHausLike.finiteCoproduct.ι {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] (a : α) : X a ⟶ finiteCoproduct X

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

def CompHausLike.finiteCoproduct.desc {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) : 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 CompHausLike.finiteCoproduct.ι_desc {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] {B : CompHausLike P} (e : (a : α) → X a ⟶ B) (a : α) : CategoryTheory.CategoryStruct.comp (ι X a) (desc X e) = e a

@[simp]

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

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

@[reducible, inline]

abbrev CompHausLike.finiteCoproduct.cofan {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.Cofan X

The coproduct cocone associated to the explicit finite coproduct.

def CompHausLike.finiteCoproduct.isColimit {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.IsColimit (cofan X)

The explicit finite coproduct cocone is a colimit cocone.

theorem CompHausLike.finiteCoproduct.ι_injective {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] (a : α) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (ι X a))

theorem CompHausLike.finiteCoproduct.ι_jointly_surjective {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] (R : ↑(finiteCoproduct X).toTop) : ∃ (a : α) (r : ↑(X a).toTop), R = (CategoryTheory.ConcreteCategory.hom (ι X a)) r

theorem CompHausLike.finiteCoproduct.ι_desc_apply {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] {B : CompHausLike P} {π : (a : α) → X a ⟶ B} (a : α) (x : (fun (X : CompHausLike P) => ↑X.toTop) (X a)) : (CategoryTheory.ConcreteCategory.hom (desc X π)) ((CategoryTheory.ConcreteCategory.hom (ι X a)) x) = (CategoryTheory.ConcreteCategory.hom (π a)) x

instance CompHausLike.instHasCoproduct {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.HasCoproduct X

class CompHausLike.HasExplicitFiniteCoproducts (P : TopCat → Prop) : Prop

A typeclass describing the property that forming all finite disjoint unions is stable under the property P.

• hasProp {α : Type w} [Finite α] (X : α → CompHausLike P) : HasExplicitFiniteCoproduct X

instance CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] (α : Type w) [Finite α] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) (CompHausLike P)

instance CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] : CategoryTheory.Limits.HasFiniteCoproducts (CompHausLike P)

theorem CompHausLike.finiteCoproduct.isOpenEmbedding_ι {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] (a : α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (ι X a))

The inclusion maps into the explicit finite coproduct are open embeddings.

theorem CompHausLike.Sigma.isOpenEmbedding_ι {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [HasExplicitFiniteCoproduct X] (a : α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι X a))

The inclusion maps into the abstract finite coproduct are open embeddings.

instance CompHausLike.instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts (P : TopCat → Prop) [HasExplicitFiniteCoproducts P] : CategoryTheory.Limits.PreservesFiniteCoproducts (compHausLikeToTop P)

The functor to TopCat preserves finite coproducts if they exist.

instance CompHausLike.instPreservesFiniteCoproductsToCompHausLike {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : CategoryTheory.Limits.PreservesFiniteCoproducts (toCompHausLike h)

The functor to another CompHausLike preserves finite coproducts if they exist.

@[reducible, inline]

abbrev CompHausLike.HasExplicitPullback {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) : Prop

A typeclass describing the property that an explicit pullback is stable under the property P.

def CompHausLike.pullback {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CompHausLike P

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 CompHausLike.pullback.fst {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : pullback f g ⟶ X

The projection from the pullback to the first component.

def CompHausLike.pullback.snd {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : pullback f g ⟶ Y

The projection from the pullback to the second component.

theorem CompHausLike.pullback.condition {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CategoryTheory.CategoryStruct.comp (fst f g) f = CategoryTheory.CategoryStruct.comp (snd f g) g

theorem CompHausLike.pullback.condition_assoc {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (fst f g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (snd f g) (CategoryTheory.CategoryStruct.comp g h)

def CompHausLike.pullback.lift {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : Z ⟶ 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 CompHausLike.pullback.lift_fst {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (lift f g a b w) (fst f g) = a

@[simp]

theorem CompHausLike.pullback.lift_fst_assoc {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z✝ : CompHausLike P} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift f g a b w) (CategoryTheory.CategoryStruct.comp (fst f g) h) = CategoryTheory.CategoryStruct.comp a h

@[simp]

theorem CompHausLike.pullback.lift_snd {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) : CategoryTheory.CategoryStruct.comp (lift f g a b w) (snd f g) = b

@[simp]

theorem CompHausLike.pullback.lift_snd_assoc {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y) (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z✝ : CompHausLike P} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift f g a b w) (CategoryTheory.CategoryStruct.comp (snd f g) h) = CategoryTheory.CategoryStruct.comp b h

theorem CompHausLike.pullback.hom_ext {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {Z : CompHausLike P} (a b : Z ⟶ pullback f g) (hfst : CategoryTheory.CategoryStruct.comp a (fst f g) = CategoryTheory.CategoryStruct.comp b (fst f g)) (hsnd : CategoryTheory.CategoryStruct.comp a (snd f g) = CategoryTheory.CategoryStruct.comp b (snd f g)) : a = b

def CompHausLike.pullback.cone {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CategoryTheory.Limits.PullbackCone f g

The pullback cone whose cone point is the explicit pullback.

@[simp]

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

@[simp]

theorem CompHausLike.pullback.cone_pt {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : (cone f g).pt = pullback f g

def CompHausLike.pullback.isLimit {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CategoryTheory.Limits.IsLimit (cone f g)

The explicit pullback cone is a limit cone.

@[simp]

theorem CompHausLike.pullback.isLimit_lift {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] (s : CategoryTheory.Limits.PullbackCone f g) : (isLimit f g).lift s = lift f g s.fst s.snd ⋯

instance CompHausLike.instHasLimitWalkingCospanCospan {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)

noncomputable instance CompHausLike.instCreatesLimitTopCatWalkingCospanCospanCompHausLikeToTop {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) (compHausLikeToTop P)

The functor to TopCat creates pullbacks if they exist.

instance CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (compHausLikeToTop P)

The functor to TopCat preserves pullbacks.

instance CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [HasExplicitPullback f g] {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (toCompHausLike h)

The functor to another CompHausLike preserves pullbacks.

class CompHausLike.HasExplicitPullbacks (P : TopCat → Prop) : Prop

A typeclass describing the property that forming all explicit pullbacks is stable under the property P.

• hasProp {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) : HasExplicitPullback f g

instance CompHausLike.instHasPullbacksOfHasExplicitPullbacks {P : TopCat → Prop} [HasExplicitPullbacks P] : CategoryTheory.Limits.HasPullbacks (CompHausLike P)

class CompHausLike.HasExplicitPullbacksOfInclusions (P : TopCat → Prop) [HasExplicitFiniteCoproducts P] : Prop

A typeclass describing the property that explicit pullbacks along inclusion maps into disjoint unions is stable under the property P.

• hasProp {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y) : HasExplicitPullback CategoryTheory.Limits.coprod.inl f

instance CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks {P : TopCat → Prop} [HasExplicitPullbacks P] [HasExplicitFiniteCoproducts P] : HasExplicitPullbacksOfInclusions P

instance CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] [HasExplicitPullbacksOfInclusions P] : CategoryTheory.HasPullbacksOfInclusions (CompHausLike P)

theorem CompHausLike.hasPullbacksOfInclusions {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] (hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → HasExplicitPullback f g) : HasExplicitPullbacksOfInclusions P

instance CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] [HasExplicitPullbacksOfInclusions P] : CategoryTheory.PreservesPullbacksOfInclusions (compHausLikeToTop P)

The functor to TopCat preserves pullbacks of inclusions if they exist.

instance CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] [HasExplicitPullbacksOfInclusions P] : CategoryTheory.FinitaryExtensive (CompHausLike P)

theorem CompHausLike.finitaryExtensive {P : TopCat → Prop} [HasExplicitFiniteCoproducts P] (hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) → HasExplicitPullback f g) : CategoryTheory.FinitaryExtensive (CompHausLike P)

def CompHausLike.isTerminalPUnit {P : TopCat → Prop} [HasProp P PUnit.{u + 1}] : CategoryTheory.Limits.IsTerminal (of P PUnit.{u + 1})

A one-element space is terminal in CompHaus