[Merged by Bors] - feat(Topology): define compactly generated topological spaces

[dagurtomas]

---

• depends on: [Merged by Bors] - feat:(Condensed): the functor from TopCat to CondensedSet is a faithful right adjoint. #14455
• depends on: [Merged by Bors] - feat(CategoryTheory/Adjunction): left adjoint is faithful iff unit is mono, etc. #14490
• depends on: [Merged by Bors] - feat(LightCondensed): the functor from TopCat to LightCondSet is a faithful right adjoint #14506

[github-actions]

PR summary f796ab7361

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Category.CompactlyGenerated	1300

---

Declarations diff

+ CompactlyGenerated
+ CompactlyGeneratedSpace
+ TopologicalSpace.compactlyGenerated
+ compactlyGeneratedToTop
+ continuous_from_compactlyGenerated
+ continuous_from_compactlyGeneratedSpace
+ eq_compactlyGenerated
+ fullyFaithfulCompactlyGeneratedToTop
+ homeoOfIso
+ instance (X : Type w) [t : TopologicalSpace X] [DiscreteTopology X] :
+ instance : Category.{w, w+1} CompactlyGenerated.{u, w}
+ instance : CoeSort CompactlyGenerated Type*
+ instance : ConcreteCategory.{w} CompactlyGenerated.{u, w}
+ instance : Inhabited CompactlyGenerated.{u, w}
+ instance : compactlyGeneratedToTop.{u, w}.Faithful := fullyFaithfulCompactlyGeneratedToTop.faithful
+ instance : compactlyGeneratedToTop.{u, w}.Full := fullyFaithfulCompactlyGeneratedToTop.full
+ isoEquivHomeo
+ isoOfHomeo
+ of

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat:(Condensed): the functor from TopCat to CondensedSet is a faithful right adjoint. #14455
• [Merged by Bors] - feat(CategoryTheory/Adjunction): left adjoint is faithful iff unit is mono, etc. #14490
• [Merged by Bors] - feat(LightCondensed): the functor from TopCat to LightCondSet is a faithful right adjoint #14506
  By Dependent Issues (🤖). Happy coding!

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style