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.

instance CompactlyGenerated.instInhabited : Inhabited CompactlyGenerated

Equations

• CompactlyGenerated.instInhabited = { default := CompactlyGenerated.mk (TopCat.of (ULift.{?u.3, 0} (Fin 37))) }

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.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory CompactlyGenerated fun (x1 x2 : CompactlyGenerated) => C(↑x1.toTop, ↑x2.toTop)

Equations

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

@[reducible, inline]

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

@[reducible, inline]

abbrev CompactlyGenerated.ofHom {X : Type w} [TopologicalSpace X] [UCompactlyGeneratedSpace X] {Y : Type w} [TopologicalSpace Y] [UCompactlyGeneratedSpace Y] (f : C(X, Y)) : of X ⟶ of Y

Typecheck a ContinuousMap as a morphism in CompactlyGenerated.

Equations

• CompactlyGenerated.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def CompactlyGenerated.compactlyGeneratedToTop : CategoryTheory.Functor CompactlyGenerated TopCat

The fully faithful embedding of CompactlyGenerated in TopCat.

Equations

• CompactlyGenerated.compactlyGeneratedToTop = CategoryTheory.inducedFunctor CompactlyGenerated.toTop

@[simp]

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

@[simp]

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

def CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop : compactlyGeneratedToTop.FullyFaithful

compactlyGeneratedToTop is fully faithful.

Equations

• CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop = CategoryTheory.fullyFaithfulInducedFunctor CompactlyGenerated.toTop

instance CompactlyGenerated.instFullTopCatCompactlyGeneratedToTop : compactlyGeneratedToTop.Full

instance CompactlyGenerated.instFaithfulTopCatCompactlyGeneratedToTop : compactlyGeneratedToTop.Faithful

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

Construct an isomorphism from a homeomorphism.

Equations

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

@[simp]

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

@[simp]

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

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

Construct a homeomorphism from an isomorphism.

Equations

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

@[simp]

theorem CompactlyGenerated.homeoOfIso_symm_apply {X Y : CompactlyGenerated} (f : X ≅ Y) (a : ↑Y.toTop) : (homeoOfIso f).symm a = (CategoryTheory.ConcreteCategory.hom f.inv) a

@[simp]

theorem CompactlyGenerated.homeoOfIso_apply {X Y : CompactlyGenerated} (f : X ≅ Y) (a : ↑X.toTop) : (homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom) a

def CompactlyGenerated.isoEquivHomeo {X 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 := ⋯ }

@[simp]

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

@[simp]

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