Documentation

Mathlib.Topology.Category.CompHausLike.Basic

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:

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

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

```lean
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.

Instances For

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] :

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

hasProp : P (TopCat.of X)

Instances

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] :

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

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)

Instances For

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

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

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)

Instances For

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

@[simp]

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

CompHausLike.isoEquivHomeo f = CompHausLike.homeoOfIso 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 := ⋯ }

Instances For