feat(RingTheory): etale lifting property of henselian local rings by erdOne · Pull Request #41086 · leanprover-community/mathlib4

erdOne · 2026-06-26T17:12:40Z

github-actions · 2026-06-26T17:14:05Z

PR summary a010cae47a

Import changes exceeding 2%

%	File
+79.64%	`Mathlib.RingTheory.Henselian`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Henselian	1385	2488	+1103 (+79.64%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Idempotents`	1
`Mathlib.RingTheory.Henselian`	1103
`Mathlib.RingTheory.IdempotentInstances` (new file)	1456
`Mathlib.RingTheory.LocalRing.RingHom.IsIntegral` (new file)	1636

Declarations diff (regex)

+ HenselianLocalRing.algEquivEquiv
+ HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale
+ HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing
+ HenselianLocalRing.exists_residueFieldMap_eq_of_etale
+ HenselianLocalRing.ofId_comp_bijective
+ HenselianLocalRing.of_finite
+ HenselianLocalRing.of_finite_aux
+ IsIdempotentElem.algebraMap_corner_apply
+ IsIdempotentElem.algebraMap_corner_surjective
+ IsIdempotentElem.ker_algebraMap_corner
+ IsLocalRing.eq_of_residueFieldMap_eq
+ IsLocalRing.ofId_comp_injective
+ finrank_eq_one_iff_algebraMap_bijective
+ instance : IsLocalHom e.toAlgHom := ⟨by simp⟩
+ instance : IsLocalHom e.toAlgHom.toRingHom := ⟨by simp⟩
+ instance : IsLocalHom e.toRingEquiv.toRingHom := ⟨by simp⟩
+ instance [IsLocalRing R] [Algebra.IsIntegral R S] [Nontrivial S] :
+ instance [Module.Finite R A] : Module.Finite R he.Corner
+ instance [Module.Flat R A] : Module.Flat R he.Corner
+ instance [Module.Projective R A] : Module.Projective R he.Corner
+ instance {R R' S : Type*} [CommSemiring R] [CommSemiring R'] [Semiring S] [Algebra R S]
+ instance {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
- instance : IsLocalHom e.toAlgHom := by

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit a010cae).

+20 new declarations
−0 removed declarations

+AlgEquiv.instIsLocalHomRingHomToAlgHom
+AlgEquiv.instIsLocalHomRingHomToRingHomToRingEquiv
+HenselianLocalRing.algEquivEquiv
+HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale
+HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing
+HenselianLocalRing.exists_residueFieldMap_eq_of_etale
+HenselianLocalRing.ofId_comp_bijective
+HenselianLocalRing.of_finite
+IsIdempotentElem.algebraMap_corner_apply
+IsIdempotentElem.algebraMap_corner_surjective
+IsIdempotentElem.ker_algebraMap_corner
+IsLocalRing.eq_of_residueFieldMap_eq
+IsLocalRing.ofId_comp_injective
+Module.finrank_eq_one_iff_algebraMap_bijective
+instAlgebraCorner
+instFiniteCorner
+instFlatCorner
+instIsLocalHomRingHomAlgebraMapOfIsLocalRingOfIsIntegralOfNontrivial
+instIsScalarTowerCorner
+instProjectiveCorner

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

Current number	Change	Type (strong)
5690	1	backward.isDefEq.respectTransparency

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

Current number	Change	Type (weak)
4975	2	exposed public sections

Current commit a010cae47a
Reference commit 571b8a8e54

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

Co-authored-by: Christian Merten <christian@merten.dev>

into erd1/henselianStuff

Co-authored-by: Christian Merten <christian@merten.dev>

chrisflav

Thanks!
maintainer merge

github-actions · 2026-06-27T19:43:38Z

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

faenuccio

I've left some comments, but in particular I wonder if we don't need a Henselian folder to distinguish basic stuff from étale one.

Also, can you update the PR description? Thanks.

faenuccio · 2026-06-30T16:23:41Z

+public import Mathlib.RingTheory.Flat.Stability
+public import Mathlib.RingTheory.Idempotents
+
+/-! # Instances on corners -/


Can you improve this docstring?

faenuccio · 2026-06-30T16:26:18Z

+    Function.Surjective (algebraMap R he.Corner) :=
+  fun x ↦ ⟨x.1, Subtype.ext ((Subsemigroup.mem_corner_iff he).mp x.2).2⟩
+
+lemma IsIdempotentElem.ker_algebraMap_corner [CommRing R] {e : R} (he : IsIdempotentElem e) :


Suggested change

lemma IsIdempotentElem.ker_algebraMap_corner [CommRing R] {e : R} (he : IsIdempotentElem e) :

lemma IsIdempotentElem.ker_algebraMap_corner_eq_span [CommRing R] {e : R} (he : IsIdempotentElem e) :

faenuccio · 2026-06-30T16:30:23Z

+
+variable {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
+
+attribute [local instance] Localization.AtPrime.algebraOfLiesOver in


Can you explain why this is the natural place for this results? The statement has nothing to do with henselianity, AFAICT.

faenuccio · 2026-06-30T16:32:56Z

+attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
+/-- If `R` is a local ring with residue field `k`, then for any étale `R`-algebra `A`,
+every `A →ₐ[R] k` lifts to at most one an `A →ₐ[R] R`. -/
+lemma IsLocalRing.ofId_comp_injective [Algebra.Etale R A] [IsLocalRing R] :


Don't you think that this should live in the Algebra.Etale namespace?

faenuccio · 2026-06-30T16:38:16Z

+    simpa using 𝓟.hasMap.isUnit_derivative_f.map f₁
+
+attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
+/-- If `R` is a Henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,


Can you add this important result to the module docstring?

faenuccio · 2026-06-30T16:50:54Z

+    · simp
+    · rw [ha]; simp [← hroot]
+
+/-- Let `R` be an henselian local ring, `A, B` be local `R`-algebras.


Suggested change

/-- Let `R` be an henselian local ring, `A, B` be local `R`-algebras.

/-- Let `R` be a henselian local ring, `A, B` be local `R`-algebras.

faenuccio · 2026-06-30T16:51:46Z

+    · rw [ha]; simp [← hroot]
+
+/-- Let `R` be an henselian local ring, `A, B` be local `R`-algebras.
+Suppose `A` is etale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to


Suggested change

Suppose `A` is etale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to

Suppose `A` is étale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to

can you also check all the other etale and add the accent?

faenuccio · 2026-06-30T16:53:20Z

+an `R`-algebra map `A → B`.
+
+See `HenselianLocalRing.eq_of_residueFieldMap_eq` for the uniqueness of the lift. -/
+lemma HenselianLocalRing.exists_residueFieldMap_eq_of_etale [HenselianLocalRing R] [IsLocalRing A]


The name seems to suggest the existence of a residue field map, whereas it is the existence of a lift. Do you have other naming options?

faenuccio · 2026-06-30T16:55:36Z

+    have : IsLocalHom (φ.comp ψ).toRingHom := by
+      dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢; exact RingHom.isLocalHom_comp _ _
+    apply IsLocalRing.eq_of_residueFieldMap_eq
+    dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢ hφ' hψ'


I would squeeze this as well, no?

faenuccio · 2026-06-30T16:56:31Z

+Then `Aut(A/R) ≃ Gal(k(A)/k(R))`.
+
+Paired with `galRestrict`, this shows that `Gal(Frac A / Frac R) ≃* Gal(k(A)/k(R))`. -/
+def HenselianLocalRing.algEquivEquiv [HenselianLocalRing R]


Why not algEquivMulEquiv?

feat(RingTheory): etale lifting property of henselian local rings

316d7d6

github-actions Bot added large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory labels Jun 26, 2026

fix

a3b4e38

chrisflav reviewed Jun 27, 2026

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 27, 2026

chrisflav reviewed Jun 27, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Idempotents.lean Outdated

chrisflav reviewed Jun 27, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Idempotents.lean Outdated

chrisflav reviewed Jun 27, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Idempotents.lean

erdOne and others added 4 commits June 27, 2026 12:00

Apply suggestions from code review

3b7d379

Co-authored-by: Christian Merten <christian@merten.dev>

address comments

0598017

Merge branch 'erd1/henselianStuff' of https://github.com/erdOne/mathlib4

5abc0fe

into erd1/henselianStuff

fix

8ae282f

erdOne added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 27, 2026

erdOne added 3 commits June 27, 2026 15:30

oops

b50adef

oops

f95fe6a

fix

d3b6170

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 27, 2026

chrisflav reviewed Jun 27, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Henselian.lean Outdated

Apply suggestion from @chrisflav

a010cae

Co-authored-by: Christian Merten <christian@merten.dev>

chrisflav approved these changes Jun 27, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 27, 2026

faenuccio self-assigned this Jun 30, 2026

faenuccio added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 30, 2026

faenuccio reviewed Jun 30, 2026

View reviewed changes

	lemma IsIdempotentElem.ker_algebraMap_corner [CommRing R] {e : R} (he : IsIdempotentElem e) :
	lemma IsIdempotentElem.ker_algebraMap_corner_eq_span [CommRing R] {e : R} (he : IsIdempotentElem e) :


		variable {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]

		attribute [local instance] Localization.AtPrime.algebraOfLiesOver in

	/-- Let `R` be an henselian local ring, `A, B` be local `R`-algebras.
	/-- Let `R` be a henselian local ring, `A, B` be local `R`-algebras.

	Suppose `A` is etale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to
	Suppose `A` is étale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to

Uh oh!

Conversation

erdOne commented Jun 26, 2026

Uh oh!

github-actions Bot commented Jun 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a010cae47a

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Jun 27, 2026

Uh oh!

faenuccio left a comment

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!

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!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Jun 26, 2026 •

edited

Loading