Categories of Compact Hausdorff Spaces

We construct the category of compact Hausdorff spaces satisfying an additional property P.

structure CompHausLike (P : TopCat → Prop) : Type (u + 1)

The type of Compact Hausdorff topological spaces satisfying an additional property P.

• toTop : TopCat

  The underlying topological space of an object of CompHausLike P.

• is_compact : CompactSpace ↑self.toTop

  The underlying topological space is compact.

• is_hausdorff : T2Space ↑self.toTop

  The underlying topological space is T2.

• prop : P self.toTop

  The underlying topological space satisfies P.

theorem CompHausLike.is_compact {P : TopCat → Prop} (self : CompHausLike P) : CompactSpace ↑self.toTop

The underlying topological space is compact.

theorem CompHausLike.is_hausdorff {P : TopCat → Prop} (self : CompHausLike P) : T2Space ↑self.toTop

The underlying topological space is T2.

theorem CompHausLike.prop {P : TopCat → Prop} (self : CompHausLike P) : P self.toTop

The underlying topological space satisfies P.

instance CompHausLike.instCoeSortType (P : TopCat → Prop) : CoeSort (CompHausLike P) (Type u)

Equations

• CompHausLike.instCoeSortType P = { coe := fun (X : CompHausLike P) => ↑X.toTop }

instance CompHausLike.category (P : TopCat → Prop) : CategoryTheory.Category.{u, u + 1} (CompHausLike P)

Equations

• CompHausLike.category P = CategoryTheory.InducedCategory.category CompHausLike.toTop

instance CompHausLike.concreteCategory (P : TopCat → Prop) : CategoryTheory.ConcreteCategory (CompHausLike P)

Equations

• CompHausLike.concreteCategory P = CategoryTheory.InducedCategory.concreteCategory CompHausLike.toTop

instance CompHausLike.hasForget₂ (P : TopCat → Prop) : CategoryTheory.HasForget₂ (CompHausLike P) TopCat

Equations

• CompHausLike.hasForget₂ P = CategoryTheory.InducedCategory.hasForget₂ CompHausLike.toTop

class CompHausLike.HasProp (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] : Prop

This wraps the predicate P : TopCat → Prop in a typeclass.

• hasProp : P (TopCat.of X)

theorem CompHausLike.HasProp.hasProp {P : TopCat → Prop} {X : Type u} [TopologicalSpace X] [self : CompHausLike.HasProp P X] : P (TopCat.of X)

def CompHausLike.of (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : CompHausLike P

A constructor for objects of the category CompHausLike P, taking a type, and bundling the compact Hausdorff topology found by typeclass inference.

Equations

• CompHausLike.of P X = CompHausLike.mk (TopCat.of X) ⋯

@[simp]

theorem CompHausLike.coe_of (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : ↑(CompHausLike.of P X).toTop = X

@[simp]

theorem CompHausLike.coe_id (P : TopCat → Prop) (X : CompHausLike P) : CategoryTheory.CategoryStruct.id ((CategoryTheory.forget (CompHausLike P)).obj X) = id

@[simp]

theorem CompHausLike.coe_comp (P : TopCat → Prop) {X : CompHausLike P} {Y : CompHausLike P} {Z : CompHausLike P} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget (CompHausLike P)).map f) ((CategoryTheory.forget (CompHausLike P)).map g) = ⇑g ∘ ⇑f

instance CompHausLike.instTopologicalSpaceObjForget (P : TopCat → Prop) (X : CompHausLike P) : TopologicalSpace ((CategoryTheory.forget (CompHausLike P)).obj X)

Equations

• CompHausLike.instTopologicalSpaceObjForget P X = inferInstanceAs (TopologicalSpace ↑X.toTop)

instance CompHausLike.instCompactSpaceObjForget (P : TopCat → Prop) (X : CompHausLike P) : CompactSpace ((CategoryTheory.forget (CompHausLike P)).obj X)

Equations

• ⋯ = ⋯

instance CompHausLike.instT2SpaceObjForget (P : TopCat → Prop) (X : CompHausLike P) : T2Space ((CategoryTheory.forget (CompHausLike P)).obj X)

Equations

• ⋯ = ⋯

@[simp]

