Documentation

Mathlib.RingTheory.Localization.AsSubring

Localizations of domains as subalgebras of the fraction field. #

Given a domain A with fraction field K, and a submonoid S of A which does not contain zero, this file constructs the localization of A at S as a subalgebra of the field K over A.

theorem Localization.map_isUnit_of_le {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) [CommRing K] [Algebra A K] [IsFractionRing A K] (hS : S nonZeroDivisors A) (s : S) :
IsUnit ((algebraMap A K) s)
noncomputable def Localization.mapToFractionRing {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) [CommRing K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S nonZeroDivisors A) :

The canonical map from a localization of A at S to the fraction ring of A, given that S ≤ A⁰.

Equations
Instances For
    @[simp]
    theorem Localization.mapToFractionRing_apply {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) [CommRing K] [Algebra A K] [IsFractionRing A K] {B : Type u_3} [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S nonZeroDivisors A) (b : B) :
    theorem Localization.mem_range_mapToFractionRing_iff {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) [CommRing K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S nonZeroDivisors A) (x : K) :
    x (Localization.mapToFractionRing K S B hS).range ∃ (a : A) (s : A) (hs : s S), x = IsLocalization.mk' K a s,
    Equations
    • =
    instance Localization.isFractionRing_range_mapToFractionRing {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) [CommRing K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S nonZeroDivisors A) :
    Equations
    • =
    noncomputable def Localization.subalgebra {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) [CommRing K] [Algebra A K] [IsFractionRing A K] (hS : S nonZeroDivisors A) :

    Given a commutative ring A with fraction ring K, and a submonoid S of A which contains no zero divisor, this is the localization of A at S, considered as a subalgebra of K over A.

    The carrier of this subalgebra is defined as the set of all x : K of the form IsLocalization.mk' K a ⟨s, _⟩, where s ∈ S.

    Equations
    Instances For
      Equations
      • =
      Equations
      • =
      theorem Localization.subalgebra.mem_range_mapToFractionRing_iff_ofField {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) (hS : S nonZeroDivisors A) [Field K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [Algebra A B] [IsLocalization S B] (x : K) :
      x (Localization.mapToFractionRing K S B hS).range ∃ (a : A) (s : A) (_ : s S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
      noncomputable def Localization.subalgebra.ofField {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) (hS : S nonZeroDivisors A) [Field K] [Algebra A K] [IsFractionRing A K] :

      Given a domain A with fraction field K, and a submonoid S of A which contains no zero divisor, this is the localization of A at S, considered as a subalgebra of K over A.

      The carrier of this subalgebra is defined as the set of all x : K of the form algebraMap A K a * (algebraMap A K s)⁻¹ where a s : A and s ∈ S.

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