Skip to content

[Merged by Bors] - feat(RingTheory/Flat/Basic): Submodule.toBaseChange as a LinearEquiv#37115

Closed
tb65536 wants to merge 8 commits intoleanprover-community:masterfrom
tb65536:tb_tbcequiv
Closed

[Merged by Bors] - feat(RingTheory/Flat/Basic): Submodule.toBaseChange as a LinearEquiv#37115
tb65536 wants to merge 8 commits intoleanprover-community:masterfrom
tb65536:tb_tbcequiv

Conversation

@tb65536
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 commented Mar 24, 2026

If the extensions of rings is flat, then Submodule.toBaseChange becomes a LinearEquiv.

Open in Gitpod

@tb65536 tb65536 added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory labels Mar 24, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 24, 2026 •
edited
Loading

PR summary e60d89a050

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ toBaseChange.toLinearEquiv
+ toBaseChange.toLinearEquiv_symm_apply
+ toBaseChange_injective

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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 removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 24, 2026
robin-carlier
robin-carlier reviewed Mar 27, 2026
View reviewed changes
Comment thread Mathlib/RingTheory/Flat/Basic.lean Outdated
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026
@tb65536 tb65536 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 30, 2026
@robin-carlier
Copy link
Copy Markdown
Contributor

robin-carlier commented Apr 3, 2026

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 3, 2026

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 3, 2026
faenuccio
faenuccio reviewed Apr 5, 2026
View reviewed changes
Comment thread Mathlib/RingTheory/Flat/Basic.lean Outdated

/-- `Submodule.toBaseChange` as a `LinearEquiv`. -/
@[simps! apply]
noncomputable def toBaseChangeEquiv : A ⊗[R] ↥p ≃ₗ[A] baseChange A p :=
Copy link
Copy Markdown
Contributor

@faenuccio faenuccio Apr 5, 2026

Choose a reason for hiding this comment

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

Why not baseChange_toLinearEquiv?

Copy link
Copy Markdown
Contributor Author

@tb65536 tb65536 Apr 6, 2026

Choose a reason for hiding this comment

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

It's a def, so is it ok to have an underscore?

Copy link
Copy Markdown
Contributor

@faenuccio faenuccio Apr 6, 2026

Choose a reason for hiding this comment

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

No, it is not, you're right. I wanted to suggest toBaseChange.toLinearEquiv, but I was sceptical since toBaseChange is not a structure per se: perhaps in the end it is ok, though, so why not toBaseChange.toLinearEquiv?

Copy link
Copy Markdown
Contributor Author

@tb65536 tb65536 Apr 6, 2026

Choose a reason for hiding this comment

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

Sure.

Copy link
Copy Markdown
Contributor Author

@tb65536 tb65536 Apr 7, 2026

Choose a reason for hiding this comment

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

Done, although one disadvantage is that you can no longer use dot-notation in the Submodule namespace.

Copy link
Copy Markdown
Contributor

@faenuccio faenuccio Apr 8, 2026

Choose a reason for hiding this comment

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

OK, I'm happy to merge as it is unless you've got a better proposal (as long as it conserves the toLinearEquiv)

Copy link
Copy Markdown
Contributor Author

@tb65536 tb65536 Apr 8, 2026

Choose a reason for hiding this comment

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

Yeah, I can't really think of a better name with toLinearEquiv.

@faenuccio faenuccio self-assigned this Apr 5, 2026
@tb65536 tb65536 added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 6, 2026
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 7, 2026
@faenuccio
Copy link
Copy Markdown
Contributor

faenuccio commented Apr 8, 2026

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 8, 2026

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

@mathlib-triage mathlib-triage bot 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 Apr 8, 2026
@tb65536
Copy link
Copy Markdown
Contributor Author

tb65536 commented Apr 8, 2026

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Apr 8, 2026
@tb65536
feat(RingTheory/Flat/Basic): Submodule.toBaseChange as a `LinearEqu…
b1ae7e3 
…iv` (#37115)

If the extensions of rings is flat, then `Submodule.toBaseChange` becomes a `LinearEquiv`.

Co-authored-by: tb65536 <[email protected]>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 8, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/Flat/Basic): Submodule.toBaseChange as a LinearEquiv [Merged by Bors] - feat(RingTheory/Flat/Basic): Submodule.toBaseChange as a LinearEquiv Apr 8, 2026
@mathlib-bors mathlib-bors bot closed this Apr 8, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 10, 2026
@tb65536 @xroblot
feat(RingTheory/Flat/Basic): Submodule.toBaseChange as a `LinearEqu…
7cae23e 
…iv` (leanprover-community#37115)

If the extensions of rings is flat, then `Submodule.toBaseChange` becomes a `LinearEquiv`.

Co-authored-by: tb65536 <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-carlier robin-carlier robin-carlier left review comments

@faenuccio faenuccio faenuccio left review comments

Assignees

@faenuccio faenuccio

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tb65536 @robin-carlier @faenuccio