Compactly generated topological spaces

This file defines the category of compactly generated topological spaces. These are spaces X such that a map f : X → Y is continuous whenever the composition S → X → Y is continuous for all compact Hausdorff spaces S mapping continuously to X.

TODO

• CompactlyGenerated is a reflective subcategory of TopCat.
• CompactlyGenerated is cartesian closed.
• Every first-countable space is u-compactly generated for every universe u.

structure CompactlyGenerated : Type (w + 1)

CompactlyGenerated.{u, w} is the type of u-compactly generated w-small topological spaces. This should always be used with explicit universe parameters.

• toTop : TopCat

  The underlying topological space of an object of CompactlyGenerated.

• is_compactly_generated : UCompactlyGeneratedSpace ↑self.toTop

  The underlying topological space is compactly generated.

theorem CompactlyGenerated.is_compactly_generated (self : CompactlyGenerated) : UCompactlyGeneratedSpace ↑self.toTop

The underlying topological space is compactly generated.

instance CompactlyGenerated.instInhabited : Inhabited CompactlyGenerated

Equations

• CompactlyGenerated.instInhabited = { default := CompactlyGenerated.mk { α := ULift.{w, 0} (Fin 37), str := inferInstance } }

instance CompactlyGenerated.instCoeSortType : CoeSort CompactlyGenerated (Type u_1)

Equations

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

instance CompactlyGenerated.instCategory : CategoryTheory.Category.{w, w + 1} CompactlyGenerated

Equations

• CompactlyGenerated.instCategory = CategoryTheory.InducedCategory.category CompactlyGenerated.toTop

instance CompactlyGenerated.instConcreteCategory : CategoryTheory.ConcreteCategory CompactlyGenerated

Equations

• CompactlyGenerated.instConcreteCategory = CategoryTheory.InducedCategory.concreteCategory CompactlyGenerated.toTop

def CompactlyGenerated.of (X : Type w) [TopologicalSpace X] [UCompactlyGeneratedSpace X] : CompactlyGenerated

Constructor for objects of the category CompactlyGenerated.

Equations

• CompactlyGenerated.of X = CompactlyGenerated.mk (TopCat.of X)

@[simp]

theorem CompactlyGenerated.compactlyGeneratedToTop_map : ∀ {X Y : CategoryTheory.InducedCategory TopCat CompactlyGenerated.toTop} (f : X ⟶ Y), CompactlyGenerated.compactlyGeneratedToTop.map f = f

@[simp]

theorem CompactlyGenerated.compactlyGeneratedToTop_obj (self : CompactlyGenerated) : CompactlyGenerated.compactlyGeneratedToTop.obj self = self.toTop

def CompactlyGenerated.compactlyGeneratedToTop : CategoryTheory.Functor CompactlyGenerated TopCat

The fully faithful embedding of CompactlyGenerated in TopCat.

Equations

• CompactlyGenerated.compactlyGeneratedToTop = CategoryTheory.inducedFunctor CompactlyGenerated.toTop

def CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop : CompactlyGenerated.compactlyGeneratedToTop.FullyFaithful

compactlyGeneratedToTop is fully faithful.

Equations

• CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop = CategoryTheory.fullyFaithfulInducedFunctor CompactlyGenerated.toTop

instance CompactlyGenerated.instFullTopCatCompactlyGeneratedToTop : CompactlyGenerated.compactlyGeneratedToTop.Full

Equations

• CompactlyGenerated.instFullTopCatCompactlyGeneratedToTop = ⋯

instance CompactlyGenerated.instFaithfulTopCatCompactlyGeneratedToTop : CompactlyGenerated.compactlyGeneratedToTop.Faithful

Equations

• CompactlyGenerated.instFaithfulTopCatCompactlyGeneratedToTop = ⋯

@[simp]

theorem CompactlyGenerated.isoOfHomeo_hom {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (CompactlyGenerated.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }

@[simp]

theorem CompactlyGenerated.isoOfHomeo_inv {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (CompactlyGenerated.isoOfHomeo f).inv = { toFun := ⇑f.symm, continuous_toFun := ⋯ }

def CompactlyGenerated.isoOfHomeo {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : X ≅ Y

Construct an isomorphism from a homeomorphism.

Equations

• CompactlyGenerated.isoOfHomeo f = { hom := { toFun := ⇑f, continuous_toFun := ⋯ }, inv := { toFun := ⇑f.symm, continuous_toFun := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CompactlyGenerated.homeoOfIso_symm_apply {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : X ≅ Y) (a : (CategoryTheory.forget CompactlyGenerated).obj Y) : (CompactlyGenerated.homeoOfIso f).symm a = f.inv a

@[simp]

theorem CompactlyGenerated.homeoOfIso_apply {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : X ≅ Y) (a : (CategoryTheory.forget CompactlyGenerated).obj X) : (CompactlyGenerated.homeoOfIso f) a = f.hom a

def CompactlyGenerated.homeoOfIso {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : X ≅ Y) : ↑X.toTop ≃ₜ ↑Y.toTop

Construct a homeomorphism from an isomorphism.

Equations

• CompactlyGenerated.homeoOfIso f = { toFun := ⇑f.hom, invFun := ⇑f.inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem CompactlyGenerated.isoEquivHomeo_symm_apply {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : CompactlyGenerated.isoEquivHomeo.symm f = CompactlyGenerated.isoOfHomeo f

@[simp]

theorem CompactlyGenerated.isoEquivHomeo_apply {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : X ≅ Y) : CompactlyGenerated.isoEquivHomeo f = CompactlyGenerated.homeoOfIso f

def CompactlyGenerated.isoEquivHomeo {X : CompactlyGenerated} {Y : CompactlyGenerated} : (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)

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

Equations

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