Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map
theorem Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : NormalizedGCDMonoid R] {p : Polynomial R},
p.IsPrimitive → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
**Gauss's Lemma** for GCD domains states that for any commutative ring `R`, field `K`, and a polynomial `p` from the ring, given that `K` is the field of fractions of `R`, `R` is an integral domain, `R` is a normalized GCD monoid, and `p` is a primitive polynomial (meaning that the greatest common divisor of its coefficients is 1), then `p` is irreducible in `R` if and only if its image under the homomorphism induced by the integral domain structure of `R` to `K` is irreducible in `K`. In other words, the irreducibility of a primitive polynomial in an integral domain is preserved when it's mapped to its fraction field.
More concisely: A primitive polynomial in an integral domain is irreducible if and only if its image under the homomorphism to the field of fractions is an irreducible polynomial.
|
Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast
theorem Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast :
∀ {p : Polynomial ℤ}, p.IsPrimitive → (Irreducible p ↔ Irreducible (Polynomial.map (Int.castRingHom ℚ) p)) := by
sorry
**Gauss's Lemma** for integers states that, for any given primitive polynomial with integer coefficients, the polynomial is irreducible (i.e., it cannot be factored into two non-unit polynomials) if and only if it is irreducible when its coefficients are mapped to rational numbers via an integer to rational number ring homomorphism. This theorem provides a connection between the irreducibility of a polynomial in the ring of integers and the ring of rational numbers.
More concisely: Gauss's Lemma: A primitive polynomial with integer coefficients is irreducible if and only if its image under the homomorphism from the ring of integers to the field of rational numbers is an irreducible polynomial.
|
IsIntegrallyClosed.eq_map_mul_C_of_dvd
theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd :
∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst_4 : IsIntegrallyClosed R] {f : Polynomial R},
f.Monic →
∀ {g : Polynomial K},
g ∣ Polynomial.map (algebraMap R K) f →
∃ g', Polynomial.map (algebraMap R K) g' * Polynomial.C g.leadingCoeff = g
The theorem `IsIntegrallyClosed.eq_map_mul_C_of_dvd` states that for a commutative ring `R`, a field `K`, where `K` is the field of fractions of `R` and `R` is integrally closed, given a monic polynomial `f` with coefficients in `R` and any polynomial `g` from `K` that divides the polynomial obtained by mapping `f` via the ring homomorphism induced by the algebra structure of `R` in `K`, there exists another polynomial `g'` such that `g'` mapped via the same ring homomorphism times the constant polynomial of the multiplicative inverse of `g`'s leading coefficient equals `g`.
In other words, if a polynomial from `K` divides a polynomial from `R` under the mapping induced by the algebra structure, then it's possible to find another polynomial in `R` that maps to `K` and scales by the inverse of the leading coefficient of the original polynomial to equal the original polynomial.
More concisely: If `R` is an integrally closed commutative ring, and `K` is its field of fractions, then for any monic polynomial `f` in `R` and any polynomial `g` in `K` that maps `f` under the homomorphism induced by `R` in `K`, there exists a polynomial `g'` in `R` such that `g'` maps to `g` and scales by the inverse of `g`'s leading coefficient.
|
Polynomial.isIntegrallyClosed_iff'
theorem Polynomial.isIntegrallyClosed_iff' :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst_4 : IsDomain R],
IsIntegrallyClosed R ↔
∀ (p : Polynomial R), p.Monic → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
This theorem states that an integral domain `R` is integrally closed if and only if Gauss's lemma holds for all monic polynomials in `R`. Specifically, Gauss's lemma is the statement that a monic polynomial `p` in `R` is irreducible if and only if its image under the algebraic map to the field of fractions `K` of `R` is also irreducible. Here, `R` is assumed to be a commutative ring, and `K` is a field that is the field of fractions of `R`. Moreover, `R` is assumed to be an integral domain. This theorem links the property of being integrally closed with the property of irreducibility being preserved under the algebraic mapping to the field of fractions, for monic polynomials.
More concisely: A commutative integral domain R is integrally closed if and only if Gauss's lemma holds, i.e., monic polynomials in R are irreducible in R if and only if their images in the field of fractions of R are irreducible.
|
Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map
theorem Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst_4 : IsIntegrallyClosed R] {p : Polynomial R},
p.Monic → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
**Gauss's Lemma** for integrally closed domains states that for any commutative ring `R`, field `K`, where `K` is the field of fractions of `R`, and `R` is integrally closed, and for any monic polynomial `p` with coefficients in `R`, the polynomial `p` is irreducible in `R` if and only if it is irreducible in the fraction field `K`. Here, a polynomial is said to be irreducible if it cannot be factored into the product of two nontrivial polynomials. The irreducibility in the fraction field `K` is determined after mapping the polynomial `p` from `R` to `K` using the embedding given by the `Algebra` structure.
More concisely: A monic polynomial is irreducible in an integrally closed domain if and only if it is irreducible in the domain's field of fractions.
|