Localizations of domains as subalgebras of the fraction field. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) :
is_unit (⇑(algebra_map A K) ↑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⁰.
@[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) :
⇑(localization.map_to_fraction_ring K S B hS) b = ⇑(is_localization.lift _) 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]
def
localization.is_localization_range_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) :
is_localization S ↥((localization.map_to_fraction_ring K S B hS).range)
@[protected, instance]
def
localization.is_fraction_ring_range_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) :
is_fraction_ring ↥((localization.map_to_fraction_ring K S B hS).range) K
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) :
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
is_localization.mk' K a ⟨s, _⟩, where s ∈ S.
Equations
- localization.subalgebra K S hS = (localization.map_to_fraction_ring K S (localization S) hS).range.copy {x : K | ∃ (a s : A) (hs : s ∈ S), x = is_localization.mk' K a ⟨s, _⟩} _
Instances for ↥localization.subalgebra
@[protected, instance]
def
localization.subalgebra.is_localization_subalgebra
{A : Type u_1}
(K : Type u_2)
[comm_ring A]
(S : submonoid A)
(hS : S ≤ non_zero_divisors A)
[comm_ring K]
[algebra A K]
[is_fraction_ring A K] :
is_localization S ↥(localization.subalgebra K S hS)
@[protected, instance]
def
localization.subalgebra.is_fraction_ring
{A : Type u_1}
(K : Type u_2)
[comm_ring A]
(S : submonoid A)
(hS : S ≤ non_zero_divisors A)
[comm_ring K]
[algebra A K]
[is_fraction_ring A K] :
is_fraction_ring ↥(localization.subalgebra K S hS) K
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] :
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
algebra_map A K a * (algebra_map A K s)⁻¹ where a s : A and s ∈ S.
Equations
- localization.subalgebra.of_field K S hS = (localization.map_to_fraction_ring K S (localization S) hS).range.copy {x : K | ∃ (a s : A) (hs : s ∈ S), x = ⇑(algebra_map A K) a * (⇑(algebra_map A K) s)⁻¹} _
Instances for ↥localization.subalgebra.of_field
@[protected, instance]
def
localization.subalgebra.is_localization_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] :
is_localization S ↥(localization.subalgebra.of_field K S hS)
@[protected, instance]
def
localization.subalgebra.is_fraction_ring_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] :