HepLean Documentation

Mathlib.RingTheory.Localization.Away.Basic

Localizations away from an element #

Main definitions #

Implementation notes #

See Mathlib/RingTheory/Localization/Basic.lean for a design overview.

Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

@[reducible, inline]
abbrev IsLocalization.Away {R : Type u_1} [CommSemiring R] (x : R) (S : Type u_4) [CommSemiring S] [Algebra R S] :

Given x : R, the typeclass IsLocalization.Away x S states that S is isomorphic to the localization of R at the submonoid generated by x. See IsLocalization.Away.mk for a specialized constructor.

Equations
Instances For
    noncomputable def IsLocalization.Away.invSelf {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] :
    S

    Given x : R and a localization map F : R →+* S away from x, invSelf is (F x)⁻¹.

    Equations
    Instances For
      noncomputable def IsLocalization.Away.sec {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] (s : S) :

      For s : S with S being the localization of R away from x, this is a choice of (r, n) : R × ℕ such that s * algebraMap R S (x ^ n) = algebraMap R S r.

      Equations
      Instances For
        theorem IsLocalization.Away.sec_spec {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] (s : S) :
        theorem IsLocalization.Away.algebraMap_pow_isUnit {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] (n : ) :
        IsUnit ((algebraMap R S) x ^ n)
        theorem IsLocalization.Away.surj {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] (z : S) :
        ∃ (n : ) (a : R), z * (algebraMap R S) x ^ n = (algebraMap R S) a
        theorem IsLocalization.Away.exists_of_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] {a b : R} (h : (algebraMap R S) a = (algebraMap R S) b) :
        ∃ (n : ), x ^ n * a = x ^ n * b
        theorem IsLocalization.Away.mk {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (r : R) (map_unit : IsUnit ((algebraMap R S) r)) (surj : ∀ (s : S), ∃ (n : ) (a : R), s * (algebraMap R S) r ^ n = (algebraMap R S) a) (exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b∃ (n : ), r ^ n * a = r ^ n * b) :

        Specialized constructor for IsLocalization.Away.

        theorem IsLocalization.Away.of_associated {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {r r' : R} (h : Associated r r') [IsLocalization.Away r S] :

        If r and r' are associated elements of R, an R-algebra S is the localization of R away from r if and only of it is the localization of R away from r'.

        theorem IsLocalization.Away.isUnit_of_dvd {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [IsLocalization.Away x S] {r : R} (h : r x) :
        IsUnit ((algebraMap R S) r)
        noncomputable def IsLocalization.Away.lift {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)) :
        S →+* P

        Given x : R, a localization map F : R →+* S away from x, and a map of CommSemirings g : R →+* P such that g x is invertible, the homomorphism induced from S to P sending z : S to g y * (g x)⁻ⁿ, where y : R, n : ℕ are such that z = F y * (F x)⁻ⁿ.

        Equations
        Instances For
          @[simp]
          theorem IsLocalization.Away.lift_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)) (a : R) :
          @[simp]
          theorem IsLocalization.Away.lift_comp {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)) :
          @[deprecated IsLocalization.Away.lift_eq]
          theorem IsLocalization.Away.AwayMap.lift_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)) (a : R) :

          Alias of IsLocalization.Away.lift_eq.

          @[deprecated IsLocalization.Away.lift_comp]
          theorem IsLocalization.Away.AwayMap.lift_comp {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)) :

          Alias of IsLocalization.Away.lift_comp.

          noncomputable def IsLocalization.Away.awayToAwayLeft {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] (y : R) [Algebra R P] [IsLocalization.Away (y * x) P] :
          S →+* P

          Given x y : R and localizations S, P away from x and y * x respectively, the homomorphism induced from S to P.

          Equations
          Instances For
            noncomputable def IsLocalization.Away.awayToAwayRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] (y : R) [Algebra R P] [IsLocalization.Away (x * y) P] :
            S →+* P

            Given x y : R and localizations S, P away from x and x * y respectively, the homomorphism induced from S to P.

            Equations
            Instances For
              theorem IsLocalization.Away.awayToAwayLeft_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] (y : R) [Algebra R P] [IsLocalization.Away (y * x) P] (a : R) :
              theorem IsLocalization.Away.awayToAwayRight_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [IsLocalization.Away x S] (y : R) [Algebra R P] [IsLocalization.Away (x * y) P] (a : R) :
              noncomputable def IsLocalization.Away.map {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (f : R →+* P) (r : R) [IsLocalization.Away r S] [IsLocalization.Away (f r) Q] :
              S →+* Q

              Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.

              Equations
              Instances For
                instance IsLocalization.Away.instMapRingHomPowersOfCoe {A : Type u_5} [CommSemiring A] {B : Type u_6} [CommSemiring B] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] {f : A →+* B} (a : A) [IsLocalization.Away (f a) Bₚ] :
                Equations
                • =
                noncomputable def IsLocalization.Away.mapₐ {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] (Aₚ : Type u_7) [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] :
                Aₚ →ₐ[R] Bₚ

                Given a algebra map f : A →ₐ[R] B and an element a : A, we may construct a map Aₐ →ₐ[R] Bₐ.

                Equations
                Instances For
                  @[simp]
                  theorem IsLocalization.Away.mapₐ_apply {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] (Aₚ : Type u_7) [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (x : Aₚ) :
                  (IsLocalization.Away.mapₐ Aₚ Bₚ f a) x = (IsLocalization.Away.map Aₚ Bₚ f.toRingHom a) x
                  theorem IsLocalization.Away.mapₐ_injective_of_injective {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] {Aₚ : Type u_7} [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] {Bₚ : Type u_8} [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (hf : Function.Injective f) :
                  theorem IsLocalization.Away.mapₐ_surjective_of_surjective {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] {Aₚ : Type u_7} [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] {Bₚ : Type u_8} [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (hf : Function.Surjective f) :
                  theorem IsLocalization.Away.mul {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_5) [CommSemiring T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (x y : R) [IsLocalization.Away x S] [IsLocalization.Away ((algebraMap R S) y) T] :

                  Localizing the localization of R at x at the image of y is the same as localizing R at y * x. See IsLocalization.Away.mul' for the x * y version.

                  theorem IsLocalization.Away.mul' {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_5) [CommSemiring T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (x y : R) [IsLocalization.Away x S] [IsLocalization.Away ((algebraMap R S) y) T] :

                  Localizing the localization of R at x at the image of y is the same as localizing R at x * y. See IsLocalization.Away.mul for the y * x version.

                  Localizing the localization of R at x at the image of y is the same as localizing R at y * x.

                  Equations
                  • =

                  Localizing the localization of R at x at the image of y is the same as localizing R at x * y.

                  Equations
                  • =
                  theorem IsLocalization.Away.commutes {R : Type u_5} [CommSemiring R] (S₁ : Type u_6) (S₂ : Type u_7) (T : Type u_8) [CommSemiring S₁] [CommSemiring S₂] [CommSemiring T] [Algebra R S₁] [Algebra R S₂] [Algebra R T] [Algebra S₁ T] [Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T] (x y : R) [IsLocalization.Away x S₁] [IsLocalization.Away y S₂] [IsLocalization.Away ((algebraMap R S₂) x) T] :

                  If S₁ is the localization of R away from f and S₂ is the localization away from g, then any localization T of S₂ away from f is also a localization of S₁ away from g.

                  noncomputable def IsLocalization.atUnit (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (x : R) (e : IsUnit x) [IsLocalization.Away x S] :

                  The localization away from a unit is isomorphic to the ring.

                  Equations
                  Instances For
                    noncomputable def IsLocalization.atOne (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization.Away 1 S] :

                    The localization at one is isomorphic to the ring.

                    Equations
                    Instances For
                      theorem IsLocalization.away_of_isIdempotentElem_of_mul {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] {e : R} (he : IsIdempotentElem e) (H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y e * x = e * y) (H' : Function.Surjective (algebraMap R S)) :
                      instance IsLocalization.away_fst {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] :
                      Equations
                      • =
                      instance IsLocalization.away_snd {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] :
                      Equations
                      • =
                      @[reducible, inline]
                      noncomputable abbrev Localization.awayLift {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : R →+* P) (r : R) (hr : IsUnit (f r)) :

                      Given a map f : R →+* S and an element r : R, such that f r is invertible, we may construct a map Rᵣ →+* S.

                      Equations
                      Instances For
                        theorem Localization.awayLift_mk {R : Type u_1} [CommSemiring R] {A : Type u_4} [CommRing A] (f : R →+* A) (r a : R) (v : A) (hv : f r * v = 1) (j : ) :
                        (Localization.awayLift f r ) (Localization.mk a r ^ j, ) = f a * v ^ j
                        @[reducible, inline]
                        noncomputable abbrev Localization.awayMap {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : R →+* P) (r : R) :

                        Given a map f : R →+* S and an element r : R, we may construct a map Rᵣ →+* Sᵣ.

                        Equations
                        Instances For
                          @[reducible, inline]
                          noncomputable abbrev Localization.awayMapₐ {R : Type u_1} [CommSemiring R] {A : Type u_4} [CommSemiring A] [Algebra R A] {B : Type u_5} [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (a : A) :

                          Given a map f : A →ₐ[R] B and an element a : A, we may construct a map Aₐ →ₐ[R] Bₐ.

                          Equations
                          Instances For
                            theorem Localization.existsUnique_algebraMap_eq_of_span_eq_top {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Ideal.span s = ) (f : (a : s) → Localization.Away a) (h : ∀ (a b : s), (IsLocalization.Away.awayToAwayRight a b) (f a) = (IsLocalization.Away.awayToAwayLeft b a) (f b)) :
                            ∃! r : R, ∀ (a : s), (algebraMap R (Localization.Away a)) r = f a

                            The sheaf condition for the structure sheaf on Spec R for a covering of the whole prime spectrum by basic opens.

                            noncomputable def selfZPow {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (m : ) :
                            B

                            selfZPow x (m : ℤ) is x ^ m as an element of the localization away from x.

                            Equations
                            Instances For
                              theorem selfZPow_of_nonneg {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n : } (hn : 0 n) :
                              selfZPow x B n = (algebraMap R B) x ^ n.natAbs
                              @[simp]
                              theorem selfZPow_natCast {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ) :
                              selfZPow x B d = (algebraMap R B) x ^ d
                              @[simp]
                              theorem selfZPow_zero {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] :
                              selfZPow x B 0 = 1
                              theorem selfZPow_of_neg {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n : } (hn : n < 0) :
                              theorem selfZPow_of_nonpos {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n : } (hn : n 0) :
                              @[simp]
                              theorem selfZPow_neg_natCast {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ) :
                              @[simp]
                              theorem selfZPow_sub_natCast {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n m : } :
                              selfZPow x B (n - m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)
                              @[deprecated selfZPow_natCast]
                              theorem selfZPow_coe_nat {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ) :
                              selfZPow x B d = (algebraMap R B) x ^ d

                              Alias of selfZPow_natCast.

                              @[deprecated selfZPow_neg_natCast]
                              theorem selfZPow_neg_coe_nat {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ) :

                              Alias of selfZPow_neg_natCast.

                              @[deprecated selfZPow_sub_natCast]
                              theorem selfZPow_sub_cast_nat {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n m : } :
                              selfZPow x B (n - m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)

                              Alias of selfZPow_sub_natCast.

                              @[simp]
                              theorem selfZPow_add {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n m : } :
                              selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
                              theorem selfZPow_mul_neg {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ) :
                              selfZPow x B d * selfZPow x B (-d) = 1
                              theorem selfZPow_neg_mul {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ) :
                              selfZPow x B (-d) * selfZPow x B d = 1
                              theorem selfZPow_pow_sub {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (a : R) (b : B) (m d : ) :
                              selfZPow x B (m - d) * IsLocalization.mk' B a 1 = b selfZPow x B m * IsLocalization.mk' B a 1 = selfZPow x B d * b
                              theorem exists_reduced_fraction' {R : Type u_3} [CommRing R] (x : R) (B : Type u_4) [CommRing B] [Algebra R B] [IsLocalization.Away x B] [IsDomain R] [WfDvdMonoid R] {b : B} (hb : b 0) (hx : Irreducible x) :
                              ∃ (a : R) (n : ), ¬x a selfZPow x B n * (algebraMap R B) a = b