mathlib documentation

ring_theory.localization.as_subring

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_is_unit_of_le {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [algebra A K] [is_fraction_ring A K] (hS : S non_zero_divisors A) (s : S) :
noncomputable def localization.map_to_fraction_ring {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [algebra A K] [is_fraction_ring A K] (B : Type u_3) [comm_ring B] [algebra A B] [is_localization S B] (hS : S non_zero_divisors A) :

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

Equations
@[simp]
theorem localization.map_to_fraction_ring_apply {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [algebra A K] [is_fraction_ring A K] {B : Type u_3} [comm_ring B] [algebra A B] [is_localization S B] (hS : S non_zero_divisors A) (b : B) :
theorem localization.mem_range_map_to_fraction_ring_iff {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [algebra A K] [is_fraction_ring A K] (B : Type u_3) [comm_ring B] [algebra A B] [is_localization S B] (hS : S non_zero_divisors A) (x : K) :
x (localization.map_to_fraction_ring K S B hS).range ∃ (a s : A) (hs : s S), x = is_localization.mk' K a s, _⟩
@[protected, instance]
@[protected, instance]
noncomputable def localization.subalgebra {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) [comm_ring K] [algebra A K] [is_fraction_ring A K] (hS : S non_zero_divisors 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 is_localization.mk' K a ⟨s, _⟩, where s ∈ S.

Equations
Instances for localization.subalgebra
@[protected, instance]
@[protected, instance]
theorem localization.subalgebra.mem_range_map_to_fraction_ring_iff_of_field {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S non_zero_divisors A) [field K] [algebra A K] [is_fraction_ring A K] (B : Type u_3) [comm_ring B] [algebra A B] [is_localization S B] (x : K) :
x (localization.map_to_fraction_ring K S B hS).range ∃ (a s : A) (hs : s S), x = (algebra_map A K) a * ((algebra_map A K) s)⁻¹
noncomputable def localization.subalgebra.of_field {A : Type u_1} (K : Type u_2) [comm_ring A] (S : submonoid A) (hS : S non_zero_divisors A) [field K] [algebra A K] [is_fraction_ring 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 algebra_map A K a * (algebra_map A K s)⁻¹ where a s : A and s ∈ S.

Equations
Instances for localization.subalgebra.of_field
@[protected, instance]
@[protected, instance]