Skip to content

[Merged by Bors] - feat(GroupTheory/QuotientGroup): group correspondence theorem#20007

Closed
jhanschoo wants to merge 5 commits intomasterfrom
comap_mk_orderiso
Closed

[Merged by Bors] - feat(GroupTheory/QuotientGroup): group correspondence theorem#20007
jhanschoo wants to merge 5 commits intomasterfrom
comap_mk_orderiso

Conversation

@jhanschoo
Copy link
Copy Markdown
Collaborator

@jhanschoo jhanschoo commented Dec 16, 2024 •
edited
Loading

add the group correspondence theorem (a.k.a. lattice theorem, fourth isomorphism theorem).

edit: forgot to give credit; most of this PR is a translation from Submodule.comapMkQRelIso

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 16, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 16, 2024 •
edited
Loading

PR summary 7c928c7a6f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ comapMk'OrderIso
+ comap_map_mk'
+ le_comap_mk'
+ range_mk'

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).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Dec 16, 2024
@Vierkantor Vierkantor changed the title feat(GroupQuotient): group correspondence theorem feat(GroupTheory/QuotientGroup): group correspondence theorem Dec 19, 2024
Vierkantor
Vierkantor reviewed Dec 19, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Thanks! I have some comments but they are short and hopefully they are easy to address.

@Vierkantor Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 19, 2024
@jhanschoo
Copy link
Copy Markdown
Collaborator Author

jhanschoo commented Dec 20, 2024

Thanks! I'll update the PR with the suggestions in the weekend

@jhanschoo
Copy link
Copy Markdown
Collaborator Author

jhanschoo commented Dec 20, 2024

@Vierkantor it would be a separate PR with extensive refactoring of course, but what's your opinion on renaming mk' to mkQ to align with Submodule.mkQ? And renaming bare mk to say mkC standing for cosets.

@jhanschoo jhanschoo force-pushed the comap_mk_orderiso branch 2 times, most recently from 04db1ea to f83f306 Compare December 21, 2024 09:33
@jhanschoo jhanschoo removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 21, 2024
@jhanschoo
Copy link
Copy Markdown
Collaborator Author

jhanschoo commented Jan 3, 2025

bump

@jhanschoo jhanschoo requested a review from j-loreaux January 5, 2025 05:01
tb65536
tb65536 reviewed Jan 5, 2025
View reviewed changes
@jhanschoo @tb65536
Update Mathlib/GroupTheory/QuotientGroup/Basic.lean
80d98a9 
Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
@jhanschoo jhanschoo requested a review from tb65536 January 6, 2025 03:42
tb65536
tb65536 reviewed Jan 6, 2025
View reviewed changes
Vierkantor
Vierkantor approved these changes Jan 6, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Hi, I'm finally back from holidays. This looks good to me, with these small suggestions by @tb65536 and myself.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 6, 2025

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

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 6, 2025
jhanschoo and others added 2 commits January 7, 2025 11:46
@jhanschoo @Vierkantor
Apply suggestions from code review
a46a437 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@jhanschoo @tb65536
Apply suggestions from code review
7c928c7 
Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
@jhanschoo
Copy link
Copy Markdown
Collaborator Author

jhanschoo commented Jan 7, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@jhanschoo
feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
d7f04b9 
add the group correspondence theorem (a.k.a. lattice theorem, fourth isomorphism theorem).
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(GroupTheory/QuotientGroup): group correspondence theorem [Merged by Bors] - feat(GroupTheory/QuotientGroup): group correspondence theorem Jan 7, 2025
@mathlib-bors mathlib-bors bot closed this Jan 7, 2025
@mathlib-bors mathlib-bors bot deleted the comap_mk_orderiso branch January 7, 2025 04:59
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into emultiplicity-of-nat
53d4c08 
* origin/master: (642 commits)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  feat(Analysis/Analytic): lemmas about `smul` for power series (#19816)
  chore: don't import algebra in `Data.Multiset.Basic` (#19775)
  ...
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
0ae6406 
* origin/master: (80 commits)
  chore(CategoryTheory): remove data produced by tactic block (#20565)
  feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tb65536 tb65536 tb65536 left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

@grunweg grunweg Awaiting requested review from grunweg

@Ruben-VandeVelde Ruben-VandeVelde Awaiting requested review from Ruben-VandeVelde

@j-loreaux j-loreaux Awaiting requested review from j-loreaux

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@jhanschoo @Vierkantor @grunweg @tb65536 @Ruben-VandeVelde