Universal factorization ring

Let R be a commutative ring and p : R[X] be monic of degree n and let n = m + k. We construct the universal ring of the following functors on R-Alg:

• S ↦ "monic polynomials over S of degree n": Represented by R[X₁,...,Xₙ]. See MvPolynomial.mapEquivMonic.
• S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S": Represented by an R-algebra (Polynomial.UniversalFactorizationRing) that is finitely-presented as an R-module. See Polynomial.UniversalFactorizationRing.homEquiv.
• S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S": Represented by an etale R-algebra (Polynomial.UniversalCoprimeFactorizationRing). See Polynomial.UniversalCoprimeFactorizationRing.homEquiv.

def Polynomial.freeMonic (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial (MvPolynomial (Fin n) R)

The free monic polynomial of degree n, as a polynomial in R[X₁,...,Xₙ][X].

theorem Polynomial.coeff_freeMonic (R : Type u_1) [CommRing R] (n k : ℕ) : (freeMonic R n).coeff k = if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

theorem Polynomial.degree_freeMonic (R : Type u_1) [CommRing R] (n : ℕ) [Nontrivial R] : (freeMonic R n).degree = ↑n

theorem Polynomial.natDegree_freeMonic (R : Type u_1) [CommRing R] (n : ℕ) [Nontrivial R] : (freeMonic R n).natDegree = n

theorem Polynomial.monic_freeMonic (R : Type u_1) [CommRing R] (n : ℕ) : (freeMonic R n).Monic

theorem Polynomial.map_map_freeMonic (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] (n : ℕ) (f : R →+* S) : map (MvPolynomial.map f) (freeMonic R n) = freeMonic S n

def Polynomial.MonicDegreeEq.freeMonic (R : Type u_1) [CommRing R] (n : ℕ) : MonicDegreeEq (MvPolynomial (Fin n) R) n

The free monic polynomial of degree n, as a MonicDegreeEq in R[X₁,...,Xₙ][X].

@[simp]

theorem Polynomial.MonicDegreeEq.freeMonic_coe (R : Type u_1) [CommRing R] (n : ℕ) : ↑(freeMonic R n) = Polynomial.freeMonic R n

def MvPolynomial.mapEquivMonic (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) : (MvPolynomial (Fin n) R →ₐ[R] S) ≃ Polynomial.MonicDegreeEq S n

MonicDegreeEq · n is representable by R[X₁,...,Xₙ], with the universal element being freeMonic.

theorem MvPolynomial.coe_mapEquivMonic_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S) (g : S →ₐ[R] T) : ↑((mapEquivMonic R T n) (g.comp f)) = Polynomial.map ↑g ↑((mapEquivMonic R S n) f)

theorem MvPolynomial.coe_mapEquivMonic_comp' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S) (g : S →ₐ[R] T) : (mapEquivMonic R T n) (g.comp f) = ((mapEquivMonic R S n) f).map ↑g

theorem MvPolynomial.mapEquivMonic_symm_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (p : Polynomial.MonicDegreeEq S n) (g : S →ₐ[R] T) : (mapEquivMonic R T n).symm (p.map ↑g) = g.comp ((mapEquivMonic R S n).symm p)

theorem MvPolynomial.mapEquivMonic_symm_map_algebraMap {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (p : Polynomial.MonicDegreeEq S n) [Algebra S T] [IsScalarTower R S T] : (mapEquivMonic R T n).symm (p.map (algebraMap S T)) = (IsScalarTower.toAlgHom R S T).comp ((mapEquivMonic R S n).symm p)

def MvPolynomial.universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : MvPolynomial (Fin n) R →ₐ[R] TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)

In light of the fact that MonicDegreeEq · n is representable by R[X₁,...,Xₙ], this is the map R[X₁,...,Xₘ₊ₖ] → R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₖ] corresponding to the multiplication MonicDegreeEq · m × MonicDegreeEq · k → MonicDegreeEq · (m + k).

theorem MvPolynomial.universalFactorizationMap_freeMonic (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : Polynomial.map (↑(universalFactorizationMap R n m k hn)) (Polynomial.freeMonic R n) = Polynomial.map (algebraMap (MvPolynomial (Fin m) R) (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R))) (Polynomial.freeMonic R m) * Polynomial.map (↑Algebra.TensorProduct.includeRight) (Polynomial.freeMonic R k)

theorem MvPolynomial.universalFactorizationMap_comp_map (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMap S n m k hn).comp (map (algebraMap R S)) = (Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S))) ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S))) ⋯).comp (universalFactorizationMap R n m k hn).toRingHom

