[Merged by Bors] - feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` by erdOne · Pull Request #20690 · leanprover-community/mathlib4

erdOne · 2025-01-12T19:38:13Z

github-actions · 2025-01-12T19:39:05Z

PR summary 6bc3893b73

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.LocalRing.ResidueField.Basic	1213	1154	-59 (-4.86%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal`	-59
`Mathlib.RingTheory.Henselian`	-56
`Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField`	-46
4 files `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuedField`	-38
`Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued`	-37
`Mathlib.RingTheory.Unramified.LocalRing` (new file)	1992

Declarations diff

+ FormallyUnramified.iff_map_maximalIdeal_eq
+ FormallyUnramified.isField_quotient_map_maximalIdeal
+ FormallyUnramified.map_maximalIdeal
+ FormallyUnramified.of_map_maximalIdeal
+ IsUnramifiedAt
+ finite_of_module_finite
+ instance (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
+ instance : FormallyUnramified S (ResidueField S) := .quotient _
+ instance [EssFiniteType R S] (I : Ideal S) : EssFiniteType R (S ⧸ I)
+ instance [EssFiniteType R S] (M : Submonoid S) : EssFiniteType R (Localization M)
+ instance [FormallyUnramified R S] (M : Submonoid S) : FormallyUnramified R (Localization M)
+ instance {R₀} [CommRing R₀] [Algebra R₀ R] [Module.Finite R₀ R] :
+ isNilpotent_nilradical
+ isUnramifiedAt_iff_map_eq
+ jacobson_eq_radical
+++ instance [FormallyUnramified R S] :

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 script/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/unramifiedLocalRing

Mathlib/RingTheory/Unramified/LocalRing.lean

Mathlib/RingTheory/Unramified/Locus.lean

Mathlib/RingTheory/Unramified/LocalRing.lean

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

chrisflav

Thanks!

maintainer merge

github-actions · 2025-02-03T18:17:49Z

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

jcommelin · 2025-02-04T06:08:36Z

Do you also have the version that says a map (non-locally) is unramified if it is unramified at all stalks? Because afaict this PR only deals with the local case.

erdOne · 2025-02-04T06:10:39Z

It is Algebra.unramifiedLocus_eq_univ_iff.

jcommelin · 2025-02-04T10:11:08Z

Ah right, but that is already in mathlib. So could you please rephrase the PR title? Because that's the first result I think of when I see this title.

bors d+

mathlib-bors · 2025-02-04T10:11:11Z

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

erdOne · 2025-02-04T14:06:56Z

bors merge

… qS_q` (#20690) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

mathlib-bors · 2025-02-04T14:26:26Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (103 commits) chore(PresheafedSpace): remove `mk_coe` and some comments from porting (#21382) refactor(CategoryTheory): `ConcreteCategory` instance for `FintypeCat` (#21466) refactor(Algebra/Category): clean up remaining uses of `HasForget` (#21460) chore(Algebra/Field/Basic): make some arguments implicit (#21453) chore(LinearAlgebra/TensorProduct): upgrade `TensorProduct.prodRight` (#21432) docs(Logic/Function/Defs): missing backticks (#21459) style(Logic/Embedding/Set): unindent (#21457) doc: document design choice of (AE)StronglyMeasurable.enorm and `edist` (#21423) perf(RingTheory/Artinian): reorder arguments in `IsArtinianRing.isMaximal_of_isPrime` (#21449) feat(Probability): first two derivatives of `cgf` (#21223) feat(RingTheory): `Ring.KrullDimLE` type class (#21452) chore(Probability/ProbabilityMassFunction/Binomial): typo "bernoulli" (#21455) chore: remove unused argument (#21393) feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is regular and define the Riesz measure (#20040) chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `ContinuousLinearMap` (#21443) doc(CategoryTheory/Monoidal/Category): fix expression in docs (#21445) refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a Heyting algebra is automatically a frame (#21391) chore: cleanup porting notes in TuringMachine (#20821) chore: remove @[simp] when the discr_key is a lambda (#21395) feat/doc: split files, add documentation (#21421) feat(Data/Set/Lattice): iUnion + insertion (#21322) feat(Factorial): k! divides the product of any k successive integers (#21332) feat(CI): bench-after-CI (#21414) feat: primitive group actions (#12052) feat(Algebra/GroupWithZero/Int): add lemmas about Zm0 (#21370) feat(CategoryTheory): small classes of morphisms (#21411) feat(CategoryTheory): (co)limits of constant functors (#21412) chore: rename isUnit_ofPowEqOne (#21407) chore: split mapDomain out of MonoidAlgebra.Defs (#21398) chore: generalise lemmas to `ENorm` spaces, part 1 (#21380) chore: add `simp` to `Setoid.refl` (#21107) chore: tidy various files (#21406) chore(Geometry/Manifold/IsManifold): split out material on extended charts (#21219) refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930) chore(Algebra/Category/ModuleCat): delete `ModuleCat.hasForgetModuleCat` (#21425) feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` (#20690) doc(Order/Heyting/Basic): Coheyting difference is not right adjoint but left adjoint (#21418) chore: move ProofWidgets to v0.0.51 (#21416) chore: rename mem_nonZeroDivisor_of_injective and comap_nonZeroDivisor_le_of_injective (#21408) feat: drop ordering assumption in `RootPairing.coxeterWeight_mem_set_of_isCrystallographic` (#21122) feat(AlgebraicGeometry): the diagonal of an unramified morphism is an open immersion (#21386) feat(Data/LinearIndependent): iff versions of smul action on independent sets (#21383) chore(Combinatorics/SimpleGraph): Fix `hadj` naming (#21389) chore: rename AnalyticAt.order_neq_top_iff (#21388) fix: bug in daily.yml (#21401) chore: remove `@[simp]` from `CategoryTheory.Discrete.functor_map` (#21392) chore(Algebra/PUnitInstances): generalise universes (#21381) feat(RingTheory/PowerSeries): describe when power series map is zero (#21379) feat(Tactic/Linter): options to in/exclude definitions and private decls (#21374) feat: the prime spectrum is quasi-separated (#21362) ...

… qS_q` (#20690) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

feat(RingTheory): unramified iff unramified fibers

e6c2c75

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 12, 2025

erdOne added 3 commits January 12, 2025 19:39

Update LocalRing.lean

9feb779

Update Basic.lean

99ed6d8

Update LocalRing.lean

902079b

erdOne changed the title ~~feat(RingTheory): unramified iff unramified fibers~~ feat(RingTheory): unramified iff unramified at stalks Jan 12, 2025

fix

99824e0

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 25, 2025

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

0cc9584

…lib4 into erd1/unramifiedLocalRing

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 Jan 25, 2025

chrisflav reviewed Jan 31, 2025

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

erdOne and others added 3 commits January 31, 2025 23:43

add instances

88ec4a0

split lemma

5e38747

Update Mathlib/RingTheory/Unramified/Locus.lean

6bc3893

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

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 Jan 31, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 31, 2025

chrisflav approved these changes Feb 3, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 3, 2025

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 4, 2025

erdOne changed the title ~~feat(RingTheory): unramified iff unramified at stalks~~ feat(RingTheory): unramified iff κ(q)/κ(p) is separable and pS_q = qS_q Feb 4, 2025

mathlib-bors bot pushed a commit that referenced this pull request Feb 4, 2025

feat(RingTheory): unramified iff κ(q)/κ(p) is separable and `pS_q =…

cf27f6e

… qS_q` (#20690) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

mathlib-bors bot changed the title ~~feat(RingTheory): unramified iff κ(q)/κ(p) is separable and pS_q = qS_q~~ [Merged by Bors] - feat(RingTheory): unramified iff κ(q)/κ(p) is separable and pS_q = qS_q Feb 4, 2025

mathlib-bors bot closed this Feb 4, 2025

mathlib-bors bot deleted the erd1/unramifiedLocalRing branch February 4, 2025 14:26

pfaffelh pushed a commit that referenced this pull request Feb 7, 2025

feat(RingTheory): unramified iff κ(q)/κ(p) is separable and `pS_q =…

cb45ada

… qS_q` (#20690) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q`#20690

[Merged by Bors] - feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q`#20690
erdOne wants to merge 9 commits intomasterfrom
erd1/unramifiedLocalRing

erdOne commented Jan 12, 2025

Uh oh!

github-actions bot commented Jan 12, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisflav left a comment

Uh oh!

github-actions bot commented Feb 3, 2025

Uh oh!

jcommelin commented Feb 4, 2025

Uh oh!

erdOne commented Feb 4, 2025

Uh oh!

jcommelin commented Feb 4, 2025

Uh oh!

mathlib-bors bot commented Feb 4, 2025

Uh oh!

erdOne commented Feb 4, 2025

Uh oh!

mathlib-bors bot commented Feb 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

erdOne commented Jan 12, 2025

Uh oh!

github-actions bot commented Jan 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 6bc3893b73

Import changes for modified files

Declarations diff

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 Feb 3, 2025

Uh oh!

jcommelin commented Feb 4, 2025

Uh oh!

erdOne commented Feb 4, 2025

Uh oh!

jcommelin commented Feb 4, 2025

Uh oh!

mathlib-bors bot commented Feb 4, 2025

Uh oh!

erdOne commented Feb 4, 2025

Uh oh!

mathlib-bors bot commented Feb 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Jan 12, 2025 •

edited

Loading