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.

def TopologicalSpace.compactlyGenerated (X : Type w) [TopologicalSpace X] : TopologicalSpace X

The compactly generated topology on a topological space X. This is the finest topology which makes all maps from compact Hausdorff spaces to X, which are continuous for the original topology, continuous.

Note: this definition should be used with an explicit universe parameter u for the size of the compact Hausdorff spaces mapping to X.

Equations

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

theorem continuous_from_compactlyGenerated {X : Type w} [TopologicalSpace X] {Y : Type u_1} [t : TopologicalSpace Y] (f : X → Y) (h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) : Continuous f

class CompactlyGeneratedSpace (X : Type w) [t : TopologicalSpace X] : Prop

A topological space X is compactly generated if its topology is finer than (and thus equal to) the compactly generated topology, i.e. it is coinduced by the continuous maps from compact Hausdorff spaces to X.

• le_compactlyGenerated : t ≤ TopologicalSpace.compactlyGenerated X

  The topology of X is finer than the compactly generated topology.

theorem CompactlyGeneratedSpace.le_compactlyGenerated {X : Type w} [t : TopologicalSpace X] [self : CompactlyGeneratedSpace X] : t ≤ TopologicalSpace.compactlyGenerated X

The topology of X is finer than the compactly generated topology.

theorem eq_compactlyGenerated {X : Type w} [t : TopologicalSpace X] [CompactlyGeneratedSpace X] : t = TopologicalSpace.compactlyGenerated X

instance instCompactlyGeneratedSpaceOfDiscreteTopology (X : Type w) [t : TopologicalSpace X] [DiscreteTopology X] : CompactlyGeneratedSpace X

Equations

• ⋯ = ⋯

theorem continuous_from_compactlyGeneratedSpace {X : Type w} [TopologicalSpace X] [CompactlyGeneratedSpace X] {Y : Type u_1} [TopologicalSpace Y] (f : X → Y) (h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) : Continuous f

theorem compactlyGeneratedSpace_of_continuous_maps {X : Type w} [t : TopologicalSpace X] (h : ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f) : CompactlyGeneratedSpace X

structure CompactlyGenerated : Type (w + 1)

The type of u-compactly generated w-small topological spaces.

• toTop : TopCat

  The underlying topological space of an object of CompactlyGenerated.

• is_compactly_generated : CompactlyGeneratedSpace ↑self.toTop

  The underlying topological space is compactly generated.

theorem CompactlyGenerated.is_compactly_generated (self : CompactlyGenerated) : CompactlyGeneratedSpace ↑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] [CompactlyGeneratedSpace 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_apply {X : CompactlyGenerated} {Y : CompactlyGenerated} (f : X ≅ Y) (a : (CategoryTheory.forget CompactlyGenerated).obj X) : (CompactlyGenerated.homeoOfIso f) a = f.hom a

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

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