Integral and algebraic elements of a fraction field #
Implementation notes #
See src/ring_theory/localization/basic.lean for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
noncomputable
def
is_localization.coeff_integer_normalization
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X])
(i : ℕ) :
R
coeff_integer_normalization p gives the coefficients of the polynomial
integer_normalization p
Equations
- is_localization.coeff_integer_normalization M p i = dite (i ∈ p.support) (λ (hi : i ∈ p.support), classical.some _) (λ (hi : i ∉ p.support), 0)
theorem
is_localization.coeff_integer_normalization_of_not_mem_support
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X])
(i : ℕ)
(h : p.coeff i = 0) :
theorem
is_localization.coeff_integer_normalization_mem_support
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X])
(i : ℕ)
(h : is_localization.coeff_integer_normalization M p i ≠ 0) :
noncomputable
def
is_localization.integer_normalization
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X]) :
R[X]
integer_normalization g normalizes g to have integer coefficients
by clearing the denominators
Equations
- is_localization.integer_normalization M p = ∑ (i : ℕ) in p.support, ⇑(polynomial.monomial i) (is_localization.coeff_integer_normalization M p i)
@[simp]
theorem
is_localization.integer_normalization_coeff
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X])
(i : ℕ) :
theorem
is_localization.integer_normalization_spec
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X]) :
∃ (b : ↥M), ∀ (i : ℕ), ⇑(algebra_map R S) ((is_localization.integer_normalization M p).coeff i) = ↑b • p.coeff i
theorem
is_localization.integer_normalization_map_to_map
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(p : S[X]) :
∃ (b : ↥M), polynomial.map (algebra_map R S) (is_localization.integer_normalization M p) = ↑b • p
theorem
is_localization.integer_normalization_eval₂_eq_zero
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
{R' : Type u_4}
[comm_ring R']
(g : S →+* R')
(p : S[X])
{x : R'}
(hx : polynomial.eval₂ g x p = 0) :
polynomial.eval₂ (g.comp (algebra_map R S)) x (is_localization.integer_normalization M p) = 0
theorem
is_localization.integer_normalization_aeval_eq_zero
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
{R' : Type u_4}
[comm_ring R']
[algebra R R']
[algebra S R']
[is_scalar_tower R S R']
(p : S[X])
{x : R'}
(hx : ⇑(polynomial.aeval x) p = 0) :
⇑(polynomial.aeval x) (is_localization.integer_normalization M p) = 0
theorem
is_fraction_ring.integer_normalization_eq_zero_iff
{A : Type u_4}
{K : Type u_5}
[comm_ring A]
[is_domain A]
[field K]
[algebra A K]
[is_fraction_ring A K]
{p : K[X]} :
is_localization.integer_normalization A⁰ p = 0 ↔ p = 0
theorem
is_fraction_ring.is_algebraic_iff
(A : Type u_4)
(K : Type u_5)
(C : Type u_6)
[comm_ring A]
[is_domain A]
[field K]
[algebra A K]
[is_fraction_ring A K]
[comm_ring C]
[algebra A C]
[algebra K C]
[is_scalar_tower A K C]
{x : C} :
is_algebraic A x ↔ is_algebraic K x
An element of a ring is algebraic over the ring A iff it is algebraic
over the field of fractions of A.
theorem
is_fraction_ring.comap_is_algebraic_iff
{A : Type u_4}
{K : Type u_5}
{C : Type u_6}
[comm_ring A]
[is_domain A]
[field K]
[algebra A K]
[is_fraction_ring A K]
[comm_ring C]
[algebra A C]
[algebra K C]
[is_scalar_tower A K C] :
A ring is algebraic over the ring A iff it is algebraic over the field of fractions of A.
theorem
ring_hom.is_integral_elem_localization_at_leading_coeff
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(x : S)
(p : R[X])
(hf : polynomial.eval₂ f x p = 0)
(M : submonoid R)
(hM : p.leading_coeff ∈ M)
{Rₘ : Type u_3}
{Sₘ : Type u_4}
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (submonoid.map ↑f M) Sₘ] :
(is_localization.map Sₘ f _).is_integral_elem (⇑(algebra_map S Sₘ) x)
theorem
is_integral_localization_at_leading_coeff
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
{Rₘ : Type u_4}
{Sₘ : Type u_5}
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
{x : S}
(p : R[X])
(hp : ⇑(polynomial.aeval x) p = 0)
(hM : p.leading_coeff ∈ M) :
(is_localization.map Sₘ (algebra_map R S) _).is_integral_elem (⇑(algebra_map S Sₘ) x)
Given a particular witness to an element being algebraic over an algebra R → S,
We can localize to a submonoid containing the leading coefficient to make it integral.
Explicitly, the map between the localizations will be an integral ring morphism
theorem
is_integral_localization
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
{Rₘ : Type u_4}
{Sₘ : Type u_5}
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
(H : algebra.is_integral R S) :
(is_localization.map Sₘ (algebra_map R S) _).is_integral
If R → S is an integral extension, M is a submonoid of R,
Rₘ is the localization of R at M,
and Sₘ is the localization of S at the image of M under the extension map,
then the induced map Rₘ → Sₘ is also an integral extension
theorem
is_integral_localization'
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
{f : R →+* S}
(hf : f.is_integral)
(M : submonoid R) :
(is_localization.map (localization (submonoid.map ↑f M)) f _).is_integral
theorem
is_integral_closure.is_fraction_ring_of_algebraic
(A : Type u_4)
[comm_ring A]
[is_domain A]
{L : Type u_6}
[field L]
[algebra A L]
(C : Type u_7)
[comm_ring C]
[is_domain C]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
(alg : algebra.is_algebraic A L)
(inj : ∀ (x : A), ⇑(algebra_map A L) x = 0 → x = 0) :
is_fraction_ring C L
If the field L is an algebraic extension of the integral domain A,
the integral closure C of A in L has fraction field L.
theorem
is_integral_closure.is_fraction_ring_of_finite_extension
(A : Type u_4)
(K : Type u_5)
[comm_ring A]
[is_domain A]
(L : Type u_6)
[field K]
[field L]
[algebra A K]
[algebra A L]
[is_fraction_ring A K]
(C : Type u_7)
[comm_ring C]
[is_domain C]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[algebra K L]
[is_scalar_tower A K L]
[finite_dimensional K L] :
is_fraction_ring C L
If the field L is a finite extension of the fraction field of the integral domain A,
the integral closure C of A in L has fraction field L.
theorem
integral_closure.is_fraction_ring_of_algebraic
{A : Type u_4}
[comm_ring A]
[is_domain A]
{L : Type u_6}
[field L]
[algebra A L]
(alg : algebra.is_algebraic A L)
(inj : ∀ (x : A), ⇑(algebra_map A L) x = 0 → x = 0) :
is_fraction_ring ↥(integral_closure A L) L
If the field L is an algebraic extension of the integral domain A,
the integral closure of A in L has fraction field L.
theorem
integral_closure.is_fraction_ring_of_finite_extension
{A : Type u_4}
(K : Type u_5)
[comm_ring A]
[is_domain A]
(L : Type u_6)
[field K]
[field L]
[algebra A K]
[is_fraction_ring A K]
[algebra A L]
[algebra K L]
[is_scalar_tower A K L]
[finite_dimensional K L] :
is_fraction_ring ↥(integral_closure A L) L
If the field L is a finite extension of the fraction field of the integral domain A,
the integral closure of A in L has fraction field L.
theorem
is_fraction_ring.is_algebraic_iff'
(R : Type u_1)
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
(K : Type u_5)
[field K]
[is_domain R]
[is_domain S]
[algebra R K]
[algebra S K]
[no_zero_smul_divisors R K]
[is_fraction_ring S K]
[is_scalar_tower R S K] :
S is algebraic over R iff a fraction ring of S is algebraic over R
theorem
is_fraction_ring.ideal_span_singleton_map_subset
(R : Type u_1)
[comm_ring R]
{S : Type u_2}
[comm_ring S]
[algebra R S]
{K : Type u_5}
{L : Type u_3}
[is_domain R]
[is_domain S]
[field K]
[field L]
[algebra R K]
[algebra R L]
[algebra S L]
[is_integral_closure S R L]
[is_fraction_ring S L]
[algebra K L]
[is_scalar_tower R S L]
[is_scalar_tower R K L]
{a : S}
{b : set S}
(alg : algebra.is_algebraic R L)
(inj : function.injective ⇑(algebra_map R L))
(h : ↑(ideal.span {a}) ⊆ ↑(submodule.span R b)) :
↑(ideal.span {⇑(algebra_map S L) a}) ⊆ ↑(submodule.span K (⇑(algebra_map S L) '' b))
If the S-multiples of a are contained in some R-span, then Frac(S)-multiples of a
are contained in the equivalent Frac(R)-span.