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.

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.

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

Equations

• CompHausLike.HasExplicitFiniteCoproduct X = CompHausLike.HasProp P ((a : α) × ↑(X a).toTop)

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

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

Equations

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

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

@[reducible, inline]

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

The coproduct cocone associated to the explicit finite coproduct.

Equations

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

def CompHausLike.finiteCoproduct.isColimit {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] : CategoryTheory.Limits.IsColimit (CompHausLike.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.

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

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

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

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

Equations

• ⋯ = ⋯

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} [inst : Finite α] (X : α → CompHausLike P), CompHausLike.HasExplicitFiniteCoproduct X

theorem CompHausLike.HasExplicitFiniteCoproducts.hasProp {P : TopCat → Prop} [self : CompHausLike.HasExplicitFiniteCoproducts P] {α : Type w} [Finite α] (X : α → CompHausLike P) : CompHausLike.HasExplicitFiniteCoproduct X

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CompHausLike.finiteCoproduct.openEmbedding_ι {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : OpenEmbedding ⇑(CompHausLike.finiteCoproduct.ι X a)

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

theorem CompHausLike.Sigma.openEmbedding_ι {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : OpenEmbedding ⇑(CategoryTheory.Limits.Sigma.ι X a)

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

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

The functor to TopCat preserves finite coproducts if they exist.

Equations

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

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

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

Equations

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

@[reducible, inline]

abbrev CompHausLike.HasExplicitPullback {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} {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.

Equations

• CompHausLike.HasExplicitPullback f g = CompHausLike.HasProp P ↑{xy : ↑X.toTop × ↑Y.toTop | f xy.1 = g xy.2}

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

Equations

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

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

The projection from the pullback to the first component.

Equations

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

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

The projection from the pullback to the second component.

Equations

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CompHausLike.pullback.lift_snd_assoc {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} {B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.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 (CompHausLike.pullback.lift f g a b w) (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp b h

@[simp]

theorem CompHausLike.pullback.lift_snd {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} {B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.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 (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.snd f g) = b

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

@[simp]

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

@[simp]

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

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

The pullback cone whose cone point is the explicit pullback.

Equations

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

@[simp]

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

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

The explicit pullback cone is a limit cone.

Equations

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

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

Equations

• ⋯ = ⋯

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

The functor to TopCat creates pullbacks if they exist.

Equations

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

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

The functor to TopCat preserves pullbacks.

Equations

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

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

The functor to another CompHausLike preserves pullbacks.

Equations

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

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), CompHausLike.HasExplicitPullback f g

theorem CompHausLike.HasExplicitPullbacks.hasProp {P : TopCat → Prop} [self : CompHausLike.HasExplicitPullbacks P] {X : CompHausLike P} {Y : CompHausLike P} {B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) : CompHausLike.HasExplicitPullback f g

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

Equations

• ⋯ = ⋯

class CompHausLike.HasExplicitPullbacksOfInclusions (P : TopCat → Prop) [CompHausLike.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), CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f

theorem CompHausLike.HasExplicitPullbacksOfInclusions.hasProp {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] [self : CompHausLike.HasExplicitPullbacksOfInclusions P] {X : CompHausLike P} {Y : CompHausLike P} {Z : CompHausLike P} (f : Z ⟶ X ⨿ Y) : CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions = CategoryTheory.PreservesPullbacksOfInclusions.mk

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

Equations

• ⋯ = ⋯

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

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

A one-element space is terminal in CompHaus

Equations

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