Theorems · Definition · category theory
GeneratedByTopCat.adj
{ι : Type t} →
{X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → GeneratedByTopCat.toTopCat ⊣ TopCat.toGeneratedByTopCatThe adjunction between the categories GeneratedByTopCat X and TopCat.
The left adjoint is the inclusion functor, and the right adjoint sends
a topological space Y to the underlying type of Y endowed with
the X-generated topology.
- Defined in
- Mathlib.Topology.Convenient.Category
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- CategoryTheory.Iso.homproof · cited by 7,684
- TopCatstatement · cited by 1,889
- CategoryTheory.Adjunctionstatement · cited by 524
- TopCat.generatedBystatement · cited by 11
- GeneratedByTopCatstatement · cited by 10
- GeneratedByTopCat.toTopCatstatement · cited by 2
- TopCat.toGeneratedByTopCatstatement · cited by 2
- GeneratedByTopCat.adjCounitproof · cited by 1
- GeneratedByTopCat.adjUnitIsoproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- DeltaGenerated.coreflectorAdjunctionproof · cited by 0
- GeneratedByTopCat.adj_counitstatement and proof · cited by 0
- GeneratedByTopCat.adj_unitstatement and proof · cited by 0