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.

source
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)
source
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) :
B →ₐ[A] K

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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) :
    (Localization.mapToFractionRing K S B hS) b = (IsLocalization.lift (_ : ∀ (s : ↥S), IsUnit ((algebraMap A K) ↑s))) b
    source
    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 ∈ AlgHom.range (Localization.mapToFractionRing K S B hS) ↔ ∃ (a : A) (s : A) (hs : s ∈ S), x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ nonZeroDivisors A) }
    source
    instance Localization.isLocalization_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) :
    IsLocalization S ↥(AlgHom.range (Localization.mapToFractionRing K S B hS))
    Equations
    source
    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) :
    IsFractionRing (↥(AlgHom.range (Localization.mapToFractionRing K S B hS))) K
    Equations
    source
    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) :
    Subalgebra A K

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Localization.subalgebra.isLocalization_subalgebra {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [CommRing K] [Algebra A K] [IsFractionRing A K] :
      IsLocalization S ↥(Localization.subalgebra K S hS)
      Equations
      source
      instance Localization.subalgebra.isFractionRing {A : Type u_1} (K : Type u_2) [CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [CommRing K] [Algebra A K] [IsFractionRing A K] :
      IsFractionRing (↥(Localization.subalgebra K S hS)) K
      Equations
      source
      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 ∈ AlgHom.range (Localization.mapToFractionRing K S B hS) ↔ ∃ (a : A) (s : A) (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
      source
      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] :
      Subalgebra 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
        source
        instance Localization.subalgebra.isLocalization_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] :
        IsLocalization S ↥(Localization.subalgebra.ofField K S hS)
        Equations
        source
        instance Localization.subalgebra.isFractionRing_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] :
        IsFractionRing (↥(Localization.subalgebra.ofField K S hS)) K
        Equations