[Merged by Bors] - refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures by Thmoas-Guan · Pull Request #20740 · leanprover-community/mathlib4

Thmoas-Guan · 2025-01-14T14:28:23Z

Refactor morphisms in ProfiniteGrp into one-field structure.

still need API from ContinuousMulEquiv

github-actions · 2025-01-14T14:29:18Z

messageFile.md

chrisflav · 2025-01-15T04:48:23Z

Could you please add a test file in MathlibTest, similar to the one for AlgebraCat?

Vierkantor

Thank you for taking this on! I'm happy to see the amount of required changes was much less than for some of the other concrete categories. :)

A few small remarks.

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Vierkantor · 2025-01-16T09:30:25Z

I think this is pretty much good to go. I am less convinced we need that extra test file, since we do exactly the same as for AlgebraCat/ModuleCat/RingCat, so there should not be any surprises. But those tests are quite helpful for my follow-up work on the concrete category class. So I certainly wouldn't oppose more test files :)

Thmoas-Guan · 2025-01-16T09:35:57Z

I think this is pretty much good to go. I am less convinced we need that extra test file, since we do exactly the same as for AlgebraCat/ModuleCat/RingCat, so there should not be any surprises. But those tests are quite helpful for my follow-up work on the concrete category class. So I certainly wouldn't oppose more test files :)

So which one do you prefer? Adding test file right in this PR or in another one?

Vierkantor · 2025-01-16T09:41:48Z

