Documentation

Mathlib.RingTheory.Ideal.LocalRing

Local rings #

Define local rings as commutative rings having a unique maximal ideal.

Main definitions #

class LocalRing (R : Type u) [Semiring R] extends Nontrivial :
  • of_is_unit_or_is_unit_of_add_one :: (
    • exists_pair_ne : x y, x y
    • isUnit_or_isUnit_of_add_one : ∀ {a b : R}, a + b = 1IsUnit a IsUnit b

      in a local ring R, if a + b = 1, then either a is a unit or b is a unit. In another word, for every a : R, either a is a unit or 1 - a is a unit.

  • )

A semiring is local if it is nontrivial and a or b is a unit whenever a + b = 1. Note that LocalRing is a predicate.

Instances
    theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add {R : Type u} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), IsUnit (a + b)IsUnit a IsUnit b) :
    theorem LocalRing.of_nonunits_add {R : Type u} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), a nonunits Rb nonunits Ra + b nonunits R) :

    A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.

    A semiring is local if it has a unique maximal ideal.

    theorem LocalRing.isUnit_or_isUnit_of_isUnit_add {R : Type u} [CommSemiring R] [LocalRing R] {a : R} {b : R} (h : IsUnit (a + b)) :
    theorem LocalRing.nonunits_add {R : Type u} [CommSemiring R] [LocalRing R] {a : R} {b : R} (ha : a nonunits R) (hb : b nonunits R) :
    a + b nonunits R

    The ideal of elements that are not units.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem LocalRing.of_surjective' {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective f) :
      class IsLocalRingHom {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) :
      • map_nonunit : ∀ (a : R), IsUnit (f a)IsUnit a

        A local ring homomorphism f : R ⟶ S will send nonunits of R to nonunits of S.

      A local ring homomorphism is a homomorphism f between local rings such that a in the domain is a unit if f a is a unit for any a. See LocalRing.local_hom_TFAE for other equivalent definitions.

      Instances
        @[simp]
        theorem isUnit_map_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) :
        IsUnit (f a) IsUnit a
        @[simp]
        theorem map_mem_nonunits_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) :
        f a nonunits S a nonunits R
        @[simp]
        theorem isUnit_of_map_unit {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [IsLocalRingHom f] (a : R) (h : IsUnit (f a)) :
        theorem of_irreducible_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) [h : IsLocalRingHom f] {x : R} (hfx : Irreducible (f x)) :
        theorem isLocalRingHom_of_comp {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) [IsLocalRingHom (RingHom.comp g f)] :
        theorem RingHom.domain_localRing {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [H : LocalRing S] (f : R →+* S) [IsLocalRingHom f] :

        If f : R →+* S is a local ring hom, then R is a local ring if S is.

        theorem map_nonunit {R : Type u} {S : Type v} [CommSemiring R] [LocalRing R] [CommSemiring S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] (a : R) (h : a LocalRing.maximalIdeal R) :

        The image of the maximal ideal of the source is contained within the maximal ideal of the target.

        A ring homomorphism between local rings is a local ring hom iff it reflects units, i.e. any preimage of a unit is still a unit. https://stacks.math.columbia.edu/tag/07BJ

        If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.

        The residue field of a local ring is the quotient of the ring by its maximal ideal.

        Equations
        Instances For
          Equations
          Equations

          The quotient map from a local ring to its residue field.

          Equations
          Instances For

            A local ring homomorphism into a field can be descended onto the residue field.

            Equations
            Instances For
              @[simp]
              theorem LocalRing.ResidueField.lift_residue_apply {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalRingHom f] (x : R) :

              The map on residue fields induced by a local homomorphism between local rings

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]

                Applying LocalRing.ResidueField.map to the identity ring homomorphism gives the identity ring homomorphism.

                theorem LocalRing.ResidueField.map_residue {R : Type u} {S : Type v} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalRingHom f] (r : R) :

                A ring isomorphism defines an isomorphism of residue fields.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem LocalRing.ResidueField.mapAut_apply {R : Type u} [CommRing R] [LocalRing R] (f : R ≃+* R) :
                  LocalRing.ResidueField.mapAut f = LocalRing.ResidueField.mapEquiv f

                  The group homomorphism from RingAut R to RingAut k where k is the residue field of R.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    If G acts on R as a MulSemiringAction, then it also acts on LocalRing.ResidueField R.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    @[simp]
                    theorem LocalRing.ResidueField.residue_smul {R : Type u} [CommRing R] [LocalRing R] (G : Type u_1) [Group G] [MulSemiringAction G R] (g : G) (r : R) :
                    ↑(LocalRing.residue R) (g r) = g ↑(LocalRing.residue R) r
                    @[reducible]
                    theorem RingEquiv.localRing {A : Type u_1} {B : Type u_2} [CommSemiring A] [LocalRing A] [CommSemiring B] (e : A ≃+* B) :