feat(RingTheory/Smooth): some lemmas about formally smooth by Thmoas-Guan · Pull Request #35675 · leanprover-community/mathlib4

Thmoas-Guan · 2026-02-23T07:15:53Z

This PR mainly formalized the result [Stacks 031L]
This is a preliminary of Cohen Structure Theorem.

github-actions · 2026-02-23T07:17:04Z

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.Smooth.Quotient` (new file)	2178

Declarations diff

+ Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat
+ Ideal.subtype_rTensor_range
+ LinearMap.ker_inf_smul_top_eq_smul_of_flat
+ RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zero
+ comap_ker_eq_sup_of_ker_eq_map
+ eq_map_of_comap_eq_ker_sup
+ exists_of_comap_eq_ker_sup
+ ker_mapCotangent_ker_surjective
+ mapCotangent_surjective_of_comap_eq
+ mul_le_ker_of_range_le_mul_of_sq_zero

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

Mathlib/RingTheory/RingHom/Smooth.lean

Mathlib/RingTheory/Smooth/Quotient.lean

Thmoas-Guan · 2026-03-04T16:39:15Z

There are some lemma that I didn't find an appropriate place, do anyone familiar with the field give some suggestions?

and get rid of base change related stuffs

Mathlib/RingTheory/RingHom/Smooth.lean

Mathlib/RingTheory/TensorProduct/Quotient.lean

riccardobrasca · 2026-03-30T13:40:56Z

Mathlib/RingTheory/TensorProduct/Quotient.lean


 end Algebra.TensorProduct
+
+lemma Ideal.subtype_rTensor_range {R : Type*} [CommRing R] (M : Type*) [AddCommGroup M] [Module R M]


Can you use some variables already in scope?

riccardobrasca · 2026-03-30T13:42:39Z

Mathlib/RingTheory/Smooth/Quotient.lean

+
+variable {R : Type u} [CommRing R]
+
+lemma LinearMap.ker_inf_smul_top_eq_smul_of_flat {M N : Type*} [AddCommGroup M] [AddCommGroup N]


Can this go to another file? It is unrelated to smoothness.

Also, maybe add a short docstring.

@riccardobrasca do you have idea about where to move? find home suggested Mathlib.RingTheory.LocalRing.Module but I think the content is unrelated?

Also can you help have a look for good places or make private of all those lemmas separated out? Thanks.

Something about flat modules maybe?

Mathlib/RingTheory/Smooth/Quotient.lean

riccardobrasca · 2026-03-30T13:45:55Z

Mathlib/RingTheory/Smooth/Quotient.lean

+/-- For flat ring homomorphism `f : R →+* S`, `I` an ideal of `R` which is square zero,
+if `R ⧸ I →+* S ⧸ IS` is formally smooth, so do `f`. -/
+@[stacks 031L]
+lemma Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat {S : Type v} [CommRing S]


This proof is very long. Can you try to split off as many sublemmas as possible? Don't worry if they will never be used, you can mark them as private (or even better use private/public sections).

I'll try, I know the general convention for maintainability.

I know it's not always easy, so don't get crazy about it, but usually it is possible to split at least a couple of results.

I separated many annoying stuffs I remembered throughout the proof, reducing the main proof for about 50 lines but total length gaining 40.

The rest of the proof is much harder to separate because they really involve the resolution constructed in this specific case.

Mathlib/RingTheory/Smooth/Quotient.lean

Thmoas-Guan added 3 commits February 23, 2026 10:51

Add formally smooth lemma

a9f83c6

Update Mathlib.lean

3230a58

Update Quotient.lean

b6a6839

github-actions bot added the t-ring-theory Ring theory label Feb 23, 2026

fix namespace

d32b013

Thmoas-Guan mentioned this pull request Feb 27, 2026

feat(RingTheory): existence of coefficient ring #35852

Draft

3 tasks

mathlib-triage bot assigned jcommelin Mar 1, 2026

jcommelin reviewed Mar 3, 2026

View reviewed changes

Mathlib/RingTheory/RingHom/Smooth.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/RingHom/Smooth.lean Outdated Show resolved Hide resolved

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

replace by formally smooth comp

1dcb7a3

Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 3, 2026

jcommelin reviewed Mar 4, 2026

View reviewed changes

Mathlib/RingTheory/Smooth/Quotient.lean Outdated Show resolved Hide resolved

Thmoas-Guan added 3 commits March 4, 2026 19:45

Merge branch 'master' into FormallySmooth-Lemma

72e2943

total refactor

42834a4

move lemma

00c270f

Thmoas-Guan added 5 commits March 5, 2026 13:32

add base change lemma

1208f34

restate theorem

9f5ee2b

and get rid of base change related stuffs

remove unrelated stuffs

bfa7aa5

add ring hom variant

9e743d2

Merge branch 'master' into FormallySmooth-Lemma

6f344c1

jcommelin reviewed Mar 11, 2026

View reviewed changes

Mathlib/RingTheory/RingHom/Smooth.lean Show resolved Hide resolved

jcommelin reviewed Mar 11, 2026

View reviewed changes

Mathlib/RingTheory/TensorProduct/Quotient.lean Outdated Show resolved Hide resolved

Thmoas-Guan added 3 commits March 11, 2026 18:23

fix layout

c47a6aa

remove unrelated change

03a6d2e

Merge branch 'master' into FormallySmooth-Lemma

d133dfb

mathlib-triage bot assigned erdOne and unassigned jcommelin Mar 18, 2026

Merge branch 'master' into FormallySmooth-Lemma

0ea4c08

mathlib-triage bot assigned riccardobrasca and mattrobball Mar 27, 2026

riccardobrasca changed the title ~~feat(RingTheory/Smooth): some lemma about formally smooth~~ feat(RingTheory/Smooth): some lemmas about formally smooth Mar 30, 2026

riccardobrasca reviewed Mar 30, 2026

View reviewed changes

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

Thmoas-Guan added 6 commits March 31, 2026 00:04

Merge branch 'master' into FormallySmooth-Lemma

451ff70

fix doc

7af5884

fix variable

315b071

Merge branch 'master' into FormallySmooth-Lemma

ab60ac7

splits lots of lemmas

dfaa295

reduce lemma condition

7ca60f5

Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026

Merge branch 'master' into FormallySmooth-Lemma

d3a86a6


		end Algebra.TensorProduct

		lemma Ideal.subtype_rTensor_range {R : Type} [CommRing R] (M : Type) [AddCommGroup M] [Module R M]


		variable {R : Type u} [CommRing R]

		lemma LinearMap.ker_inf_smul_top_eq_smul_of_flat {M N : Type*} [AddCommGroup M] [AddCommGroup N]

Conversation

Thmoas-Guan commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 6ef8cc2731

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Thmoas-Guan commented Mar 4, 2026

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Thmoas-Guan commented Feb 23, 2026 •

edited

Loading

github-actions bot commented Feb 23, 2026 •

edited

Loading