Skip to content

feat(Algebra): lemma about IsBaseChange under exact sequence#31219

Open
Thmoas-Guan wants to merge 34 commits intoleanprover-community:masterfrom
Thmoas-Guan:IsBaseChange-Lemma
Open

feat(Algebra): lemma about IsBaseChange under exact sequence#31219
Thmoas-Guan wants to merge 34 commits intoleanprover-community:masterfrom
Thmoas-Guan:IsBaseChange-Lemma

Conversation

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator

@Thmoas-Guan Thmoas-Guan commented Nov 3, 2025

In this lemma, we proved cokernel preserve IsBaseChange S and kernel preserve IsBaseChange S when S is flat.

Co-authored-by: Wang Jingting [email protected]

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 3, 2025 •
edited
Loading

PR summary 6ef8cc2731

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact (new file) 1181
Mathlib.RingTheory.Flat.IsBaseChange (new file) 1401

Declarations diff

+ IsBaseChange.comp_equiv
+ IsBaseChange.of_equiv_left
+ IsBaseChange.of_equiv_right
+ IsBaseChange.of_left_exact
+ IsBaseChange.of_right_exact
+ linearEquiv_comp
+ linearEquiv_comp_compl₂
+ linearEquiv_compl₂
+ linearEquiv_compr₂

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

@Thmoas-Guan Thmoas-Guan mentioned this pull request Nov 3, 2025
Open
3 tasks
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 10, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 10, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 12, 2025
urkud
urkud reviewed Nov 16, 2025
View reviewed changes
urkud
urkud reviewed Nov 16, 2025
View reviewed changes
@j-loreaux j-loreaux removed their assignment Nov 16, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

This pull request has conflicts, please merge master and resolve them.

@kex-y kex-y removed their assignment Nov 19, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 20, 2025
@robin-carlier robin-carlier added the t-ring-theory Ring theory label Nov 21, 2025
erdOne
erdOne reviewed Nov 22, 2025
View reviewed changes
erdOne
erdOne reviewed Nov 22, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Some of these results have nothing to do with flatness right? Can you move them out?

@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 22, 2025
@Thmoas-Guan
Copy link
Copy Markdown
Collaborator Author

Thmoas-Guan commented Dec 29, 2025 •
edited
Loading

Some of these results have nothing to do with flatness right? Can you move them out?

find_home! didn't give me better suggestions (importing both five lemma and IsBaseChange is hard to find in any sense) @erdOne

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator Author

Thmoas-Guan commented Mar 20, 2026

File splited as I didn't find an appropriate place for it.

@Thmoas-Guan Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026
chrisflav
chrisflav reviewed Mar 27, 2026
View reviewed changes
@chrisflav chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026
@Thmoas-Guan Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026
@Thmoas-Guan Thmoas-Guan requested review from chrisflav and erdOne April 3, 2026 08:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

@erdOne erdOne Awaiting requested review from erdOne

@chrisflav chrisflav Awaiting requested review from chrisflav

Assignees

@mariainesdff mariainesdff

Labels

t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

9 participants

@Thmoas-Guan @mathlib4-merge-conflict-bot @urkud @erdOne @chrisflav @j-loreaux @kex-y @robin-carlier @mariainesdff