[Merged by Bors] - refactor(Topology/Category): add CompHausLike.Basic by dagurtomas · Pull Request #13904 · leanprover-community/mathlib4

dagurtomas · 2024-06-17T20:35:26Z

This is the first part of the refactor of CompHaus and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see #12930)

github-actions · 2024-06-17T20:36:01Z

PR summary 676af2a8a2

Import changes

No significant changes to the import graph

Declarations diff

+ CompHausLike
+ HasProp
+ category
+ coe_comp
+ coe_id
+ coe_of
+ compHausLikeToTop
+ concreteCategory
+ epi_of_surjective
+ forget_reflectsIsomorphisms
+ fullyFaithfulCompHausLikeToTop
+ fullyFaithfulToCompHausLike
+ hasForget₂
+ homeoOfIso
+ instance (X : CompHausLike P) : CompactSpace ((compHausLikeToTop P).obj X)
+ instance (X : CompHausLike P) : T2Space ((compHausLikeToTop P).obj X)
+ instance (X : CompHausLike.{u} P) : CompactSpace ((forget (CompHausLike P)).obj X)
+ instance (X : CompHausLike.{u} P) : T2Space ((forget (CompHausLike P)).obj X)
+ instance (X : CompHausLike.{u} P) : TopologicalSpace ((forget (CompHausLike P)).obj X)
+ instance : (compHausLikeToTop P).Faithful
+ instance : (compHausLikeToTop P).Full
+ instance : (toCompHausLike h).Faithful := (fullyFaithfulToCompHausLike h).faithful
+ instance : (toCompHausLike h).Full := (fullyFaithfulToCompHausLike h).full
+ instance : CoeSort (CompHausLike P) (Type u)
+ isClosedMap
+ isIso_of_bijective
+ isoEquivHomeo
+ isoOfBijective
+ isoOfHomeo
+ mono_iff_injective
+ of
+ toCompHausLike

You can run this locally as follows

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

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

Mathlib/Topology/Category/CompHausLike/Basic.lean

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/Topology/Category/CompHausLike/Basic.lean

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/Topology/Category/CompHausLike/Basic.lean

joelriou · 2024-06-19T15:19:41Z

Thanks!

bors d+

mathlib-bors · 2024-06-19T15:19:43Z

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

dagurtomas · 2024-06-19T15:32:44Z

Thanks for the reviews!

bors merge

This is the first part of the refactor of `CompHaus` and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see #12930)

mathlib-bors · 2024-06-19T15:52:55Z

Pull request successfully merged into master.

Build succeeded:

This is the first part of the refactor of `CompHaus` and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see #12930)

refactor(Topology/Category): add CompHausLike.Basic

9de51ee

dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Jun 17, 2024

dagurtomas mentioned this pull request Jun 17, 2024

[Merged by Bors] - refactor(Topology/Category): add CompHausLike.Limits #13905

Closed

1 task

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 17, 2024

riccardobrasca reviewed Jun 18, 2024

View reviewed changes

Mathlib/Topology/Category/CompHausLike/Basic.lean Outdated Show resolved Hide resolved

dagurtomas commented Jun 18, 2024

View reviewed changes