Theorems · Theorem · commutative algebra

Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime

∀ {R : Type u} [inst : CommRing R] (P : Ideal R) [inst_1 : P.IsPrime] (p : Polynomial R)
  (f g : Polynomial P.ResidueField),
  p.Monic →
    f.Monic →
      g.Monic →
        Polynomial.map (algebraMap R P.ResidueField) p = f * g →
          IsCoprime f g →
            ∃ R' x x_1,
              ∃ (_ : Algebra.Etale R R'),
                ∃ Q,
                  ∃ (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P),
                    ∃ f' g',
                      Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) ∧
                        f'.Monic ∧
                          g'.Monic ∧
                            Polynomial.map (algebraMap R R') p = f' * g' ∧
                              IsCoprime f' g' ∧
                                Polynomial.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom f =
                                    Polynomial.map (algebraMap R' Q.ResidueField) f' ∧
                                  Polynomial.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom g =
                                    Polynomial.map (algebraMap R' Q.ResidueField) g'

If a monic polynomial p : R[X] factors into a product of coprime monic polynomials p = f * g in the residue field κ(P) of some P : Spec R, then there exists an etale algebra R' of R and a prime Q of R' lying over P, such that κ(P) = κ(Q) and that the factorization lifts to R'.

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

1 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIdeal.IsPrime