HenselianLocalRing.forall_exists_monic_dvd_eval_of_prime_of_not_associated
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_forall_exists_monic_dvd_eval_of_prime_of_not_associated
open IsLocalRingLean source · statement
theorem _root_.HenselianLocalRing.forall_exists_monic_dvd_eval_of_prime_of_not_associated
{A : Type*} [CommRing A] [IsNoetherianRing A] [HenselianLocalRing A]
(ϖ : A) (hϖ : maximalIdeal A = Ideal.span {ϖ})
{S : Type*} [CommRing S] [IsLocalRing S] [IsNoetherianRing S]
(φ : Polynomial A →+* S) (hφf : φ.EssFiniteType)
(hm : maximalIdeal S = Ideal.span {φ (Polynomial.C ϖ), φ Polynomial.X})
(hprime : Prime (φ (Polynomial.C ϖ)))
(χ₀ : S →+* ResidueField A) (hχ₀ : RingHom.ker χ₀ = maximalIdeal S)
(hχ₀C : ∀ a : A, χ₀ (φ (Polynomial.C a)) = IsLocalRing.residue A a) :
∀ p : S, Prime p → ¬ Associated p (φ (Polynomial.C ϖ)) →
∀ x : S, ∃ r : Polynomial A, r.Monic ∧ p ∣ (r.map (φ.comp Polynomial.C)).eval x