Documentation

Mathlib.RingTheory.LocalProperties

Local properties of commutative rings #

In this file, we provide the proofs of various local properties.

Naming Conventions #

Main results #

The following properties are covered:

def LocalizationPreserves (P : (R : Type u) → [inst : CommRing R] → Prop) :

A property P of comm rings is said to be preserved by localization if P holds for M⁻¹R whenever P holds for R.

Equations
Instances For
    def OfLocalizationMaximal (P : (R : Type u) → [inst : CommRing R] → Prop) :

    A property P of comm rings satisfies OfLocalizationMaximal if P holds for R whenever P holds for Rₘ for all maximal ideal m.

    Equations
    Instances For
      def RingHom.LocalizationPreserves (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

      A property P of ring homs is said to be preserved by localization if P holds for M⁻¹R →+* M⁻¹S whenever P holds for R →+* S.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def RingHom.OfLocalizationFiniteSpan (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

        A property P of ring homs satisfies RingHom.OfLocalizationFiniteSpan if P holds for R →+* S whenever there exists a finite set { r } that spans R such that P holds for Rᵣ →+* Sᵣ.

        Note that this is equivalent to RingHom.OfLocalizationSpan via RingHom.ofLocalizationSpan_iff_finite, but this is easier to prove.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def RingHom.OfLocalizationSpan (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

          A property P of ring homs satisfies RingHom.OfLocalizationFiniteSpan if P holds for R →+* S whenever there exists a set { r } that spans R such that P holds for Rᵣ →+* Sᵣ.

          Note that this is equivalent to RingHom.OfLocalizationFiniteSpan via RingHom.ofLocalizationSpan_iff_finite, but this has less restrictions when applying.

          Equations
          Instances For
            def RingHom.HoldsForLocalizationAway (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

            A property P of ring homs satisfies RingHom.HoldsForLocalizationAway if P holds for each localization map R →+* Rᵣ.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def RingHom.OfLocalizationFiniteSpanTarget (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

              A property P of ring homs satisfies RingHom.OfLocalizationFiniteSpanTarget if P holds for R →+* S whenever there exists a finite set { r } that spans S such that P holds for R →+* Sᵣ.

              Note that this is equivalent to RingHom.OfLocalizationSpanTarget via RingHom.ofLocalizationSpanTarget_iff_finite, but this is easier to prove.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def RingHom.OfLocalizationSpanTarget (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

                A property P of ring homs satisfies RingHom.OfLocalizationSpanTarget if P holds for R →+* S whenever there exists a set { r } that spans S such that P holds for R →+* Sᵣ.

                Note that this is equivalent to RingHom.OfLocalizationFiniteSpanTarget via RingHom.ofLocalizationSpanTarget_iff_finite, but this has less restrictions when applying.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def RingHom.OfLocalizationPrime (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

                  A property P of ring homs satisfies RingHom.OfLocalizationPrime if P holds for R whenever P holds for Rₘ for all prime ideals p.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    structure RingHom.PropertyIsLocal (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :

                    A property of ring homs is local if it is preserved by localizations and compositions, and for each { r } that spans S, we have P (R →+* S) ↔ ∀ r, P (R →+* Sᵣ).

                    Instances For
                      theorem RingHom.PropertyIsLocal.LocalizationPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (self : RingHom.PropertyIsLocal P) :
                      theorem RingHom.PropertyIsLocal.StableUnderComposition {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (self : RingHom.PropertyIsLocal P) :
                      theorem RingHom.HoldsForLocalizationAway.of_bijective {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) (H : RingHom.HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) (hf : Function.Bijective f) :
                      P f
                      theorem RingHom.PropertyIsLocal.respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.PropertyIsLocal P) :
                      theorem RingHom.LocalizationPreserves.away {R : Type u} {S : Type u} [CommRing R] [CommRing S] {R' : Type u} {S' : Type u} [CommRing R'] [CommRing S'] {f : R →+* S} [Algebra R R'] [Algebra S S'] {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (H : RingHom.LocalizationPreserves P) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : P f) :
                      theorem RingHom.PropertyIsLocal.ofLocalizationSpan {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.PropertyIsLocal P) :
                      theorem RingHom.OfLocalizationSpanTarget.ofIsLocalization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP : RingHom.OfLocalizationSpanTarget fun {R S : Type u} [CommRing R] [CommRing S] => P) (hP' : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ) (hT : ∀ (r : s), ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)) :
                      P f
                      theorem Ideal.le_of_localization_maximal {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : ∀ (P : Ideal R) (hP : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I Ideal.map (algebraMap R (Localization.AtPrime P)) J) :
                      I J

                      Let I J : Ideal R. If the localization of I at each maximal ideal P is included in the localization of J at P, then I ≤ J.

                      theorem Ideal.eq_of_localization_maximal {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (h : ∀ (P : Ideal R) (x : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) J) :
                      I = J

                      Let I J : Ideal R. If the localization of I at each maximal ideal P is equal to the localization of J at P, then I = J.

                      theorem ideal_eq_bot_of_localization' {R : Type u} [CommRing R] (I : Ideal R) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ) :
                      I =

                      An ideal is trivial if its localization at every maximal ideal is trivial.

                      theorem ideal_eq_bot_of_localization {R : Type u} [CommRing R] (I : Ideal R) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ) :
                      I =

                      An ideal is trivial if its localization at every maximal ideal is trivial.

                      theorem eq_zero_of_localization {R : Type u} [CommRing R] (r : R) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0) :
                      r = 0
                      Equations
                      • =
                      theorem surjective_localRingHom_of_surjective {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Function.Surjective f) (P : Ideal S) [P.IsPrime] :

                      A surjective ring homomorphism R →+* S induces a surjective homomorphism R_{f⁻¹(P)} →+* S_P for every prime ideal P of S.

                      theorem Module.Finite_of_isLocalization (R : Type u_1) (S : Type u_2) (Rₚ : Type u_3) (Sₚ : Type u_4) [CommSemiring R] [CommRing S] [CommRing Rₚ] [CommRing Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] :
                      Module.Finite Rₚ Sₚ

                      If S is a finite R-algebra, then S' = M⁻¹S is a finite R' = M⁻¹R-algebra.

                      theorem localization_away_map_finite {R : Type u} {S : Type u} [CommRing R] [CommRing S] (R' : Type u) (S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) [Algebra R R'] [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : f.Finite) :
                      (IsLocalization.Away.map R' S' f r).Finite
                      theorem IsLocalization.smul_mem_finsetIntegerMultiple_span {R : Type u} {S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (S' : Type u) [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S') (hx : (algebraMap S S') x Submodule.span R s) :
                      ∃ (m : { x : R // x M }), m x Submodule.span R (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

                      Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S. If the image of some x : S falls in the span of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the span of IsLocalization.finsetIntegerMultiple _ s over R.

                      theorem multiple_mem_span_of_mem_localization_span {R : Type u} [CommRing R] (M : Submonoid R) (R' : Type u) [CommRing R'] [Algebra R R'] {N : Type u_1} [AddCommMonoid N] [Module R N] [Module R' N] [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) (hx : x Submodule.span R' s) :
                      ∃ (t : { x : R // x M }), t x Submodule.span R s

                      If M is an R' = S⁻¹R module, and x ∈ span R' s, then t • x ∈ span R s for some t : S.

                      theorem multiple_mem_adjoin_of_mem_localization_adjoin {R : Type u} {S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (R' : Type u) [CommRing R'] [Algebra R R'] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S) (hx : x Algebra.adjoin R' s) :
                      ∃ (t : { x : R // x M }), t x Algebra.adjoin R s

                      If S is an R' = M⁻¹R algebra, and x ∈ adjoin R' s, then t • x ∈ adjoin R s for some t : M.

                      theorem localization_away_map_finiteType {R : Type u} {S : Type u} [CommRing R] [CommRing S] (R' : Type u) (S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) [Algebra R R'] [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : f.FiniteType) :
                      (IsLocalization.Away.map R' S' f r).FiniteType
                      theorem IsLocalization.exists_smul_mem_of_mem_adjoin {R : Type u} {S : Type u} [CommRing R] [CommRing S] {S' : Type u} [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S') (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s) A) (hA₂ : M A.toSubmonoid) (hx : (algebraMap S S') x Algebra.adjoin R s) :
                      ∃ (m : { x : S // x M }), m x A

                      Let S be an R-algebra, M a submonoid of S, S' = M⁻¹S. Suppose the image of some x : S falls in the adjoin of some finite s ⊆ S' over R, and A is an R-subalgebra of S containing both M and the numerators of s. Then, there exists some m : M such that m • x falls in A.

                      theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple {R : Type u} {S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) {S' : Type u} [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S') (hx : (algebraMap S S') x Algebra.adjoin R s) :
                      ∃ (m : { x : R // x M }), m x Algebra.adjoin R (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

                      Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S. If the image of some x : S falls in the adjoin of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the adjoin of IsLocalization.finsetIntegerMultiple _ s over R.