Categories of Compact Hausdorff Spaces

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

Implementation

We define a structure CompHausLike which takes as an argument a predicate P on topological spaces. It consists of the data of a topological space, satisfying the additional properties of being compact and Hausdorff, and satisfying P. We give a category structure to CompHausLike P induced by the forgetful functor to topological spaces.

It used to be the case (before #12930 was merged) that several different categories of compact Hausdorff spaces, possibly satisfying some extra property, were defined from scratch in this way. For example, one would define a structure CompHaus as follows:

structure CompHaus where
  toTop : TopCat
  [is_compact : CompactSpace toTop]
  [is_hausdorff : T2Space toTop]

and give it the category structure induced from topological spaces. Then the category of profinite spaces was defined as follows:

structure Profinite where
  toCompHaus : CompHaus
  [isTotallyDisconnected : TotallyDisconnectedSpace toCompHaus]

The categories Stonean consisting of extremally disconnected compact Hausdorff spaces and LightProfinite consisting of totally disconnected, second countable compact Hausdorff spaces were defined in a similar way. This resulted in code duplication, and reducing this duplication was part of the motivation for introducing CompHausLike.

Using CompHausLike, we can now define CompHaus := CompHausLike (fun _ ↦ True) Profinite := CompHausLike (fun X ↦ TotallyDisconnectedSpace X). Stonean := CompHausLike (fun X ↦ ExtremallyDisconnected X). LightProfinite := CompHausLike (fun X ↦ TotallyDisconnectedSpace X ∧ SecondCountableTopology X).

These four categories are important building blocks of condensed objects (see the files Condensed.Basic and Condensed.Light.Basic). These categories share many properties and often, one wants to argue about several of them simultaneously. This is the other part of the motivation for introducing CompHausLike. On paper, one would say "let C be on of the categories CompHaus or Profinite, then the following holds: ...". This was not possible in Lean using the old definitions. Using the new definitions, this becomes a matter of identifying what common property of CompHaus and Profinite is used in the proof in question, and then proving the theorem for CompHausLike P satisfying that property, and it will automatically apply to both CompHaus and Profinite.

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} : ∀ {inst : 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

• ⋯ = ⋯

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.

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

• ⋯ = ⋯

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

@[simp]

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

@[simp]

theorem CompHausLike.compHausLikeToTop_obj (P : TopCat → Prop) (self : CompHausLike P) : (CompHausLike.compHausLikeToTop P).obj self = self.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

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

@[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.const {P : TopCat → Prop} (T : CompHausLike P) {S : CompHausLike P} (s : ↑S.toTop) : T ⟶ S

A constant map as a morphism in CompHausLike

Equations

• T.const s = ContinuousMap.const (↑T.toTop) s

theorem CompHausLike.const_comp {P : TopCat → Prop} {S : CompHausLike P} {T : CompHausLike P} {U : CompHausLike P} (s : ↑S.toTop) (g : S ⟶ U) : CategoryTheory.CategoryStruct.comp (T.const s) g = T.const (g s)