We should add it in this PR definitely. (Assuming you want to add it at all: having thought about it a bit more, I'm in favour of having the test file, but will not insist if you are not.)

Thmoas-Guan · 2025-01-16T10:10:17Z

We should add it in this PR definitely. (Assuming you want to add it at all: having thought about it a bit more, I'm in favour of having the test file, but will not insist if you are not.)

Currently, 9 out of 14 failed.... I may need some time to fix.
Probably because of ContinuousMonoidHom is missing API every where....

and add missing API of ContinuousMonoidHom

github-actions · 2025-01-16T11:06:51Z

messageFile.md

chrisflav · 2025-01-16T16:51:28Z

We should add it in this PR definitely. (Assuming you want to add it at all: having thought about it a bit more, I'm in favour of having the test file, but will not insist if you are not.)

Currently, 9 out of 14 failed.... I may need some time to fix. Probably because of ContinuousMonoidHom is missing API every where....

This is why I wanted the test file :) Thanks!

github-actions · 2025-01-17T02:44:18Z

PR summary 022323a991

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ProfiniteAddGrp.Hom
+ ProfiniteGrp.Hom
+ ProfiniteGrp.coe_of
+ ProfiniteGrp.of
+ ProfiniteGrp.ofHom
+ coe_comp
+ coe_id
+ comp_apply
+ hom_comp
+ hom_ext
+ hom_id
+ hom_inv_apply
+ hom_ofHom
+ id_apply
+ instance : (forget₂ ProfiniteGrp Profinite).Faithful := {
+ instance : Group (Profinite.limitCone (F ⋙ (forget₂ ProfiniteGrp Profinite))).pt
+ instance : HasForget₂ ProfiniteGrp Profinite
+ instance : Limits.PreservesLimits (forget₂ ProfiniteGrp Profinite)
+ instance : TopologicalGroup (Profinite.limitCone (F ⋙ (forget₂ ProfiniteGrp Profinite))).pt
+ instance {M N : ProfiniteGrp.{u}} : CoeFun (M ⟶ N) (fun _ ↦ M → N)
+ inv_hom_apply
+ ofHom_apply
+ ofHom_comp
+ ofHom_hom
+ ofHom_id
- coe_of
- instance (G H : ProfiniteGrp) : ContinuousMapClass (G ⟶ H) G H
- instance (G H : ProfiniteGrp) : FunLike (G ⟶ H) G H
- instance (G H : ProfiniteGrp) : MonoidHomClass (G ⟶ H) G H
- instance : Group (Profinite.limitCone (F ⋙ profiniteGrpToProfinite.{max v u})).pt
- instance : Limits.PreservesLimits profiniteGrpToProfinite.{u}
- instance : TopologicalGroup (Profinite.limitCone (F ⋙ profiniteGrpToProfinite.{max v u})).pt
- instance : profiniteGrpToProfinite.Faithful := {
- of
- profiniteGrpToProfinite

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

chrisflav

Modulo the comment above and the merge conflict, this looks good, thanks!

and fix to_additive attribute

Thmoas-Guan · 2025-01-30T14:32:02Z

Do anyone know why lint failed here? Sorry that I have no idea about it.

chrisflav · 2025-01-30T14:35:58Z

Do anyone know why lint failed here? Sorry that I have no idea about it.

I think github is having issues right now, I don't think there is anything wrong with your PR.

chrisflav · 2025-01-30T14:36:29Z

Do anyone know why lint failed here? Sorry that I have no idea about it.

I think github is having issues right now, I don't think there is anything wrong with your PR.

chrisflav · 2025-01-30T14:37:28Z

Do anyone know why lint failed here? Sorry that I have no idea about it.

I think github is having issues right now, I don't think there is anything wrong with your PR.

chrisflav · 2025-01-30T23:25:04Z

Thanks!

maintainer merge

github-actions · 2025-01-30T23:25:23Z

🚀 Pull request has been placed on the maintainer queue by chrisflav.

kim-em · 2025-01-30T23:34:32Z

@Vierkantor, could you do the final review/merge?

Vierkantor

Looks good with some minor fixes, thanks! I think it should be easy enough to turn this into a new-style ConcreteCategory afterwards.

bors d+

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Vierkantor · 2025-01-31T09:26:30Z

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

+  forget₂.map f := Grp.ofHom f.hom.toMonoidHom

 /-- A closed subgroup of a profinite group is profinite. -/
 def ofClosedSubgroup {G : ProfiniteGrp} (H : ClosedSubgroup G)  : ProfiniteGrp :=


All of the declarations starting here are missing @[to_additive]. Or is there a reason for that?

No, it is only because previously to_additive some how failed and many things are missing API for the add version, I should add it now.

however is this a bug for to_additive ?

it somehow didn't transport the Group instance.

Hmm, that's weird. And if I make the instance manually and add @[to_additive existing] then @[to_additive] on the TopologicalGroup doesn't work either... Don't know how to fix that, and it feels like we're getting off the purpose of this PR. So if we can't fix it now it's fine to leave this as a TODO.

Almost everything broke after limitConePtAux, need to fix using attribute @[to_additive] which I think isn't a good idea, I'll leave a TODO then.

mathlib-bors · 2025-01-31T09:28:29Z

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

Thmoas-Guan · 2025-01-31T11:15:05Z

Is this OK for now?

Vierkantor

Looks good, thanks!

bors r+

…ld structures (#20740) Refactor morphisms in ProfiniteGrp into one-field structure.

mathlib-bors · 2025-01-31T12:11:26Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

…ld structures (#20740) Refactor morphisms in ProfiniteGrp into one-field structure.

Thmoas-Guan added 3 commits January 12, 2025 20:44

refactor morphism in ProfiniteGrp

61ae0e7

refactor category of ProfiniteGrp

10808d2

update Iso construction

39ec1ea

still need API from ContinuousMulEquiv

github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jan 14, 2025

Thmoas-Guan added the WIP Work in progress label Jan 14, 2025

Thmoas-Guan added 3 commits January 14, 2025 22:30

delete unused import

4c64d91

Merge branch 'master' into refactor-morphisms-in-profiniteGrp

90e0875

remove unrelated instance

35bf485

Thmoas-Guan mentioned this pull request Jan 15, 2025

[Merged by Bors] - feat(Topology/Group): Forgetful functor of ProfiniteGrp reflects isomorphism #20764

Closed

2 tasks

Vierkantor reviewed Jan 15, 2025

View reviewed changes

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean Outdated Show resolved Hide resolved

fix docstring

4c747e3

add test file

7438c40

and add missing API of ContinuousMonoidHom

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 16, 2025

Merge branch 'master' into refactor-morphisms-in-profiniteGrp

3e6c7bb

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 17, 2025

fix with new definition

49a463b

Thmoas-Guan removed the WIP Work in progress label Jan 17, 2025

remove resolved TODO

13f49d5

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 17, 2025

Merge branch 'master' into refactor-morphisms-in-profiniteGrp

9d5b18a

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 19, 2025

chrisflav approved these changes Jan 30, 2025

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

Merge branch 'master' into refactor-morphisms-in-profiniteGrp

36cde5d

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 30, 2025

fix with new definition

f88cb0e

and fix to_additive attribute

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 30, 2025

chrisflav changed the title ~~feat(Topology/Group): Refactor morphisms in ProfiniteGrp~~ refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures Jan 30, 2025

chrisflav removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

Vierkantor approved these changes Jan 31, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 31, 2025

add to_additive attribute correctly

022323a

Vierkantor approved these changes Jan 31, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jan 31, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2025

refactor(Topology/Group): turn morphisms in ProfiniteGrp into one fie…

5c261c9

…ld structures (#20740) Refactor morphisms in ProfiniteGrp into one-field structure.

mathlib-bors bot changed the title ~~refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures~~ [Merged by Bors] - refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the refactor-morphisms-in-profiniteGrp branch January 31, 2025 12:11

jt496 pushed a commit that referenced this pull request Feb 3, 2025

refactor(Topology/Group): turn morphisms in ProfiniteGrp into one fie…

b7c1497

…ld structures (#20740) Refactor morphisms in ProfiniteGrp into one-field structure.

Conversation

Thmoas-Guan commented Jan 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chrisflav commented Jan 15, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Vierkantor commented Jan 16, 2025

Uh oh!

Thmoas-Guan commented Jan 16, 2025

Uh oh!

Vierkantor commented Jan 16, 2025

Uh oh!

Thmoas-Guan commented Jan 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 16, 2025

Uh oh!

chrisflav commented Jan 16, 2025

Uh oh!

github-actions bot commented Jan 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 022323a991

Import changes for modified files

Declarations diff

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

Thmoas-Guan commented Jan 30, 2025

Uh oh!

chrisflav commented Jan 30, 2025

Uh oh!

chrisflav commented Jan 30, 2025

Uh oh!

chrisflav commented Jan 30, 2025

Uh oh!

chrisflav commented Jan 30, 2025

Uh oh!

github-actions bot commented Jan 30, 2025

Uh oh!

kim-em commented Jan 30, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vierkantor Jan 31, 2025

Choose a reason for hiding this comment

Uh oh!

Thmoas-Guan Jan 31, 2025

Choose a reason for hiding this comment

Uh oh!

Thmoas-Guan Jan 31, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Jan 31, 2025

Choose a reason for hiding this comment

Uh oh!

Thmoas-Guan Jan 31, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Thmoas-Guan commented Jan 31, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Thmoas-Guan commented Jan 14, 2025 •

edited

Loading

github-actions bot commented Jan 14, 2025 •

edited

Loading

Thmoas-Guan commented Jan 16, 2025 •

edited

Loading

github-actions bot commented Jan 17, 2025 •

edited

Loading