`Definitions/Def_Mathlib_RingTheory_LocalRing_Defs.lean`

definition moduleadapted from the Imperial College London FLT project: FLT/Mathlib/RingTheory/LocalRing/Defs.lean

Local ring structure on quotients of a local ring

The standing context is a commutative ring R that is local, an ideal I \subseteq R, and the assumption that the quotient ring R/I is nontrivial. Two instances are registered under these hypotheses.

The first, IsLocalRing.quot, asserts that R/I is again a local ring in Mathlib's sense (nontrivial, with the non-units closed under addition, equivalently a unique maximal ideal). It is obtained from the general fact that a nontrivial ring which is the image of a local ring under a surjective ring homomorphism is local, applied to the canonical projection R \to R/I, whose surjectivity is Ideal.Quotient.mk_surjective.

The second, IsLocalHom.quotient_mk, asserts that the canonical map R \to R/I, taken in its guise as the algebra map algebraMap R (R ⧸ I), is a local homomorphism: an element a \in R whose residue class in R/I is a unit is itself a unit of R. Equivalently, the preimage of the maximal ideal of R/I is the maximal ideal of R. This too comes from surjectivity of the projection, via the corresponding statement for surjective homomorphisms out of a local ring.

Relation to Mathlib

Both facts are instances packaging Mathlib lemmas (IsLocalRing.of_surjective' and IsLocalHom.of_surjective) for the special case of a quotient ring, so that Lean's instance search finds the local ring structure on R ⧸ I and the locality of algebraMap R (R ⧸ I) automatically; no new notion is introduced.

English text generated automatically from the Lean source; the Lean statement is authoritative.

11 lines
2 declarations
used in the statements of 0 theorems and imported by 0 proofs
imports 0 definition modules

Source file: Definitions/Def_Mathlib_RingTheory_LocalRing_Defs.lean

Imports

only Mathlib

Imported by

Def_Deformations_IsResidueAlgebra

Source

import Mathlib

variable {R : Type*} [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)]

open IsLocalRing

instance IsLocalRing.quot : IsLocalRing (R ⧸ I) := .of_surjective' _ Ideal.Quotient.mk_surjective

instance IsLocalHom.quotient_mk : IsLocalHom (algebraMap R (R ⧸ I)) :=
  .of_surjective _ Ideal.Quotient.mk_surjective

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).