mathlib documentation

ring_theory.localization.integral

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 : polynomial S) (i : ) :
R

coeff_integer_normalization p gives the coefficients of the polynomial integer_normalization p

Equations
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 : polynomial S) :

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

Equations
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 : polynomial S) :
∃ (b : M), ∀ (i : ), (algebra_map R S) ((is_localization.integer_normalization M p).coeff i) = b p.coeff i
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 : polynomial S) {x : R'} (hx : polynomial.eval₂ g x 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 : polynomial S) {x : R'} (hx : (polynomial.aeval x) 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} :

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 : polynomial R) (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ₘ] :
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 : polynomial R) (hp : (polynomial.aeval x) p = 0) (hM : p.leading_coeff M) :

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) :

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_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 = 0x = 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] [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] :

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 = 0x = 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] [algebra A K] [is_fraction_ring A K] [algebra A L] [algebra K L] [is_scalar_tower A K L] [finite_dimensional K 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)) :

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.