# mathlib3documentation

ring_theory.localization.integral

# Integral and algebraic elements of a fraction field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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] [ S] [ S] (p : polynomial S) (i : ) :
R

coeff_integer_normalization p gives the coefficients of the polynomial integer_normalization p

Equations
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] [ S] [ S] (p : polynomial S) (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] [ S] [ S] (p : polynomial S) (i : ) (h : 0) :
noncomputable def is_localization.integer_normalization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) :

integer_normalization g normalizes g to have integer coefficients by clearing the denominators

Equations
@[simp]
theorem is_localization.integer_normalization_coeff {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) (i : ) :
theorem is_localization.integer_normalization_spec {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (p : polynomial S) :
(b : M), (i : ), S) = 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] [ S] [ S] (p : polynomial S) :
(b : M), = 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] [ S] [ S] {R' : Type u_4} [comm_ring R'] (g : S →+* R') (p : polynomial S) {x : R'} (hx : 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] [ S] [ S] {R' : Type u_4} [comm_ring R'] [ R'] [ R'] [ R'] (p : polynomial S) {x : R'} (hx : 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] [ K] [ K] {p : polynomial K} :
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] [ K] [ K] [comm_ring C] [ C] [ C] [ C] {x : C} :
x 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] [ K] [ K] [comm_ring C] [ C] [ C] [ 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 : polynomial R) (hf : p = 0) (M : submonoid R) (hM : p.leading_coeff M) {Rₘ : Type u_3} {Sₘ : Type u_4} [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] :
f _).is_integral_elem ( 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] [ S] {Rₘ : Type u_4} {Sₘ : Type u_5} [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] {x : S} (p : polynomial R) (hp : p = 0) (hM : p.leading_coeff M) :
S) _).is_integral_elem ( 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] [ S] {Rₘ : Type u_4} {Sₘ : Type u_5} [comm_ring Rₘ] [comm_ring Sₘ] [ Rₘ] [ Rₘ] [ Sₘ] [ Sₘ] (H : S) :

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) :
theorem is_localization.scale_roots_common_denom_mem_lifts {R : Type u_1} [comm_ring R] (M : submonoid R) {Rₘ : Type u_4} [comm_ring Rₘ] [ Rₘ] [ Rₘ] (p : polynomial Rₘ) (hp : p.leading_coeff Rₘ).range) :
theorem is_integral.exists_multiple_integral_of_is_localization {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] {Rₘ : Type u_4} [comm_ring Rₘ] [ Rₘ] [ Rₘ] [algebra Rₘ S] [ Rₘ S] (x : S) (hx : x) :
(m : M), (m x)
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] [ L] (C : Type u_7) [comm_ring C] [is_domain C] [ L] [ L] [ C] [ L] (alg : L) (inj : (x : A), L) x = 0 x = 0) :

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] [ K] [ L] [ K] (C : Type u_7) [comm_ring C] [is_domain C] [ L] [ L] [ C] [ L] [ L] [ L] [ 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] [ L] (alg : L) (inj : (x : A), L) x = 0 x = 0) :

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] [ K] [ K] [ L] [ L] [ 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] [ S] (K : Type u_5) [field K] [is_domain R] [is_domain S] [ K] [ K] [ K] [ 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] [ S] {K : Type u_5} {L : Type u_3} [is_domain R] [is_domain S] [field K] [field L] [ K] [ L] [ L] [ L] [ L] [ L] [ L] [ L] {a : S} {b : set S} (alg : L) (inj : function.injective L)) (h : (ideal.span {a}) b)) :
(ideal.span { L) a}) ( 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.