WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Local ring

Revision #1372 → #2463 · back to history

modifiedLocal ring (equivalent definitions)f9d36863a611
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.Defs
note—`IsLocalRing` is defined via the equivalent condition that for any a+b=1, one of a or b is a unit.
status—formalized
modifiedMaximal ideals coincide with Jacobson radical7d45a5fd6d47
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.ringJacobson_eq_maximalIdeal
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
note—In a commutative local ring the Jacobson radical equals the maximal ideal.
status—formalized
modifiedCommutative local ring characterizationc2ac9715f93c
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.of_unique_max_ideal
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.Basic
note—Combined with `IsLocalRing.maximal_ideal_unique` this gives the iff characterization.
status—formalized
modifiedLocal domain7805ce0f078d
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Not a distinct concept in Mathlib; expressible by combining `[IsLocalRing R] [IsDomain R]`.
status—partial
modifiedFields are local ringsc88bd188a02d
FieldFrom #1372To #2463
mathlib.decl—Field.instIsLocalRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.Basic
note—Every field is a local ring via the anonymous instance in `Field` namespace.
status—formalized
modifiedZ/p^n is local5ce5d8fed476
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No specific `IsLocalRing (ZMod (p^n))` instance was found.
status—not_formalized
modifiedRing with units and nilpotents is local0ac038241d66
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.of_nonunits_add
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.LocalRing.Basic
note—The exact statement was not found, but `of_nonunits_add` proves local from closure of nonunits under addition (which nilpotents satisfy).
status—partial
modifiedDiscrete valuation rings069a2cea798f
FieldFrom #1372To #2463
mathlib.decl—IsDiscreteValuationRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.DiscreteValuationRing.Basic
note—DVRs are formalized as `IsDiscreteValuationRing`, defined as a local PID that is not a field.
status—formalized
modifiedFormal power series ring is local2a25619b652e
FieldFrom #1372To #2463
mathlib.decl—MvPowerSeries.instIsLocalRing
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.MvPowerSeries.Inverse
note—Instance shows `IsLocalRing (MvPowerSeries σ R)` whenever `R` is local; specializes to F[[X]].
status—formalized
modifiedFormal power series over a local ring is local24ab17ce7883
FieldFrom #1372To #2463
mathlib.decl—MvPowerSeries.instIsLocalRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.MvPowerSeries.Inverse
note—The instance `[IsLocalRing R] : IsLocalRing (MvPowerSeries σ R)` is exactly this.
status—formalized
modifiedDual numbers and F[X]/(X^n) are localae016c6e8de7
FieldFrom #1372To #2463
mathlib.decl—DualNumber.instIsLocalRing
mathlib.match_kind—special_case
mathlib.module—Mathlib.RingTheory.DualNumber
note—Dual numbers are formalized as local (instance in DualNumber), but F[X]/(X^n) does not have an explicit `IsLocalRing` instance.
status—partial
modifiedQuotients of local rings are localb1543c5ec077
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.of_surjective'
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.LocalRing.Basic
note—Any surjective image (hence any nonzero quotient) of a local ring is local via `of_surjective'`.
status—formalized
modifiedRationals with odd denominatore9e30ac11aed
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This specific ring Z_(2) is not defined as a named object; it would arise as `Localization.AtPrime (2)`.
status—not_formalized
modifiedLocalization at a prime ideal593fa26a8526
FieldFrom #1372To #2463
mathlib.decl—Localization.AtPrime.isLocalRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.Localization.AtPrime.Basic
note—The instance shows `IsLocalRing (Localization P.primeCompl)` for any prime ideal P.
status—formalized
modifiedPolynomial ring is not local71639f260e43
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No specific `¬ IsLocalRing (Polynomial R)` lemma; general non-local infrastructure exists in `NonLocalRing.lean`.
status—not_formalized
modifiedIntegers are not local78b94751e6b2
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No specific `¬ IsLocalRing ℤ` lemma was found.
status—not_formalized
modifiedZ/(pq) is not localcb5d038d2d16
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No specific lemma about ZMod (p*q) with distinct primes not being local.
status—not_formalized
modifiedGerms of continuous functionsb432c02cdef6
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has germs (`Germ`) and stalks but not a specific ring-of-germs-of-continuous-functions construction.
status—not_formalized
modifiedInvertible germ characterization6daf92a26f65
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalization of the ring of germs of continuous functions or invertibility characterization there.
status—not_formalized
modifiedRing of germs is localcafb279716e3
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The ring of germs of continuous functions is not set up as an `IsLocalRing` in Mathlib.
status—not_formalized
modifiedRings of germs in various settingsf344696605c7
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalized ring-of-germs-of-continuous/smooth/holomorphic-functions instances of `IsLocalRing`.
status—not_formalized
modifiedValuation ring2c95385a23b8
FieldFrom #1372To #2463
mathlib.decl—ValuationRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.Valuation.ValuationRing
note—`ValuationRing` is the Mathlib predicate for valuation rings.
status—formalized
modifiedValuation rings are local72f2c62ba81f
FieldFrom #1372To #2463
mathlib.decl—ValuationRing.isLocalRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.Valuation.ValuationRing
note—The instance `ValuationRing.isLocalRing` gives `IsLocalRing A` for a valuation ring `A`.
status—formalized
modifiedEndomorphism ring local iff indecomposable21bb5e546d3d
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma tying local endomorphism ring to module indecomposability was found.
status—not_formalized
addedFinite length indecomposable module has local endomorphism ringb4614ff288d8
modifiedGroup algebra kG of a p-group is local73ce0cfd1ebc
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `IsLocalRing (MonoidAlgebra k G)` instance for p-group over char-p field was found.
status—not_formalized
modifiedm-adic topology05eeb03fb201
FieldFrom #1372To #2463
mathlib.decl—Ideal.adicTopology
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
note—`Ideal.adicTopology` gives the I-adic topology for any ideal; specializing to the maximal ideal gives the m-adic topology.
status—formalized
modifiedKrull's intersection theoremeda80189b2c1
FieldFrom #1372To #2463
mathlib.decl—Ideal.iInf_pow_eq_bot_of_isLocalRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.Filtration
note—Krull's intersection theorem for Noetherian local rings: `⨅ n, I^n = ⊥` for `I ≠ ⊤`.
status—formalized
modifiedGerms of smooth functions show Noetherian assumption is crucial867063902e83
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The ring of germs of smooth functions and its non-Noetherian local structure is not formalized.
status—not_formalized
modifiedCohen structure theoreme3d206de99d6
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Cohen structure theorem for complete Noetherian local rings is not in Mathlib.
status—not_formalized
modifiedResidue fieldc441efbd59e7
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.ResidueField
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.ResidueField.Defs
note—`IsLocalRing.ResidueField R := R ⧸ maximalIdeal R`, with a Field instance.
status—formalized
modifiedLocal ring homomorphism85859e05067f
FieldFrom #1372To #2463
mathlib.decl—IsLocalHom
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.RingHom.Basic
note—`IsLocalHom` predicate; used with `IsLocalRing` throughout the RingHom subfolder.
status—formalized
addedLocal ring homomorphisms are exactly continuous ring homomorphismsb65aa0899cb4
modifiedJacobson radical equals non-units482dd9acc0d4
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.mem_maximalIdeal
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
note—Combining `IsLocalRing.mem_maximalIdeal` (maximal ideal = nonunits) with `ringJacobson_eq_maximalIdeal` yields the statement, but no single lemma stated as Jacobson = nonunits.
status—partial
addedJacobson radical is the unique maximal two-sided ideal054fa7033bb4
modifiedEquivalent conditions for invertibility55d56804d603
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.notMem_maximalIdeal
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
note—`x ∉ maximalIdeal R ↔ IsUnit x` captures the invertibility characterization.
status—formalized
modifiedFactor ring R/m is a skew fieldcefa58d19288
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.ResidueField.field
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.LocalRing.ResidueField.Defs
note—The Field instance on `ResidueField R = R ⧸ maximalIdeal R` gives the (commutative) skew-field statement.
status—formalized
modifiedQuotient by two-sided ideal is locala45b327197af
FieldFrom #1372To #2463
mathlib.decl—IsLocalRing.of_surjective'
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.LocalRing.Basic
note—Applying `of_surjective'` to `Ideal.Quotient.mk` (as done in Quotient.lean) yields the local quotient.
status—formalized
modifiedKaplansky: projective modules over local rings are free199fac88586a
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Kaplansky's theorem that projective modules over local rings are free is not in Mathlib.
status—not_formalized
modifiedMorita equivalence classifies rings Morita equivalent to local rings4355a4fc8fc0
FieldFrom #1372To #2463
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Morita equivalence and matrix rings exist in Mathlib but the classification of rings Morita equivalent to a local ring is not formalized.
status—not_formalized