[Merged by Bors] - feat(Topology/Group/Profinite): limits in the category of profinite groups#16976
[Merged by Bors] - feat(Topology/Group/Profinite): limits in the category of profinite groups#16976Thmoas-Guan wants to merge 13 commits intomasterfrom
Conversation
PR summary d0b2840479Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
dagurtomas
left a comment
There was a problem hiding this comment.
Could you also add a PreservesLimits profiniteGrpToProfinite instance? It shouldn't be too hard using what you already have
|
To prove that the functor from profinite groups to profinite sets preserves limits, I would suggest using https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Limits/Preserves/Basic.html#CategoryTheory.Limits.preservesLimitOfPreservesLimitCone applied to |
Thank a lot, I just got some ugly things because of lacking this. |
|
Did you forget to remove |
|
Thanks! maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by dagurtomas. |
| toFun := ((Profinite.limitConeIsLimit (F ⋙ profiniteGrpToProfinite)).lift | ||
| (profiniteGrpToProfinite.mapCone cone)).toFun | ||
| map_one' := by | ||
| apply SetCoe.ext |
There was a problem hiding this comment.
I'm a bit sad to see that this is necessary (rather than just calling ext). It indicates to me that perhaps we haven't set up @[ext] lemmas sufficiently for TopCat.
Doesn't need to block this PR, I'll pass that decision back to @dagurtomas. :-)
There was a problem hiding this comment.
Let me investigate a bit
There was a problem hiding this comment.
I don't have time to dig more so I'd recommend that we just merge this. I added a TODO.
Let me just note that even adding the lemma
@[ext]
lemma limitCone_ext {J : Type v} [SmallCategory J] {F : J ⥤ ProfiniteGrp.{max v u}}
{x y : (limitCone F).pt} (h : ∀ i, x.1 i = y.1 i) : x = y := Subtype.ext (funext fun i ↦ h i)wasn't enough to get the ext tactic to work.
|
bors merge |
…roups (#16976) Define the limit in profinite groups as a profinite group. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com> Nailin Guan <3571819596@qq.com> Co-authored-by: dagurtomas <dagurtomas@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
…roups (#16976) Define the limit in profinite groups as a profinite group. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com> Nailin Guan <3571819596@qq.com> Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Define the limit in profinite groups as a profinite group.
Co-authored-by: Jujian Zhang jujian.zhang1998@outlook.com Nailin Guan 3571819596@qq.com