[Merged by Bors] - refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces by dagurtomas · Pull Request #13319 · leanprover-community/mathlib4

dagurtomas · 2024-05-28T15:27:30Z

Changes the definition of LightProfinite to the category of second countable totally disconnected compact Hausdorff spaces. The old LightProfinite is renamed to LightDiagram and we give an equivalence of categories between them.

This changes LightProfinite.Basic to match Profinite.Basic more closely. It also contains the equivalence of categories with LightDiagram and an EssentiallySmall instance.

The Limits and EffectiveEpi files now match their counterparts for Profinite more closely as well.

This PR also adds a new feature: LightProfinite has countable limits and the functor to Profinite creates countable limits.

…s second countable

Co-authored-by: Johan Commelin <johan@commelin.net>

…ountable profinite spaces

github-actions · 2024-06-07T22:59:22Z

PR summary fac1429c0e

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Category.LightProfinite.IsLight	1277	0	-1277 (-100.00%)
Mathlib.Topology.Category.LightProfinite.Basic	1259	1274	+15 (+1.19%)
Mathlib.Topology.Category.LightProfinite.Limits	1302	1301	-1 (-0.08%)
Mathlib.Topology.Category.LightProfinite.EffectiveEpi	1326	1325	-1 (-0.08%)

Declarations diff

