# 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

- Localization.mapToFractionRing K S B hS = { toRingHom := IsLocalization.lift ⋯, commutes' := ⋯ }

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) :
(mapToFractionRing K S B hS) b = (IsLocalization.lift ⋯) 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 ∈ (mapToFractionRing K S B hS).range ↔ ∃ (a : A) (s : A) (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩
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 ↥(mapToFractionRing K S B hS).range
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 (↥(mapToFractionRing K S B hS).range) K
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

- Localization.subalgebra K S hS = (Localization.mapToFractionRing K S (Localization S) hS).range.copy {x : K | ∃ (a : A) (s : A) (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩} ⋯

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 ↥(subalgebra K S hS)
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 (↥(subalgebra K S hS)) K
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 ∈ (mapToFractionRing K S B hS).range ↔ ∃ (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
theorem Localization.subalgebra.ofField_eq {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] :
ofField K S hS = subalgebra K S hS
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 ↥(ofField K S hS)
source
instance Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (S : Subalgebra A K) :
IsFractionRing (↥S) K
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 (↥(ofField K S hS)) K