feat(Topology/Group): Open normal subgroup in clopen nhds

[Thmoas-Guan]

Proving that there is always an open normal subgroup in a clopen nhd of compact topological group

Co-authored-by: NailinGuan [email protected] Yi Song [email protected] Xuchun Li [email protected]

---

• [x] depends on: #16980
• [x] depends on: #16977

[github-actions[bot]]

PR summary 9e4c997415

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.ClopenNhdofOne	1053

---

Declarations diff

+ OpenNormalSubgroupSubClopenNhdsOfOne + OpenSubgroupSubClopenNhdsOfOne + TopologicalAddGroup.addNegClosureNhd + TopologicalGroup.mulInvClosureNhd + exist_mul_closure_nhd + exists_mulInvClosureNhd + iUnion_pow + openNormalSubgroupSubClopenNhdsOfOne_nonempty + openNormalSubgroupSubClopenNhdsOfOne_spec + openSubgroupSubClopenNhdsOfOne_nonempty + openSubgroupSubClopenNhdsOfOne_spec

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#16980~~
• ~~leanprover-community/mathlib4#16977~~ By Dependent Issues (🤖). Happy coding!

[kim-em]

Could you please move this new material into a new file, rather than increasing the imports of the existing file? (This problem is essentially what the large-imports label is worrying about.)

[Thmoas-Guan]

The import problem is fixed for now in this PR, but I still have a problem here : I have two theorems using the import not currently in OpenSubgroup.lean, it would be used in PR #16992 in Topology.Algebra.Category.ProfiniteGrp.Limits, is there any suggestions about where to put the two theorems? Thank you.

[kim-em]

I didn't intend to tell you to delete these theorems from the PR: just move them into a newly created file.

[Thmoas-Guan]

Theorem needing more import moved to new file.

[Thmoas-Guan]

Additive version of the theory of open subgroup in clopen neighborhood is added. I think most lemmas about this would only be used only here (I think we can always use the strongest result) so want to be marked private, but in this case @[to_additive] failed, should I leave it without private or mark them as private? If the first case, should the constructions about only groups be moved to somewhere else? If the second case, how should I resolve the @[to_additive] problem? Thank you.

[mbkybky]

Additive version of the theory of open subgroup in clopen neighborhood is added. I think most lemmas about this would only be used only here (I think we can always use the strongest result) so want to be marked private, but in this case @[to_additive] failed, should I leave it without private or mark them as private? If the first case, should the constructions about only groups be moved to somewhere else? If the second case, how should I resolve the @[to_additive] problem? Thank you.

Maybe this a bug of @[to_additive]. See Zulip.

You can manually specify the name of the theorem generated by @[to_additive]. For example,

@[to_additive OpenAddSubgroup.nhbds_side_sub]
private lemma OpenSubgroup.nhbds_side_sub ...

[PatrickMassot]

See review at https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2316981.20Open.20normal.20subgroup.20in.20clopen.20nhds/near/479367242

[Thmoas-Guan]

This PR is deprecated, the same final result woud be moved to #18377 instead with better proof.