Delta-generated topological spaces #
The category of delta-generated spaces.
See https://ncatlab.org/nlab/show/Delta-generated+topological+space.
Adapted from Mathlib.Topology.Category.CompactlyGenerated
.
TODO #
DeltaGenerated
is cartesian-closed.
The type of delta-generated topological spaces.
- toTop : TopCat
the underlying topological space
- deltaGenerated : DeltaGeneratedSpace ↑self.toTop
The underlying topological space is delta-generated.
Instances For
Equations
- DeltaGenerated.instCoeSortType = { coe := fun (X : DeltaGenerated) => ↑X.toTop }
instance
DeltaGenerated.instConcreteCategoryContinuousMapCarrierToTop :
CategoryTheory.ConcreteCategory DeltaGenerated fun (x1 x2 : DeltaGenerated) => C(↑x1.toTop, ↑x2.toTop)
@[reducible, inline]
Constructor for objects of the category DeltaGenerated
Equations
- DeltaGenerated.of X = { toTop := TopCat.of X, deltaGenerated := inst✝ }
Instances For
The forgetful functor DeltaGenerated ⥤ TopCat
Instances For
@[simp]
@[simp]
theorem
DeltaGenerated.deltaGeneratedToTop_map
{X✝ Y✝ : CategoryTheory.InducedCategory TopCat toTop}
(f : X✝ ⟶ Y✝)
:
The faithful (but not full) functor taking each topological space to its delta-generated coreflection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
The adjunction between the forgetful functor DeltaGenerated ⥤ TopCat
and its coreflector.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The category of delta-generated spaces is coreflective in the category of topological spaces.