def MvPolynomial.universalFactorizationMapLiftEquiv (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq S n) : { f : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R) →ₐ[R] S // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p } ≃ { q : Polynomial.MonicDegreeEq S m × Polynomial.MonicDegreeEq S k // ↑q.1 * ↑q.2 = ↑p }

Lifts along universalFactorizationMap corresponds to factorization of p into monic polynomials with fixed degrees.

theorem MvPolynomial.ker_eval₂Hom_universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : RingHom.ker (eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) fun (x : Fin k) => 1 ⊗ₜ[R] X x)) = Ideal.span (Set.range fun (i : Fin n) => C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

def MvPolynomial.universalFactorizationMapPresentation (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) (Fin m ⊕ Fin k) (Fin n)

The canonical presentation of universalFactorizationMap.

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_relation (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin n) : (universalFactorizationMapPresentation R n m k hn).relation i = C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i)))

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_algebra_smul (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (c : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (x : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) : SMul.smul c x = (aeval (Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) fun (x : Fin k) => 1 ⊗ₜ[R] X x)).toRingHom c * x

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_σ' (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (f : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) : (universalFactorizationMapPresentation R n m k hn).σ' f = (map C) ((tensorEquivSum R (Fin m) (Fin k) R) f)

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : Algebra.algebraMap = (aeval (Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) fun (x : Fin k) => 1 ⊗ₜ[R] X x)).toRingHom

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_map (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (a✝ : Fin n) : (universalFactorizationMapPresentation R n m k hn).map a✝ = (⇑finSumFinEquiv.symm ∘ ⇑(finCongr hn)) a✝

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_val (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (a✝ : Fin m ⊕ Fin k) : (universalFactorizationMapPresentation R n m k hn).val a✝ = Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) (fun (x : Fin k) => 1 ⊗ₜ[R] X x) a✝

theorem MvPolynomial.pderiv_inl_universalFactorizationMap_X (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin m) (j : Fin n) : (pderiv (Sum.inl i)) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X j))) = if ↑j < ↑i then 0 else if h : ↑j - ↑i < k then X (Sum.inr ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = k then 1 else 0

theorem MvPolynomial.pderiv_inr_universalFactorizationMap_X (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin k) (j : Fin n) : (pderiv (Sum.inr i)) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X j))) = if ↑j < ↑i then 0 else if h : ↑j - ↑i < m then X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0

theorem MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMapPresentation R n m k hn).jacobiMatrix = -((Matrix.reindex (finCongr ⋯) (finCongr ⋯)) ((Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)).toRingHom (Polynomial.freeMonic R m)).sylvester (Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)).toRingHom (Polynomial.freeMonic R k)) m k)).transpose

theorem MvPolynomial.universalFactorizationMapPresentation_jacobian (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMapPresentation R n m k hn).jacobian = (-1) ^ n * (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (Polynomial.freeMonic R m)).resultant (Polynomial.map Algebra.TensorProduct.includeRight.toRingHom (Polynomial.freeMonic R k))

theorem MvPolynomial.finitePresentation_universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMap R n m k hn).FinitePresentation

theorem MvPolynomial.finite_universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMap R n m k hn).Finite

def Polynomial.UniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Type u_1

The universal factorization ring of a monic polynomial p of degree n. This is the representing object of the functor S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S". See UniversalFactorizationRing.homEquiv.

instance Polynomial.instCommRingUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : CommRing (UniversalFactorizationRing m k hn p)

instance Polynomial.instAlgebraUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Algebra R (UniversalFactorizationRing m k hn p)

def Polynomial.UniversalFactorizationRing.fromTensor {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R) →ₐ[R] UniversalFactorizationRing m k hn p

The canonical map R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₙ] → UniversalFactorizationRing.

def Polynomial.UniversalFactorizationRing.monicDegreeEq {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalFactorizationRing m k hn p) n

The image of p in the universal factorization ring of p.

@[simp]

theorem Polynomial.UniversalFactorizationRing.monicDegreeEq_coe {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : ↑(monicDegreeEq m k hn p) = map (algebraMap R (UniversalFactorizationRing m k hn p)) ↑p

theorem Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) = (Algebra.ofId R (UniversalFactorizationRing m k hn p)).comp ((MvPolynomial.mapEquivMonic R R n).symm p)

theorem Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap' {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) = (MvPolynomial.mapEquivMonic R (UniversalFactorizationRing m k hn p) n).symm (monicDegreeEq m k hn p)

def Polynomial.UniversalFactorizationRing.factor₁ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalFactorizationRing m k hn p) m

The first factor of p in the universal factorization ring of p.

def Polynomial.UniversalFactorizationRing.factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalFactorizationRing m k hn p) k

The second factor of p in the universal factorization ring of p.