+ FintypeCat.toLightProfiniteFullyFaithful
+ LightDiagram
+ LightDiagram'
+ LightDiagram'.toLightFunctor
+ LightDiagram'.toProfinite
+ LightDiagram.equivSmall
+ LightProfinite.equivDiagram
+ LightProfinite.toCompHaus_comp_toTop
+ LightProfinite.toTopCat
+ LightProfinite.toTopCatFullyFaithful
+ Sigma.ι_comp_toFiniteCoproduct
+ category
+ coe_comp
+ coe_id
+ coproductHomeoCoproduct
+ coproductIsoCoproduct
+ createsCountableLimits
+ finiteCoproduct.ι_desc_apply
+ finiteCoproduct.ι_injective
+ finiteCoproduct.ι_jointly_surjective
+ forget_reflectsIsomorphisms
+ hasForget₂
+ homeoOfIso
+ instCountableDiscreteQuotient
+ instance (S : LightDiagram.{u}) : SecondCountableTopology S.cone.pt := by
+ instance (S : LightProfinite) : Countable (Clopens S) := by
+ instance (X : LightProfinite) :
+ instance : Category LightDiagram := InducedCategory.category toProfinite
+ instance : Category LightDiagram' := InducedCategory.category LightDiagram'.toProfinite
+ instance : CoeSort LightProfinite (Type*)
+ instance : EssentiallySmall LightDiagram.{u}
+ instance : FinitaryExtensive LightProfinite.{u}
+ instance : FintypeCat.toLightProfinite.Faithful
+ instance : FintypeCat.toLightProfinite.Full
+ instance : HasCountableLimits LightProfinite
+ instance : Inhabited LightProfinite
+ instance : LightDiagram'.toLightFunctor.IsEquivalence
+ instance : LightDiagram'.toLightFunctor.{u}.EssSurj
+ instance : LightDiagram'.toLightFunctor.{u}.Faithful := ⟨id⟩
+ instance : LightDiagram'.toLightFunctor.{u}.Full
+ instance : LightProfinite.toTopCat.Faithful := LightProfinite.toTopCatFullyFaithful.faithful
+ instance : LightProfinite.toTopCat.Full := LightProfinite.toTopCatFullyFaithful.full
+ instance : Precoherent LightProfinite.{u} := inferInstance
+ instance : lightDiagramToLightProfinite.IsEquivalence
+ instance : lightDiagramToProfinite.Faithful := show (inducedFunctor _).Faithful from inferInstance
+ instance : lightDiagramToProfinite.Full := show (inducedFunctor _).Full from inferInstance
+ instance : lightProfiniteToCompHaus.Faithful := lightProfiniteToCompHausFullyFaithful.faithful
+ instance : lightProfiniteToCompHaus.Full := lightProfiniteToCompHausFullyFaithful.full
+ instance : lightProfiniteToLightDiagram.IsEquivalence
+ instance : lightToProfinite.Faithful := lightToProfiniteFullyFaithful.faithful
+ instance : lightToProfinite.Full := lightToProfiniteFullyFaithful.full
+ instance {J : Type v} [SmallCategory J] (F : J ⥤ LightProfinite.{max u v}) :
+ instance {X : LightDiagram} : CompactSpace ((forget LightDiagram).obj X)
+ instance {X : LightDiagram} : T2Space ((forget LightDiagram).obj X)
+ instance {X : LightDiagram} : TopologicalSpace ((forget LightDiagram).obj X)
+ instance {X : LightDiagram} : TotallyDisconnectedSpace ((forget LightDiagram).obj X)
+ instance {X : LightProfinite} : SecondCountableTopology ((forget LightProfinite).obj X)
+ instance {X : LightProfinite} : SecondCountableTopology (lightProfiniteToCompHaus.obj X)
+ instance {X : LightProfinite} : SecondCountableTopology X
+ instance {X : LightProfinite} : TotallyDisconnectedSpace (lightProfiniteToCompHaus.obj X)
+ instance {X : LightProfinite} : TotallyDisconnectedSpace X
+ instance {X Y : LightProfinite} (f : X ⟶ Y) [@Epi CompHaus _ _ _ f] : Epi f := by
+ instance {X Y : LightProfinite} (f : X ⟶ Y) [Epi f] : @Epi CompHaus _ _ _ f := by
+ isClosedMap
+ isIso_of_bijective
+ isoEquivHomeo
+ isoOfBijective
+ isoOfHomeo
+ lightDiagramToLightProfinite
+ lightDiagramToProfinite
+ lightProfiniteToCompHaus
+ lightProfiniteToCompHausFullyFaithful
+ lightProfiniteToLightDiagram
+ lightToProfiniteFullyFaithful
+ limitCone
+ limitConeIsLimit
+ mono_iff_injective
+ pullbackHomeoPullback
+ pullbackIsoPullback
+ pullback_fst_eq
+ pullback_snd_eq
+ toLightDiagram
+-+ concreteCategory
- IsLight
- LightProfinite'
- LightProfinite'.toLightFunctor
- LightProfinite'.toProfinite
- LightProfinite.equivSmall
- ext
- fintypeCatToLightProfinite
- instCountableDiscreteQuotientOfIsLight
- instIsLightProd
- instance (S : LightProfinite.{u}) : (lightToProfinite.obj S).IsLight
- instance (S : LightProfinite.{u}) : S.toProfinite.IsLight
- instance (X : LightProfinite) : Unique (X ⟶ (FintypeCat.of PUnit.{u+1}).toLightProfinite)
- instance : Category LightProfinite := InducedCategory.category toProfinite
- instance : Category LightProfinite' := InducedCategory.category LightProfinite'.toProfinite
- instance : FinitaryExtensive LightProfinite
- instance : LightProfinite'.toLightFunctor.IsEquivalence
- instance : LightProfinite'.toLightFunctor.{u}.EssSurj
- instance : LightProfinite'.toLightFunctor.{u}.Faithful := ⟨id⟩
- instance : LightProfinite'.toLightFunctor.{u}.Full
- instance : Precoherent LightProfinite := inferInstance
- instance : fintypeCatToLightProfinite.Faithful
- instance : fintypeCatToLightProfinite.Full
- instance : lightToProfinite.Faithful := show (inducedFunctor _).Faithful from inferInstance
- instance : lightToProfinite.Full := show (inducedFunctor _).Full from inferInstance
- instance : toTopCat.Faithful := Functor.Faithful.comp _ _
- instance : toTopCat.Full := Functor.Full.comp _ _
- instance [Mono f] : IsIso ((Profinite.limitConeIsLimit ((lightProfiniteDiagramOfHom f) ⋙
- instance {X Y B : LightProfinite} (f : X ⟶ B) (g : Y ⟶ B) : HasLimit (cospan f g)
- instance {X Y B : Profinite.{u}} (f : X ⟶ B) (g : Y ⟶ B) [X.IsLight] [Y.IsLight] :
- instance {α : Type w} [Finite α] (X : α → Profinite.{max u w}) [∀ a, (X a).IsLight] :
- isLight_of_mono
- lightProfiniteConeOfHom
- lightProfiniteConeOfHom_π_app
- lightProfiniteConeOfHom_π_app'
- lightProfiniteDiagramOfHom
- lightProfiniteIsLimitOfMono
- lightProfiniteOfMono
- ofIsLight
- toTopCat

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>

kbuzzard

This looks great to me -- almost ready to go. I left some small comments.

Mathlib/Topology/Category/LightProfinite/Basic.lean

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

kbuzzard · 2024-06-11T13:03:46Z

Thanks a lot!

bors merge

…ountable profinite spaces (#13319) Changes the definition of `LightProfinite` to the category of second countable totally disconnected compact Hausdorff spaces. The old `LightProfinite` is renamed to `LightDiagram` and we give an equivalence of categories between them. This changes `LightProfinite.Basic` to match `Profinite.Basic` more closely. It also contains the equivalence of categories with `LightDiagram` and an `EssentiallySmall` instance. The `Limits` and `EffectiveEpi` files now match their counterparts for `Profinite` more closely as well. This PR also adds a new feature: `LightProfinite` has countable limits and the functor to `Profinite` creates countable limits.

mathlib-bors · 2024-06-11T13:49:30Z

Pull request successfully merged into master.

Build succeeded:

…ountable profinite spaces (#13319) Changes the definition of `LightProfinite` to the category of second countable totally disconnected compact Hausdorff spaces. The old `LightProfinite` is renamed to `LightDiagram` and we give an equivalence of categories between them. This changes `LightProfinite.Basic` to match `Profinite.Basic` more closely. It also contains the equivalence of categories with `LightDiagram` and an `EssentiallySmall` instance. The `Limits` and `EffectiveEpi` files now match their counterparts for `Profinite` more closely as well. This PR also adds a new feature: `LightProfinite` has countable limits and the functor to `Profinite` creates countable limits.

- [x] depends on: #13319 - [x] depends on: #13355

dagurtomas and others added 10 commits May 17, 2024 14:23

feat(Topology): a profinite space has countably many clopens iff it i…

1747555

…s second countable

golf

4b76e3e

Update Compact.lean

13ca0cf

Merge branch 'master' into dagur/SecondCountableClopens

6541d50

Merge branch 'master' into dagur/SecondCountableClopens

86a2011

golf

42e26ad

Update Mathlib/Topology/Compactness/Compact.lean

2a24309

Co-authored-by: Johan Commelin <johan@commelin.net>

Update Mathlib/Topology/Compactness/Compact.lean

d3960af

Co-authored-by: Johan Commelin <johan@commelin.net>

fix errors

af3c9a2

refactor(LightProfinite): redefine light profinite spaces as second c…

508dace

…ountable profinite spaces

dagurtomas added the WIP Work in progress label May 28, 2024

dagurtomas added 5 commits May 28, 2024 16:29

aslimit file

8fa0af9

remove file for future PR

31f7ff8

mathlib file

e36c047

Merge branch 'master' into dagur/LightProfiniteRefactor

94d5bd4

lint

e3b89d3

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 and removed WIP Work in progress labels May 28, 2024

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

dagurtomas added 5 commits May 30, 2024 09:02

Merge branch 'master' into dagur/LightProfiniteRefactor

aa3c52c

fix merge errors

d8e49ab

Merge branch 'master' into dagur/LightProfiniteRefactor

812fb56

fix error

132d31e

fix typos

a55eab2

dagurtomas mentioned this pull request Jun 4, 2024

[Merged by Bors] - feat(CategoryTheory): a sequential limit of surjections is surjective #13507

Closed

1 task

Merge branch 'master' into dagur/LightProfiniteRefactor

8576ed6

dagurtomas added 5 commits June 10, 2024 14:11

Merge branch 'master' into dagur/LightProfiniteRefactor

64a0097

improve diff

da85001

improve diff

d352013

improve diff

f8b61fa

terminal object

ab5a457

kbuzzard approved these changes Jun 11, 2024

View reviewed changes

kbuzzard added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 11, 2024

dagurtomas and others added 3 commits June 11, 2024 13:18

Apply suggestions from code review

5e6d687

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

apply suggestions

6ce4c42

lint

fac1429

dagurtomas added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 11, 2024

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

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 11, 2024

mathlib-bors bot changed the title ~~refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces~~ [Merged by Bors] - refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces Jun 11, 2024

mathlib-bors bot closed this Jun 11, 2024

mathlib-bors bot deleted the dagur/LightProfiniteRefactor branch June 11, 2024 13:49

mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024

feat(LightProfinite): define ℕ∪{∞} as a light profinite set (#13358)

31c0e2a

- [x] depends on: #13319 - [x] depends on: #13355

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces#13319

[Merged by Bors] - refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces#13319
dagurtomas wants to merge 29 commits intomasterfrom
dagur/LightProfiniteRefactor

dagurtomas commented May 28, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Jun 7, 2024 •

edited

Loading

Declarations diff

Uh oh!

kbuzzard left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kbuzzard commented Jun 11, 2024

Uh oh!

mathlib-bors bot commented Jun 11, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

dagurtomas commented May 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary fac1429c0e

Import changes

Declarations diff

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kbuzzard commented Jun 11, 2024

Uh oh!

mathlib-bors bot commented Jun 11, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

dagurtomas commented May 28, 2024 •

edited

Loading

github-actions bot commented Jun 7, 2024 •

edited

Loading