IsLocalRing.exists_monic_coeff_mem_maximalIdeal_aeval_mem_span_of_pow_mem
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_exists_monic_coeff_mem_maximalIdeal_aeval_mem_span_of_pow_mem
open IsLocalRing PolynomialLean source · statement
theorem _root_.IsLocalRing.exists_monic_coeff_mem_maximalIdeal_aeval_mem_span_of_pow_mem
{A S : Type*} [CommRing A] [IsLocalRing A] [CommRing S] [Algebra A S]
(h T : S) [Module.Finite A (S ⧸ Ideal.span ({h} : Set S))]
(hnil : ∃ k : ℕ, (Ideal.Quotient.mk (Ideal.span ({h} : Set S)) T) ^ k ∈
(maximalIdeal A).map (algebraMap A (S ⧸ Ideal.span ({h} : Set S)))) :
∃ P : Polynomial A, P.Monic ∧ (∀ i : ℕ, i < P.natDegree → P.coeff i ∈ maximalIdeal A) ∧
Polynomial.aeval T P ∈ Ideal.span ({h} : Set S)