[Merged by Bors] - feat(AlgebraicGeometry): Zariski's main theorem by erdOne · Pull Request #35093 · leanprover-community/mathlib4

erdOne · 2026-02-10T17:17:11Z

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…lib4 into erd1/unramifiedLocalStructure3

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

…rdOne/mathlib4 into erd1/unramifiedLocalStructure3

github-actions · 2026-02-10T17:18:23Z

PR summary 2598404fe9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite`	1
`Mathlib.AlgebraicGeometry.ZariskisMainTheorem` (new file)	2749

Declarations diff

+ IsClosedImmersion.eq_proper_inf_monomorphisms
+ IsClosedImmersion.iff_isProper_and_mono
+ IsFinite.eq_proper_inf_locallyQuasiFinite
+ IsFinite.iff_isProper_and_locallyQuasiFinite
+ IsFinite.of_isProper_of_locallyQuasiFinite
+ LocallyQuasiFinite.of_injective
+ QuasiFiniteAt
+ Scheme.Hom.QuasiFiniteAt
+ Scheme.Hom.QuasiFiniteAt.quasiFiniteAt
+ Scheme.Hom.exists_isIso_morphismRestrict_toNormalization
+ Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization
+ Scheme.Hom.isOpen_quasiFiniteAt
+ Scheme.Hom.mem_quasiFiniteLocus
+ Scheme.Hom.quasiFiniteAt
+ Scheme.Hom.quasiFiniteLocus
+ Scheme.Hom.quasiFiniteLocus_eq_top
+ exists_etale_isCompl_of_quasiFiniteAt
+ frameHom
+ instance (priority := low) {f : X ⟶ Y} [LocallyOfFiniteType f]
+ instance [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] :
+ instance [LocallyQuasiFinite f] [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f] :
+ instance [QuasiSeparated f] [UniversallyClosed f] : UniversallyClosed f.toNormalization

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

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

…lib4 into erd1/smoothBaseChangeNormalization

…lib4 into erd1/ZMTScheme

jcommelin · 2026-02-11T12:40:46Z

Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

+lemma Scheme.Hom.QuasiFiniteAt.quasiFiniteAt
+    {x : X} (hx : f.QuasiFiniteAt x) {V : X.Opens} (hV : IsAffineOpen V) {U : Y.Opens}
+    (hU : IsAffineOpen U) (hVU : V ≤ f ⁻¹ᵁ U) (hxV : x ∈ V.1) :
+    letI := (f.appLE U V hVU).hom.toAlgebra


Can we avoid this? Should we have a RingHom.QuasiFiniteAt?

I think the issue here is that Algebra Γ(Y, U) Γ(X, V) should be an instance but couldn't because of hVU : V ≤ f ⁻¹ᵁ U. Maybe we can experiment with having Fact (V ≤ f ⁻¹ᵁ U).

As for RingHom.QuasiFiniteAt, I don't see any applications beyond applying to (f.appLE U V hVU).hom for now, and even if one adds such a predicate, the first thing one would do when applying this lemma is to algebraize[(f.appLE U V hVU).hom] and turn this back to Algebra.QuasiFiniteAt.

So I don't think this justifies having a bunch of API added for this. Unless you are satisfied by a barebones abbrev with virtually no API on it.

I have added a barebones abbrev with virtually no API on it.

Mathlib/AlgebraicGeometry/ZariskisMainTheorem.lean

…lib4 into erd1/ZMTScheme

Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

Mathlib/AlgebraicGeometry/ZariskisMainTheorem.lean

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

Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

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

joelriou · 2026-02-14T09:28:18Z

Thanks!

bors merge

mathlib-bors · 2026-02-14T10:00:32Z

Pull request successfully merged into master.

Build succeeded:

erdOne and others added 15 commits February 9, 2026 13:42

feat(RingTheory): algebraic version of Zariski's main theorem

ff9482e

fix

3adb763

Update Mathlib/RingTheory/ZariskisMainTheorem.lean

ba26647

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

feat(RingTheory): local structure of unramified algebras

4e97051

Merge branch 'master' of https://github.com/leanprover-community/math…

0647218

…lib4 into erd1/unramifiedLocalStructure3

feat(RingTheory): etale local structure of quasi-finite algebras

2171d0b

Update Mathlib/RingTheory/Unramified/LocalStructure.lean

47813ff

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

address comments

7697b38

Merge branch 'erd1/unramifiedLocalStructure3' of https://github.com/e…

fb1f745

…rdOne/mathlib4 into erd1/unramifiedLocalStructure3

fix

f4fcdda

namespace

4e772cc

fix lint

12018c8

feat(AlgebraicGeometry): normalization commutes with smooth base change

cfa5ed0

Merge branch 'erd1/unramifiedLocalStructure3' into erd1/ZMTScheme

88cf7c0

Merge branch 'erd1/localStructureQuasiFinite' into erd1/ZMTScheme

89cec4d

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 10, 2026

erdOne added 5 commits February 10, 2026 18:28

Merge branch 'master' of https://github.com/leanprover-community/math…

c5bd02b

…lib4 into erd1/smoothBaseChangeNormalization

merge

9c71cdc

Merge branch 'erd1/smoothBaseChangeNormalization' into erd1/ZMTScheme

c9dc4b7

add

0c0ab6b

Merge branch 'master' of https://github.com/leanprover-community/math…

561b75d

…lib4 into erd1/ZMTScheme

erdOne added the WIP Work in progress label Feb 10, 2026

Merge branch 'master' of https://github.com/leanprover-community/math…

20aba2c

…lib4 into erd1/ZMTScheme

erdOne added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebraic-geometry Algebraic geometry and removed WIP Work in progress labels Feb 11, 2026

github-actions bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed large-import Automatically added label for PRs with a significant increase in transitive imports labels Feb 11, 2026

oops

f2f819d

erdOne force-pushed the erd1/ZMTScheme branch from d4dc886 to f2f819d Compare February 11, 2026 09:45

erdOne force-pushed the erd1/ZMTScheme branch from 786cbd4 to f2f819d Compare February 11, 2026 10:29

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 11, 2026

jcommelin reviewed Feb 11, 2026

View reviewed changes

Mathlib/AlgebraicGeometry/ZariskisMainTheorem.lean Outdated Show resolved Hide resolved

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

change to dsimp

2be085e

erdOne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 12, 2026

erdOne and others added 3 commits February 13, 2026 16:36

Merge branch 'master' of https://github.com/leanprover-community/math…

09a2987

…lib4 into erd1/ZMTScheme

quasifinite

d260e94

Update QuasiFinite.lean

2daff28

chrisflav reviewed Feb 13, 2026

View reviewed changes

Apply suggestions from code review

2391e31

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

chrisflav reviewed Feb 13, 2026

View reviewed changes

Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean Outdated Show resolved Hide resolved

Update Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

ea538e5

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

chrisflav added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 13, 2026

erdOne added 2 commits February 13, 2026 18:08

fix

0a9359c

oops

b97aead

erdOne force-pushed the erd1/ZMTScheme branch from e56ce45 to b97aead Compare February 14, 2026 08:03

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 14, 2026

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 14, 2026

mathlib-bors bot pushed a commit that referenced this pull request Feb 14, 2026

feat(AlgebraicGeometry): Zariski's main theorem (#35093)

a5f6d77

mathlib-bors bot changed the title ~~feat(AlgebraicGeometry): Zariski's main theorem~~ [Merged by Bors] - feat(AlgebraicGeometry): Zariski's main theorem Feb 14, 2026

mathlib-bors bot closed this Feb 14, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(AlgebraicGeometry): Zariski's main theorem#35093

[Merged by Bors] - feat(AlgebraicGeometry): Zariski's main theorem#35093
erdOne wants to merge 30 commits intoleanprover-community:masterfrom
erdOne:erd1/ZMTScheme

erdOne commented Feb 10, 2026

Uh oh!

github-actions bot commented Feb 10, 2026 •

edited

Loading

Declarations diff

Uh oh!

jcommelin Feb 11, 2026

Uh oh!

erdOne Feb 12, 2026

Uh oh!

erdOne Feb 13, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Feb 14, 2026

Uh oh!

mathlib-bors bot commented Feb 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

erdOne commented Feb 10, 2026

Uh oh!

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

Uh oh!

PR summary 2598404fe9

Import changes for modified files

Declarations diff

Uh oh!

jcommelin Feb 11, 2026

Choose a reason for hiding this comment

Uh oh!

erdOne Feb 12, 2026

Choose a reason for hiding this comment

Uh oh!

erdOne Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Feb 14, 2026

Uh oh!

mathlib-bors bot commented Feb 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Feb 10, 2026 •

edited

Loading