Skip to content

[Merged by Bors] - feat(RingTheory/LocalRing): add instance Unique (MaximalSpectrum R) for a local ring R#20801

Closed
mistarro wants to merge 2 commits intomasterfrom
mistarro/unique-maximal-spectrum-of-local-ring
Closed

[Merged by Bors] - feat(RingTheory/LocalRing): add instance Unique (MaximalSpectrum R) for a local ring R#20801
mistarro wants to merge 2 commits intomasterfrom
mistarro/unique-maximal-spectrum-of-local-ring

Conversation

@mistarro
Copy link
Copy Markdown
Collaborator

@mistarro mistarro commented Jan 16, 2025

Introduce the instance Unique (MaximalSpectrum R) for a local ring R.

I need this for simpler proofs, for example that a local reduced artinian ring is a field (using RingEquiv.piUnique introduced in #20794). I think it's generally useful.

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jan 16, 2025
@mistarro mistarro added easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc) labels Jan 16, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 16, 2025 •
edited
Loading

PR summary 5708c32920

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic 1111 1112 +1 (+0.09%)
Import changes for all files
Files Import difference
137 files Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Module.Presentation.Differentials Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.ZetaValues Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.DualNumber Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension Mathlib.RingTheory.Filtration Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Generators Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.Henselian Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.Invariant Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.Presentation Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Support Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Sheaves.CommRingCat
 1

Declarations diff

+ instance : Unique (MaximalSpectrum R)

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

erdOne
erdOne reviewed Jan 16, 2025
View reviewed changes
@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 16, 2025
@mistarro @erdOne
Update Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
5708c32 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@mistarro mistarro removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 16, 2025
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jan 16, 2025

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 16, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 16, 2025
jcommelin
jcommelin reviewed Jan 17, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 17, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2025
@mistarro
feat(RingTheory/LocalRing): add instance Unique (MaximalSpectrum R)…
116f37b 
… for a local ring `R` (#20801)

Introduce the instance `Unique (MaximalSpectrum R)` for a local ring `R`.

I need this for simpler proofs, for example that a local reduced artinian ring is a field (using `RingEquiv.piUnique` introduced in #20794). I think it's generally useful.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 17, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2025
@mistarro
feat(RingTheory/LocalRing): add instance Unique (MaximalSpectrum R)…
767b250 
… for a local ring `R` (#20801)

Introduce the instance `Unique (MaximalSpectrum R)` for a local ring `R`.

I need this for simpler proofs, for example that a local reduced artinian ring is a field (using `RingEquiv.piUnique` introduced in #20794). I think it's generally useful.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 17, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/LocalRing): add instance Unique (MaximalSpectrum R) for a local ring R [Merged by Bors] - feat(RingTheory/LocalRing): add instance Unique (MaximalSpectrum R) for a local ring R Jan 17, 2025
@mathlib-bors mathlib-bors bot closed this Jan 17, 2025
@mathlib-bors mathlib-bors bot deleted the mistarro/unique-maximal-spectrum-of-local-ring branch January 17, 2025 06:43
Julian added a commit that referenced this pull request Jan 20, 2025
@Julian
Merge branch 'polynomial-sequences' into bhargava-factorial
856ec0d 
* polynomial-sequences: (149 commits)
  Aha, here's how to get Lean to stop showing S.elems' in the infoview.
  Try satisfying the linter gods again.
  Probably enough initial tidying to send the PR.
  Kill more temporary names.
  Touch more natDegree.
  Does protected satisfy the docstring linter?
  Bit shorter.
  More
  Quiet linters.
  Remove redundant imports.
  Copyright header and more twiddling.
  Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out
  feat(Polynomial): polynomial sequences are bases for R[X]
  chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765)
  chore(Associated): split out `Ring` results (#20737)
  feat(AlgebraicGeometry): flat morphisms of schemes (#19790)
  feat(AlgebraicGeometry): scheme-theoretic fibre (#19427)
  chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785)
  doc: typo (#20829)
  feat(CategoryTheory): condition for an induced functor between comma categories to be final  (#20139)
  feat(1000.yaml): allow statements of theorems also (#20637)
  feat(Algebra/Homology/Embedding): homology of truncGE' (#19570)
  chore: cleanup many porting notes in Combinatorics (#20823)
  chore: eliminate porting notes about `deriving Fintype` (#20820)
  feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)
  feat: define bases of root pairings (#20667)
  feat(Tactic): basic ConcreteCategory support for elementwise (#20811)
  feat(CategoryTheory): define unbundled `ConcreteCategory` class  (#20810)
  chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809)
  feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783)
  chore(yaml_check.py): re-format (#20807)
  feat: elementary estimate for Real.log (#20766)
  feat: definition of linear topologies (#14990)
  feat(RingTheory): flatness over a semiring (#19115)
  feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550)
  feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203)
  feat(Algebra/Ring): `RingEquiv.piUnique` (#20794)
  feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801)
  chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802)
  chore: restore `def` to `adicCompletion` (#20796)
  refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643)
  feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544)
  chore(Mathlib/Computability/TuringMachine): split file (#20790)
  feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753)
  feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752)
  feat(Set/Finite): a set is finite if its image and fibers are finite (#20751)
  chore: cleanup .gitignore files (#20795)
  feat(Topology/Group/Profinite):  Profinite group is limit of finite group (#16992)
  feat(Combinatorics/SimpleGraph): vertices in cycles (#20602)
  CI: merge `bot_fix_style` actions (#20789)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mistarro @erdOne @jcommelin