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) : 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' := ⋯ }

@[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

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, ⋯⟩

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

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

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, ⋯⟩} ⋯

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)

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

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)⁻¹

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.

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

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)

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

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