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

@[inline, reducible]
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.

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.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.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) :
        @[simp]
        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)) :
        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
          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
            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_isUnit_of_bijective {R : Type u_4} (S : Type u_5) [CommRing R] [CommRing S] [Algebra R S] {r : R} (hr : IsUnit r) (H : Function.Bijective (algebraMap R S)) :
                @[inline, reducible]
                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
                  @[inline, reducible]
                  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
                    noncomputable def selfZPow {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing 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} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : } (hn : 0 n) :
                      selfZPow x B n = (algebraMap R B) x ^ Int.natAbs n
                      @[simp]
                      theorem selfZPow_coe_nat {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing 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} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] :
                      selfZPow x B 0 = 1
                      theorem selfZPow_of_neg {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : } (hn : n < 0) :
                      theorem selfZPow_of_nonpos {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : } (hn : n 0) :
                      @[simp]
                      theorem selfZPow_neg_coe_nat {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] (d : ) :
                      @[simp]
                      theorem selfZPow_sub_cast_nat {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing B] [Algebra R B] [IsLocalization.Away x B] {n : } {m : } :
                      selfZPow x B (n - m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)
                      @[simp]
                      theorem selfZPow_add {R : Type u_1} [CommRing R] (x : R) (B : Type u_2) [CommRing 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} [CommRing R] (x : R) (B : Type u_2) [CommRing 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} [CommRing R] (x : R) (B : Type u_2) [CommRing 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} [CommRing R] (x : R) (B : Type u_2) [CommRing 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_1} [CommRing R] (x : R) (B : Type u_2) [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