theorem Polynomial.UniversalFactorizationRing.factor₁_mul_factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : ↑(factor₁ m k hn p) * ↑(factor₂ m k hn p) = ↑(monicDegreeEq m k hn p)

def Polynomial.UniversalFactorizationRing.homEquiv {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (UniversalFactorizationRing m k hn p →ₐ[R] S) ≃ { q : MonicDegreeEq S m × MonicDegreeEq S k // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p }

The universal factorization ring represents S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S".

instance Polynomial.instFiniteUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Module.Finite R (UniversalFactorizationRing m k hn p)

instance Polynomial.instFinitePresentationUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Algebra.FinitePresentation R (UniversalFactorizationRing m k hn p)

def Polynomial.UniversalFactorizationRing.presentation {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Algebra.PreSubmersivePresentation R (UniversalFactorizationRing m k hn p) (Fin m ⊕ Fin k) (Fin n)

The presentation of UniversalFactorizationRing. Its jacobian is the resultant of the two factors (up to sign).

theorem Polynomial.UniversalFactorizationRing.jacobian_resentation {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

@[reducible, inline]

abbrev Polynomial.UniversalCoprimeFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Type u_1

The universal coprime factorization ring of a monic polynomial p of degree n. This is the representing object of the functor S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S". See UniversalCoprimeFactorizationRing.homEquiv.

def Polynomial.UniversalCoprimeFactorizationRing.factor₁ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalCoprimeFactorizationRing m k hn p) m

The first factor of p in the universal coprime factorization ring of p.

def Polynomial.UniversalCoprimeFactorizationRing.factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalCoprimeFactorizationRing m k hn p) k

The second factor of p in the universal coprime factorization ring of p.

theorem Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : ↑(factor₁ m k hn p) * ↑(factor₂ m k hn p) = ↑(p.map (algebraMap R (UniversalCoprimeFactorizationRing m k hn p)))

theorem Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : IsCoprime ↑(factor₁ m k hn p) ↑(factor₂ m k hn p)

instance Polynomial.instEtaleUniversalCoprimeFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Algebra.Etale R (UniversalCoprimeFactorizationRing m k hn p)

def Polynomial.UniversalCoprimeFactorizationRing.homEquiv {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) ≃ { q : MonicDegreeEq S m × MonicDegreeEq S k // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }

The universal factorization ring represents S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S".

theorem Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) {T : Type u_4} [CommRing T] [Algebra R T] (f : UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) (g : S →ₐ[R] T) : (↑((homEquiv T m k hn p) (g.comp f))).1 = (↑((homEquiv S m k hn p) f)).1.map ↑g

theorem Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) {T : Type u_4} [CommRing T] [Algebra R T] (f : UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) (g : S →ₐ[R] T) : (↑((homEquiv T m k hn p) (g.comp f))).2 = (↑((homEquiv S m k hn p) f)).2.map ↑g

theorem Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) (P : Ideal R) [P.IsPrime] (f : MonicDegreeEq P.ResidueField m) (g : MonicDegreeEq P.ResidueField k) (H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g) (Hpq : IsCoprime ↑f ↑g) : ∃ (Q : Ideal (UniversalCoprimeFactorizationRing m k hn p)) (x : Q.IsPrime) (x_1 : Q.LiesOver P), Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R (UniversalCoprimeFactorizationRing m k hn p)) ⋯) ∧ f.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R (UniversalCoprimeFactorizationRing m k hn p)) ⋯).toRingHom = (factor₁ m k hn p).map (algebraMap (UniversalCoprimeFactorizationRing m k hn p) Q.ResidueField) ∧ g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R (UniversalCoprimeFactorizationRing m k hn p)) ⋯).toRingHom = (factor₂ m k hn p).map (algebraMap (UniversalCoprimeFactorizationRing m k hn p) Q.ResidueField)

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 Q : Spec R_univ in the universal coprime factorization ring lying over P, such that κ(P) = κ(Q) and f and g are the image of the universal factors.

theorem Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime {R : Type u} [CommRing R] (P : Ideal R) [P.IsPrime] (p : Polynomial R) (f g : Polynomial P.ResidueField) (hp : p.Monic) (hf : f.Monic) (hg : g.Monic) (H : Polynomial.map (algebraMap R P.ResidueField) p = f * g) (Hpq : IsCoprime f g) : ∃ (R' : Type u) (x : CommRing R') (x_1 : Algebra R R') (_ : Etale R R') (Q : Ideal R') (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P) (f' : Polynomial R') (g' : Polynomial R'), Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (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 (ofId R R') ⋯).toRingHom f = Polynomial.map (algebraMap R' Q.ResidueField) f' ∧ Polynomial.map (Ideal.ResidueField.mapₐ P Q (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'.