theorem CompHausLike.toCompHausLike_map {P : TopCat → Prop} {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : ∀ {X Y : CompHausLike P} (f : X ⟶ Y), (CompHausLike.toCompHausLike h).map f = f

@[simp]

theorem CompHausLike.toCompHausLike_obj {P : TopCat → Prop} {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) (X : CompHausLike P) : (CompHausLike.toCompHausLike h).obj X = let_fun this := ⋯; CompHausLike.of P' ↑X.toTop

def CompHausLike.toCompHausLike {P : TopCat → Prop} {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : CategoryTheory.Functor (CompHausLike P) (CompHausLike P')

If P imples P', then there is a functor from CompHausLike P to CompHausLike P'.

Equations

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

def CompHausLike.fullyFaithfulToCompHausLike {P : TopCat → Prop} {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : (CompHausLike.toCompHausLike h).FullyFaithful

If P imples P', then the functor from CompHausLike P to CompHausLike P' is fully faithful.

Equations

• CompHausLike.fullyFaithfulToCompHausLike h = CategoryTheory.fullyFaithfulInducedFunctor fun (X : CompHausLike P) => let_fun this := ⋯; CompHausLike.of P' ↑X.toTop

instance CompHausLike.instFullToCompHausLike {P : TopCat → Prop} {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : (CompHausLike.toCompHausLike h).Full

Equations

• ⋯ = ⋯

instance CompHausLike.instFaithfulToCompHausLike {P : TopCat → Prop} {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) : (CompHausLike.toCompHausLike h).Faithful

Equations

• ⋯ = ⋯

@[simp]

theorem CompHausLike.compHausLikeToTop_obj (P : TopCat → Prop) (self : CompHausLike P) : (CompHausLike.compHausLikeToTop P).obj self = self.toTop

@[simp]

theorem CompHausLike.compHausLikeToTop_map (P : TopCat → Prop) : ∀ {X Y : CategoryTheory.InducedCategory TopCat CompHausLike.toTop} (f : X ⟶ Y), (CompHausLike.compHausLikeToTop P).map f = f

def CompHausLike.compHausLikeToTop (P : TopCat → Prop) : CategoryTheory.Functor (CompHausLike P) TopCat

The fully faithful embedding of CompHausLike P in TopCat.

Equations

• CompHausLike.compHausLikeToTop P = CategoryTheory.inducedFunctor CompHausLike.toTop

def CompHausLike.fullyFaithfulCompHausLikeToTop (P : TopCat → Prop) : (CompHausLike.compHausLikeToTop P).FullyFaithful

The functor from CompHausLike P to TopCat is fully faithful.

Equations

• CompHausLike.fullyFaithfulCompHausLikeToTop P = CategoryTheory.fullyFaithfulInducedFunctor CompHausLike.toTop

instance CompHausLike.instFullTopCatCompHausLikeToTop (P : TopCat → Prop) : (CompHausLike.compHausLikeToTop P).Full

Equations

• ⋯ = ⋯

instance CompHausLike.instFaithfulTopCatCompHausLikeToTop (P : TopCat → Prop) : (CompHausLike.compHausLikeToTop P).Faithful

Equations

• ⋯ = ⋯

instance CompHausLike.instCompactSpaceαTopologicalSpaceObjTopCatCompHausLikeToTop (P : TopCat → Prop) (X : CompHausLike P) : CompactSpace ↑((CompHausLike.compHausLikeToTop P).obj X)

Equations

• ⋯ = ⋯

instance CompHausLike.instT2SpaceαTopologicalSpaceObjTopCatCompHausLikeToTop (P : TopCat → Prop) (X : CompHausLike P) : T2Space ↑((CompHausLike.compHausLikeToTop P).obj X)

Equations

• ⋯ = ⋯

theorem CompHausLike.epi_of_surjective {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ⟶ Y) (hf : Function.Surjective ⇑f) : CategoryTheory.Epi f

theorem CompHausLike.mono_iff_injective {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

theorem CompHausLike.isClosedMap {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ⟶ Y) : IsClosedMap ⇑f

Any continuous function on compact Hausdorff spaces is a closed map.

theorem CompHausLike.isIso_of_bijective {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ⟶ Y) (bij : Function.Bijective ⇑f) : CategoryTheory.IsIso f

Any continuous bijection of compact Hausdorff spaces is an isomorphism.

instance CompHausLike.forget_reflectsIsomorphisms {P : TopCat → Prop} : (CategoryTheory.forget (CompHausLike P)).ReflectsIsomorphisms

Equations

• ⋯ = ⋯

noncomputable def CompHausLike.isoOfBijective {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ⟶ Y) (bij : Function.Bijective ⇑f) : X ≅ Y

Any continuous bijection of compact Hausdorff spaces induces an isomorphism.

Equations

• CompHausLike.isoOfBijective f bij = CategoryTheory.asIso f

@[simp]

theorem CompHausLike.isoOfHomeo_inv_apply {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) (a : ↑((CompHausLike.compHausLikeToTop P).obj Y)) : (CompHausLike.isoOfHomeo f).inv a = f.symm a

@[simp]

theorem CompHausLike.isoOfHomeo_hom_apply {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) (a : ↑((CompHausLike.compHausLikeToTop P).obj X)) : (CompHausLike.isoOfHomeo f).hom a = f a

def CompHausLike.isoOfHomeo {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : X ≅ Y

Construct an isomorphism from a homeomorphism.

Equations

• CompHausLike.isoOfHomeo f = (CompHausLike.fullyFaithfulCompHausLikeToTop P).preimageIso (TopCat.isoOfHomeo f)

@[simp]

theorem CompHausLike.homeoOfIso_apply {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ≅ Y) (a : ↑X.toTop) : (CompHausLike.homeoOfIso f) a = f.hom a

@[simp]

theorem CompHausLike.homeoOfIso_symm_apply {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ≅ Y) (a : ↑Y.toTop) : (CompHausLike.homeoOfIso f).symm a = f.inv a

def CompHausLike.homeoOfIso {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ≅ Y) : ↑X.toTop ≃ₜ ↑Y.toTop

Construct a homeomorphism from an isomorphism.

Equations

• CompHausLike.homeoOfIso f = TopCat.homeoOfIso ((CompHausLike.compHausLikeToTop P).mapIso f)

@[simp]

theorem CompHausLike.isoEquivHomeo_apply {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : X ≅ Y) : CompHausLike.isoEquivHomeo f = CompHausLike.homeoOfIso f

@[simp]

theorem CompHausLike.isoEquivHomeo_symm_apply {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : CompHausLike.isoEquivHomeo.symm f = CompHausLike.isoOfHomeo f

def CompHausLike.isoEquivHomeo {P : TopCat → Prop} {X : CompHausLike P} {Y : CompHausLike P} : (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)

The equivalence between isomorphisms in CompHaus and homeomorphisms of topological spaces.

Equations

• CompHausLike.isoEquivHomeo = { toFun := CompHausLike.homeoOfIso, invFun := CompHausLike.isoOfHomeo, left_inv := ⋯, right_inv := ⋯ }