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 :

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.

  • of_is_unit_or_is_unit_of_add_one :: (
    • exists_pair_ne : ∃ (x : R) (y : R), 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.

  • )
Instances
    theorem LocalRing.isUnit_or_isUnit_of_add_one {R : Type u} [Semiring R] [self : LocalRing R] {a : R} {b : R} (h : a + b = 1) :

    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.

    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.

    theorem LocalRing.of_unique_max_ideal {R : Type u} [CommSemiring R] (h : ∃! I : Ideal R, I.IsMaximal) :

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

    theorem LocalRing.of_unique_nonzero_prime {R : Type u} [CommSemiring R] (h : ∃! P : Ideal R, P P.IsPrime) :
    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
    Instances For
      Equations
      • =
      theorem LocalRing.maximal_ideal_unique (R : Type u) [CommSemiring R] [LocalRing R] :
      ∃! I : Ideal R, I.IsMaximal
      theorem LocalRing.eq_maximalIdeal {R : Type u} [CommSemiring R] [LocalRing R] {I : Ideal R} (hI : I.IsMaximal) :
      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) :

      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.

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

      Instances
        theorem IsLocalRingHom.map_nonunit {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} [self : IsLocalRingHom f] (a : R) :
        IsUnit (f a)IsUnit a

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

        Equations
        • =
        @[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) :
        instance isLocalRingHom_comp {R : Type u} {S : Type v} {T : Type w} [Semiring R] [Semiring S] [Semiring T] (g : S →+* T) (f : R →+* S) [IsLocalRingHom g] [IsLocalRingHom f] :
        IsLocalRingHom (g.comp f)
        Equations
        • =
        instance isLocalRingHom_equiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R ≃+* S) :
        Equations
        • =
        @[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 (g.comp 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]

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

              Equations
              Instances For
                @[simp]

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

                A ring isomorphism defines an isomorphism of residue fields.

                Equations
                Instances For
                  @[simp]
                  theorem LocalRing.ResidueField.mapEquiv_trans {R : Type u} {S : Type v} {T : Type w} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing T] [LocalRing T] (e₁ : R ≃+* S) (e₂ : S ≃+* T) :
                  @[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
                  • LocalRing.ResidueField.mapAut = { toFun := LocalRing.ResidueField.mapEquiv, map_one' := , map_mul' := }
                  Instances For
                    @[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) :
                    @[instance 100]
                    instance Field.instLocalRing (K : Type u') [Field K] :
                    Equations
                    • =
                    theorem RingEquiv.localRing {A : Type u_1} {B : Type u_2} [CommSemiring A] [LocalRing A] [CommSemiring B] (e : A ≃+* B) :