Skip to content

[Merged by Bors] - feat(Topology/Profinite): extending cones in Profinite and LightProfinite#14382

Closed
dagurtomas wants to merge 13 commits intomasterfrom
dagur/ProfiniteExtend
Closed

[Merged by Bors] - feat(Topology/Profinite): extending cones in Profinite and LightProfinite#14382
dagurtomas wants to merge 13 commits intomasterfrom
dagur/ProfiniteExtend

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Jul 3, 2024 •
edited
Loading

Let (Sᵢ)_{i : I} be a family of finite sets indexed by a cofiltered category I and let S be
its limit in Profinite. Let G be a functor from Profinite to a category C and suppose that
G preserves the limit described above. Suppose further that the projection maps S ⟶ Sᵢ are
epimorphic for all i. Then G.obj S is isomorphic to a limit indexed by
StructuredArrow S toProfinite (see Profinite.Extend.isLimitCone).

We also provide the dual result for a functor of the form G : Profiniteᵒᵖ ⥤ C.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 3, 2024 •
edited
Loading

PR summary 2460397ecb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Topology.Category.Profinite.Extend 1351
Mathlib.Topology.Category.LightProfinite.Extend 1359

Declarations diff

+ exists_hom
+ instance (i : DiscreteQuotient S) : Epi (S.asLimitCone.π.app i)
+ instance (i : ℕᵒᵖ) : Epi (S.asLimitCone.π.app i)
+ instance : lightToProfinite.PreservesEpimorphisms
++ asLimit'
++ asLimitCone'
++ cocone
++ cone
++ diagram'
++ fintypeDiagram'
++ functor
++ functorOp
++ functorOp_final
++ functor_initial
++ isColimitCocone
++ isLimitCone
++ lim'

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

@dagurtomas dagurtomas added the WIP Work in progress label Jul 3, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 17, 2024
dagurtomas
dagurtomas commented Jul 31, 2024
View reviewed changes
dagurtomas
dagurtomas commented Jul 31, 2024
View reviewed changes
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 31, 2024
@dagurtomas dagurtomas changed the title feat(Topology/Profinite): profinite sets as Kan extensions feat(Topology/Profinite): extending cones in Profinite and LightProfinite Aug 6, 2024
@dagurtomas dagurtomas added t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters and removed WIP Work in progress labels Aug 6, 2024
@dagurtomas dagurtomas mentioned this pull request Aug 6, 2024
Closed
11 tasks
@dagurtomas dagurtomas mentioned this pull request Aug 6, 2024
Closed
6 tasks
@faenuccio faenuccio assigned faenuccio and adamtopaz and unassigned faenuccio Aug 27, 2024
adamtopaz
adamtopaz reviewed Aug 29, 2024
View reviewed changes
adamtopaz
adamtopaz reviewed Aug 29, 2024
View reviewed changes
adamtopaz
adamtopaz reviewed Aug 29, 2024
View reviewed changes
adamtopaz
adamtopaz reviewed Aug 29, 2024
View reviewed changes
adamtopaz
adamtopaz reviewed Aug 29, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@adamtopaz adamtopaz left a comment

Choose a reason for hiding this comment

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

Looks good! I had a few suggestions which are fairly minor. I assume you're preparing to relate Profinite.extend and friends to Kan extensions?

@adamtopaz adamtopaz added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 29, 2024
dagurtomas and others added 3 commits August 30, 2024 10:30
@dagurtomas @adamtopaz
Apply suggestions from code review
04efa93 
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
@dagurtomas
make fintypeDiagram'
a2121c2
@dagurtomas
add todo in docstring
2460397
@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Aug 30, 2024

I assume you're preparing to relate Profinite.extend and friends to Kan extensions?

Yes, see #15566, specifcally https://github.com/leanprover-community/mathlib4/blob/f7f43971b46ef2041f517cdd1c4d9440158a9dde/Mathlib/Condensed/Discrete/Colimit.lean

@dagurtomas dagurtomas removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 30, 2024
@adamtopaz
Copy link
Copy Markdown
Contributor

adamtopaz commented Aug 31, 2024

Thanks!
bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 31, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 31, 2024
@dagurtomas
feat(Topology/Profinite): extending cones in Profinite and `LightPr…
a07b93e 
…ofinite` (#14382)

Let `(Sᵢ)_{i : I}` be a family of finite sets indexed by a cofiltered category `I` and let `S` be
its limit in `Profinite`. Let `G` be a functor from `Profinite` to a category `C` and suppose that
`G` preserves the limit described above. Suppose further that the projection maps `S ⟶ Sᵢ` are
epimorphic for all `i`. Then `G.obj S` is isomorphic to a limit indexed by
`StructuredArrow S toProfinite` (see `Profinite.Extend.isLimitCone`).

We also provide the dual result for a functor of the form `G : Profiniteᵒᵖ ⥤ C`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology/Profinite): extending cones in Profinite and LightProfinite [Merged by Bors] - feat(Topology/Profinite): extending cones in Profinite and LightProfinite Aug 31, 2024
@mathlib-bors mathlib-bors bot closed this Aug 31, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/ProfiniteExtend branch August 31, 2024 20:17
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@dagurtomas @bjoernkjoshanssen
feat(Topology/Profinite): extending cones in Profinite and `LightPr…
c4a04a0 
…ofinite` (#14382)

Let `(Sᵢ)_{i : I}` be a family of finite sets indexed by a cofiltered category `I` and let `S` be
its limit in `Profinite`. Let `G` be a functor from `Profinite` to a category `C` and suppose that
`G` preserves the limit described above. Suppose further that the projection maps `S ⟶ Sᵢ` are
epimorphic for all `i`. Then `G.obj S` is isomorphic to a limit indexed by
`StructuredArrow S toProfinite` (see `Profinite.Extend.isLimitCone`).

We also provide the dual result for a functor of the form `G : Profiniteᵒᵖ ⥤ C`.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@dagurtomas @bjoernkjoshanssen
feat(Topology/Profinite): extending cones in Profinite and `LightPr…
2e85f7d 
…ofinite` (#14382)

Let `(Sᵢ)_{i : I}` be a family of finite sets indexed by a cofiltered category `I` and let `S` be
its limit in `Profinite`. Let `G` be a functor from `Profinite` to a category `C` and suppose that
`G` preserves the limit described above. Suppose further that the projection maps `S ⟶ Sᵢ` are
epimorphic for all `i`. Then `G.obj S` is isomorphic to a limit indexed by
`StructuredArrow S toProfinite` (see `Profinite.Extend.isLimitCone`).

We also provide the dual result for a functor of the form `G : Profiniteᵒᵖ ⥤ C`.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@dagurtomas @bjoernkjoshanssen
feat(Topology/Profinite): extending cones in Profinite and `LightPr…
5b7e040 
…ofinite` (#14382)

Let `(Sᵢ)_{i : I}` be a family of finite sets indexed by a cofiltered category `I` and let `S` be
its limit in `Profinite`. Let `G` be a functor from `Profinite` to a category `C` and suppose that
`G` preserves the limit described above. Suppose further that the projection maps `S ⟶ Sᵢ` are
epimorphic for all `i`. Then `G.obj S` is isomorphic to a limit indexed by
`StructuredArrow S toProfinite` (see `Profinite.Extend.isLimitCone`).

We also provide the dual result for a functor of the form `G : Profiniteᵒᵖ ⥤ C`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@adamtopaz adamtopaz adamtopaz left review comments

Assignees

@adamtopaz adamtopaz

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.

3 participants

@dagurtomas @adamtopaz @faenuccio