feat(RingTheory/Extension): naive cotangent complex commutes with flat base change by chrisflav · Pull Request #35593 · leanprover-community/mathlib4

chrisflav · 2026-02-21T01:10:53Z

From Pi1.

depends on: [Merged by Bors] - feat(RingTheory): I / I ^ 2 commutes with flat base change #35544
depends on: [Merged by Bors] - feat(RingTheory/IsTensorProduct): heterogeneous associativity #35557
depends on: [Merged by Bors] - feat(RingTheory): Extension.CotangentSpace commutes with base change #35594

github-actions · 2026-02-21T01:12:07Z

PR summary 11476c36a7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Extension.Cotangent.BaseChange	1606	1621	+15 (+0.93%)
Mathlib.RingTheory.Extension.Generators	1568	1570	+2 (+0.13%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Extension.Generators`	2
`Mathlib.RingTheory.Extension.Cotangent.BaseChange`	15

Declarations diff

+ Hom.ofAlgHom
+ Hom.toAlgHom_ofAlgHom
+ baseChangeFromBaseChange
+ baseChangeFromBaseChange_apply
+ baseChangeToBaseChange
+ baseChangeToBaseChange_apply
+ cotangentEquivCotangentKer
+ equivOfEq
+ equivOfEq_symm
+ equivOfEq_toCotangent
+ ker_baseChange
+ lift
+ lift_comp_toCotangent
+ lift_surjective_iff
+ lift_toCotangent
+ tensorCotangentOfFlat
+ tensorCotangentOfFlat_tmul
+ tensorH1CotangentOfFlat_tmul
+ tensorToH1Cotangent
+ tensorToH1Cotangent_bijective_of_flat
+ tensorToH1Cotangent_tmul
++ tensorH1CotangentOfFlat
- Cotangent.lift
- Cotangent.lift_comp_toCotangent
- Cotangent.lift_surjective_iff
- Cotangent.lift_toCotangent

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.

Increase in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
6900	3	backward.isDefEq.respectTransparency

Current commit ac8114c20f
Reference commit 11476c36a7

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

mathlib-merge-conflicts · 2026-03-03T22:36:35Z

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

mathlib-dependent-issues · 2026-03-17T16:09:53Z

This PR/issue depends on:

~~[Merged by Bors] - feat(RingTheory): I / I ^ 2 commutes with flat base change #35544~~
~~[Merged by Bors] - feat(RingTheory/IsTensorProduct): heterogeneous associativity #35557~~
~~[Merged by Bors] - feat(RingTheory): Extension.CotangentSpace commutes with base change #35594~~
By Dependent Issues (🤖). Happy coding!

mariainesdff · 2026-03-31T16:20:42Z

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

+    0 0
+    (h1Cotangentι.restrictScalars R)
+    ((P.baseChange (T := T)).cotangentComplex.restrictScalars R)
+    0 0


Suggested change

0 0

-- The row ...

0 0

It is not another row, but the vertical maps. I have added a comment, please let me know if it is not clear enough.

Mathlib/RingTheory/Ideal/Cotangent.lean

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

…nge.2

…4 into cotangent-basechange.2

chrisflav · 2026-04-01T14:33:37Z

Thanks for the review @mariainesdff!

robin-carlier

Only a minor question, I’m happy with the rest

robin-carlier · 2026-04-03T13:22:31Z

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

 end Extension

+/-- Flat base change commutes with `H1Cotangent`. -/
+noncomputable def tensorH1CotangentOfFlat (T : Type*) [CommRing T] [Algebra R T] [Module.Flat R T] :


Can we hope for somewhat reasonable lemmas characterizing this def?

robin-carlier · 2026-04-03T13:28:03Z

Mathlib/RingTheory/Extension/Generators.lean

+    simp [RingHom.algebraMap_toAlgebra]
+
+@[simp]
+lemma baseChangeFromBaseChange_apply (x) :


Suggested change

lemma baseChangeFromBaseChange_apply (x) :

lemma baseChangeFromBaseChange_apply (x : P.toExtension.baseChange.Ring) :

robin-carlier · 2026-04-03T13:28:38Z

Mathlib/RingTheory/Extension/Generators.lean

+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma baseChangeToBaseChange_apply (x) :


Suggested change

lemma baseChangeToBaseChange_apply (x) :

lemma baseChangeToBaseChange_apply (x : (baseChange T P).toExtension.Ring) :

chrisflav added 10 commits February 19, 2026 04:51

wip

4e2290a

wip

124175c

wip

f91595c

cotangent base change

6067432

wip

d35e813

istensorprod assoc

8818b4d

make private and add variant

073e52f

wip

acb2aa0

Merge branch 'istensorprod-assoc' into cotangent-basechange.2

952f70e

wip

a42686f

chrisflav added the t-ring-theory Ring theory label Feb 21, 2026

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 21, 2026

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 3, 2026

mathlib-merge-conflicts 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 Mar 3, 2026

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 4, 2026

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 17, 2026

Merge branch 'master' into cotangent-basechange.2

5d54ae8

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 Mar 17, 2026

chrisflav added 4 commits March 17, 2026 21:05

cleanup

e882cc7

add lemma

d72e1dd

add OfFlat suffix to fix name clash

904fcf0

fix lint

aa4783e

mathlib-triage bot assigned mariainesdff Mar 18, 2026

mariainesdff reviewed Mar 31, 2026

View reviewed changes

Mathlib/RingTheory/Ideal/Cotangent.lean Outdated Show resolved Hide resolved

mariainesdff reviewed Mar 31, 2026

View reviewed changes

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean Outdated Show resolved Hide resolved

mariainesdff reviewed Mar 31, 2026

View reviewed changes

Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean Outdated Show resolved Hide resolved

mariainesdff added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026

chrisflav and others added 6 commits April 1, 2026 16:04

Update Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

97c9f53

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Update Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

37eaecb

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Merge remote-tracking branch 'upstream/master' into cotangent-basecha…

7aef064

…nge.2

[pre-commit.ci lite] apply automatic fixes

093cafd

Cotangent namespace, one more comment

31bdac1

Merge branch 'cotangent-basechange.2' of github.com:chrisflav/mathlib…

ac8114c

…4 into cotangent-basechange.2

mathlib-triage bot assigned riccardobrasca Apr 2, 2026

robin-carlier reviewed Apr 3, 2026

View reviewed changes

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(RingTheory/Extension): naive cotangent complex commutes with flat base change#35593

feat(RingTheory/Extension): naive cotangent complex commutes with flat base change#35593
chrisflav wants to merge 21 commits intoleanprover-community:masterfrom
chrisflav:cotangent-basechange.2

chrisflav commented Feb 21, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Feb 21, 2026 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts bot commented Mar 3, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 17, 2026

Uh oh!

mariainesdff Mar 31, 2026

Uh oh!

chrisflav Apr 1, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisflav commented Apr 1, 2026

Uh oh!

robin-carlier left a comment

Uh oh!

robin-carlier Apr 3, 2026

Uh oh!

robin-carlier Apr 3, 2026

Uh oh!

robin-carlier Apr 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

	lemma baseChangeFromBaseChange_apply (x) :
	lemma baseChangeFromBaseChange_apply (x : P.toExtension.baseChange.Ring) :

	lemma baseChangeToBaseChange_apply (x) :
	lemma baseChangeToBaseChange_apply (x : (baseChange T P).toExtension.Ring) :

Conversation

chrisflav commented Feb 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 11476c36a7

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts bot commented Mar 3, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 17, 2026

Uh oh!

mariainesdff Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

chrisflav Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisflav commented Apr 1, 2026

Uh oh!

robin-carlier left a comment

Choose a reason for hiding this comment

Uh oh!

robin-carlier Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

robin-carlier Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

robin-carlier Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

chrisflav commented Feb 21, 2026 •

edited

Loading

github-actions bot commented Feb 21, 2026 •

edited

Loading