Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit #8613

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit #8613

wants to merge 7 commits into from

Conversation

dagurtomas
Copy link
Collaborator

We allow the indexing category for the cofiltered limit in the result Profinite.exists_locallyConstant to live in a smaller universe than our profinite sets.

Open in Gitpod

@dagurtomas dagurtomas added awaiting-review The author would like community review of the PR awaiting-CI t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels Nov 24, 2023
@dagurtomas dagurtomas marked this pull request as ready for review November 24, 2023 14:33
@joelriou
Copy link
Collaborator

Since #8556 was merged, we should be able to state more general inequalities (not just v ≤ max u v): it should be possible to use the new UnivLE.{v, u} instead (which really means v ≤ u). @alreadydone may have more precise suggestions about this. (Is the rest of the limits API ready for this application to profinite sets, or are some more refactor necessary?)

@dagurtomas
Copy link
Collaborator Author

Given UnivLE.{v, u} Lean still doesn't seem to regard Type (max v u) and Type u as the same thing. In the API for limits in Type* there is some equivShrink business to deal with this and I'm not sure we have the API to do that in categories of topological spaces. AFAIK there is no homeoShrink?

joelriou
joelriou approved these changes Nov 29, 2023
View reviewed changes
Copy link
Collaborator

@joelriou joelriou left a comment •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR is an improvement: we shall fix the global universe inequalities issues later...

@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 29, 2023
@dagurtomas dagurtomas mentioned this pull request Nov 29, 2023
Closed
5 tasks
dagurtomas and others added 2 commits November 29, 2023 14:47
@dagurtomas @joelriou
Update Mathlib/Topology/Category/Profinite/Basic.lean
8acd2bf 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@dagurtomas @joelriou
Update Mathlib/Topology/Category/Profinite/Basic.lean
0b8e389 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@dagurtomas dagurtomas added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 29, 2023
@dagurtomas @github-actions
Update Mathlib/Topology/Category/Profinite/Basic.lean
ee240e4 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@dagurtomas dagurtomas mentioned this pull request Nov 29, 2023
Closed
6 tasks
@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Nov 30, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 30, 2023
@dagurtomas
chore(Profinite): allow more universe flexibility in Profinite/Cofilt…
ee1b50f 
…eredLimit (#8613)

We allow the indexing category for the cofiltered limit in the result `Profinite.exists_locallyConstant` to live in a smaller universe than our profinite sets.
@mathlib-bors
Copy link

mathlib-bors bot commented Nov 30, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit [Merged by Bors] - chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit Nov 30, 2023
@mathlib-bors mathlib-bors bot closed this Nov 30, 2023
@mathlib-bors mathlib-bors bot deleted the dagur_UniversesCofiltered branch November 30, 2023 11:39
alexkeizer pushed a commit that referenced this pull request Nov 30, 2023
@semorrison @alexkeizer
chore: bump Std, changes for leanprover-community/batteries#366
7cd93d7 
revert

.

fix a bit

blech

one more

comment out broken and unused results

chore: bump Std

remove redundant simp lemmas

cleanup

fix: make `Nat.testBit_bitwise` a simp-lemma again.

This fixes the Int.testbit_bitwise proofs

fix `castNum_testBit`

fix `testBit_eq_inth`

fixes

golf

golf

Apply suggestions from code review

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

fix whitespace

fix name conflict

more efficient

restore lemma

feat: Mapping extreme points under continuous maps (#8574)

Prove that extreme points are preserved under affine equivalences, and the less trivial statement that a continuous affine map sends extreme points of a compact set to a superset of the extreme
points of the image of that set.

Also fix a few name and tweak the API a bit.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit (#8613)

We allow the indexing category for the cofiltered limit in the result `Profinite.exists_locallyConstant` to live in a smaller universe than our profinite sets.

feat(CategoryTheory): `Preregular` and `FinitaryPreExtensive` implies `Precoherent` (#8643)

We prove some results about effective epimorphisms which allow us to deduce that a category which is `FinitaryPreExtensive` and `Preregular` is also `Precoherent`.

feat(Analysis/Seminorm): add more `*ball_smul_*ball` (#8724)

We had `ball_smul_ball` and `closedBall_smul_closedBall`.
Add versions with mixed `ball` and `closedBall`.
Also move this lemmas below and golf the proofs.

feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739)

fix breakage in BitVec lemmas
alexkeizer pushed a commit that referenced this pull request Nov 30, 2023
@semorrison @alexkeizer
chore: bump Std, changes for leanprover-community/batteries#366
fa7b97e 
revert

.

fix a bit

blech

one more

comment out broken and unused results

chore: bump Std

remove redundant simp lemmas

cleanup

fix: make `Nat.testBit_bitwise` a simp-lemma again.

This fixes the Int.testbit_bitwise proofs

fix `castNum_testBit`

fix `testBit_eq_inth`

fixes

golf

golf

Apply suggestions from code review

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

fix whitespace

fix name conflict

more efficient

restore lemma

feat: Mapping extreme points under continuous maps (#8574)

Prove that extreme points are preserved under affine equivalences, and the less trivial statement that a continuous affine map sends extreme points of a compact set to a superset of the extreme
points of the image of that set.

Also fix a few name and tweak the API a bit.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit (#8613)

We allow the indexing category for the cofiltered limit in the result `Profinite.exists_locallyConstant` to live in a smaller universe than our profinite sets.

feat(CategoryTheory): `Preregular` and `FinitaryPreExtensive` implies `Precoherent` (#8643)

We prove some results about effective epimorphisms which allow us to deduce that a category which is `FinitaryPreExtensive` and `Preregular` is also `Precoherent`.

feat(Analysis/Seminorm): add more `*ball_smul_*ball` (#8724)

We had `ball_smul_ball` and `closedBall_smul_closedBall`.
Add versions with mixed `ball` and `closedBall`.
Also move this lemmas below and golf the proofs.

feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739)

fix breakage in BitVec lemmas
awueth pushed a commit that referenced this pull request Dec 19, 2023
@dagurtomas @awueth
chore(Profinite): allow more universe flexibility in Profinite/Cofilt…
4b4d106 
…eredLimit (#8613)

We allow the indexing category for the cofiltered limit in the result `Profinite.exists_locallyConstant` to live in a smaller universe than our profinite sets.
This was referenced Jan 7, 2024
Closed
Closed
@dagurtomas dagurtomas mentioned this pull request Mar 22, 2024
Closed
7 tasks
mathlib-bors bot pushed a commit that referenced this pull request May 14, 2024
@dagurtomas
feat(Condensed): light condensed objects (#11586)
5602b56 
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585
callesonne pushed a commit that referenced this pull request May 16, 2024
@dagurtomas @callesonne
feat(Condensed): light condensed objects (#11586)
5972017 
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585
grunweg pushed a commit that referenced this pull request May 17, 2024
@dagurtomas @grunweg
feat(Condensed): light condensed objects (#11586)
c697b59 
New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone left review comments

@github-actions github-actions[bot] github-actions left review comments

@joelriou joelriou joelriou approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@dagurtomas @joelriou @riccardobrasca @alreadydone