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.

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 {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

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

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.isOpenEmbedding_ι {P : TopCat → Prop} {α : Type w} [Finite α] (X : α → CompHausLike P) [CompHausLike.HasExplicitFiniteCoproduct X] (a : α) : IsOpenEmbedding ⇑(CompHausLike.finiteCoproduct.ι X a)

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

@[deprecated CompHausLike.finiteCoproduct.isOpenEmbedding_ι]

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

Alias of CompHausLike.finiteCoproduct.isOpenEmbedding_ι.

---

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

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

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

@[deprecated CompHausLike.Sigma.isOpenEmbedding_ι]

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

Alias of CompHausLike.Sigma.isOpenEmbedding_ι.

---

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 {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

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)

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 {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_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_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

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

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

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.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 := ⋯ }

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

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 ⋯) ⋯ ⋯ ⋯

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

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} : ∀ {inst : CompHausLike.HasExplicitFiniteCoproducts P} [self : CompHausLike.HasExplicitPullbacksOfInclusions P] {X Y 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), IsOpenEmbedding ⇑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), IsOpenEmbedding ⇑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.30 + 1} )