Skip to content

[Merged by Bors] - chore(GroupExtension/Defs): define Section and redefine Splitting#20802

Closed
yu-yama wants to merge 6 commits intomasterfrom
yu-yama/GroupExtension-Defs
Closed

[Merged by Bors] - chore(GroupExtension/Defs): define Section and redefine Splitting#20802
yu-yama wants to merge 6 commits intomasterfrom
yu-yama/GroupExtension-Defs

Conversation

@yu-yama
Copy link
Copy Markdown
Collaborator

@yu-yama yu-yama commented Jan 16, 2025 •
edited
Loading

This PR:

  • defines structure (Add)?GroupExtension.Section as a right inverse to rightHom
  • redefines structure (Add)?GroupExtension.Splitting using Section
  • rewrites the definition of structure (Add)?GroupExtension.Equiv with extends

As the first part of #19582, this PR contains only the changes to the Defs file.

Moves:

  • GroupExtension.Splitting.sectionHom -> GroupExtension.Splitting.toMonoidHom
  • GroupExtension.Splitting.rightHom_comp_sectionHom -> GroupExtension.Splitting.rightInverse_rightHom

Open in Gitpod

@github-actions github-actions bot added 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) labels Jan 16, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 16, 2025 •
edited
Loading

PR summary 725364c16c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coe_monoidHom_mk
+ instance : FunLike S.Section G E
+ rightHom_comp_section
+ rightHom_comp_splitting
+ rightHom_section
+ rightHom_splitting
++ Section
++ coe_mk
++-- Splitting
+-+- Equiv

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

@yu-yama yu-yama mentioned this pull request Jan 16, 2025
Open
3 tasks
@yu-yama yu-yama assigned yu-yama and erdOne and unassigned yu-yama Jan 16, 2025
erdOne
erdOne reviewed Jan 16, 2025
View reviewed changes
@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 16, 2025
yu-yama and others added 3 commits January 16, 2025 20:08
@yu-yama
docs: restore TODO comments to be resolved in other split PRs
64ecf23
@yu-yama @erdOne
style: prefer __ over with
0ddb665 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@yu-yama @erdOne
style: prefer field notation
2b5fe22 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
yu-yama
yu-yama commented Jan 16, 2025
View reviewed changes
yu-yama and others added 2 commits January 16, 2025 20:25
@yu-yama yu-yama removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 16, 2025
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jan 16, 2025

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 16, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 16, 2025
jcommelin
jcommelin reviewed Jan 17, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 17, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2025
@yu-yama
chore(GroupExtension/Defs): define Section and redefine Splitting (…
a1e497d 
…#20802)

This PR:
- defines `structure (Add)?GroupExtension.Section` as a right inverse to `rightHom`
- redefines `structure (Add)?GroupExtension.Splitting` using `Section`
- rewrites the definition of `structure (Add)?GroupExtension.Equiv` with `extends`

As the first part of #19582, this PR contains only the changes to the `Defs` file.

Moves:
- GroupExtension.Splitting.sectionHom -> GroupExtension.Splitting.toMonoidHom
- GroupExtension.Splitting.rightHom_comp_sectionHom -> GroupExtension.Splitting.rightInverse_rightHom
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 17, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(GroupExtension/Defs): define Section and redefine Splitting [Merged by Bors] - chore(GroupExtension/Defs): define Section and redefine Splitting Jan 17, 2025
@mathlib-bors mathlib-bors bot closed this Jan 17, 2025
@mathlib-bors mathlib-bors bot deleted the yu-yama/GroupExtension-Defs branch January 17, 2025 06:30
Julian added a commit that referenced this pull request Jan 20, 2025
@Julian
Merge branch 'polynomial-sequences' into bhargava-factorial
856ec0d 
* polynomial-sequences: (149 commits)
  Aha, here's how to get Lean to stop showing S.elems' in the infoview.
  Try satisfying the linter gods again.
  Probably enough initial tidying to send the PR.
  Kill more temporary names.
  Touch more natDegree.
  Does protected satisfy the docstring linter?
  Bit shorter.
  More
  Quiet linters.
  Remove redundant imports.
  Copyright header and more twiddling.
  Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out
  feat(Polynomial): polynomial sequences are bases for R[X]
  chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765)
  chore(Associated): split out `Ring` results (#20737)
  feat(AlgebraicGeometry): flat morphisms of schemes (#19790)
  feat(AlgebraicGeometry): scheme-theoretic fibre (#19427)
  chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785)
  doc: typo (#20829)
  feat(CategoryTheory): condition for an induced functor between comma categories to be final  (#20139)
  feat(1000.yaml): allow statements of theorems also (#20637)
  feat(Algebra/Homology/Embedding): homology of truncGE' (#19570)
  chore: cleanup many porting notes in Combinatorics (#20823)
  chore: eliminate porting notes about `deriving Fintype` (#20820)
  feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)
  feat: define bases of root pairings (#20667)
  feat(Tactic): basic ConcreteCategory support for elementwise (#20811)
  feat(CategoryTheory): define unbundled `ConcreteCategory` class  (#20810)
  chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809)
  feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783)
  chore(yaml_check.py): re-format (#20807)
  feat: elementary estimate for Real.log (#20766)
  feat: definition of linear topologies (#14990)
  feat(RingTheory): flatness over a semiring (#19115)
  feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550)
  feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203)
  feat(Algebra/Ring): `RingEquiv.piUnique` (#20794)
  feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801)
  chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802)
  chore: restore `def` to `adicCompletion` (#20796)
  refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643)
  feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544)
  chore(Mathlib/Computability/TuringMachine): split file (#20790)
  feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753)
  feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752)
  feat(Set/Finite): a set is finite if its image and fibers are finite (#20751)
  chore: cleanup .gitignore files (#20795)
  feat(Topology/Group/Profinite):  Profinite group is limit of finite group (#16992)
  feat(Combinatorics/SimpleGraph): vertices in cycles (#20602)
  CI: merge `bot_fix_style` actions (#20789)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@erdOne erdOne erdOne left review comments

Assignees

@erdOne erdOne

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@yu-yama @erdOne @jcommelin