English
Under GoingDown, there exists a prime P between p and Q lying over p with P ≤ Q.
Русский
В условиях GoingDown существует простая P между p и Q, лежащая над p и удовлетворяющая P ≤ Q.
LaTeX
$$$\forall R,S\,[R,S\text{ комм кольца}]\; [\text{Algebra HasGoingDown}]\; (P,Q: \text{Ideal } R) (Q: \text{Ideal } S) \Rightarrow \exists P \le Q, P.IsPrime \land P.LiesOver p.$$$
Lean4
/-- Let `P` be an ideal in `R[x]`. The map
`R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))`
is injective.
-/
theorem injective_quotient_le_comap_map (P : Ideal R[X]) :
Function.Injective <|
Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)
(Polynomial.mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X])))) le_comap_map :=
by
refine quotientMap_injective' (le_of_eq ?_)
rw [comap_map_of_surjective (mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
(map_surjective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))) Ideal.Quotient.mk_surjective)]
refine le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)
refine fun p hp => polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_
simpa only [coeff_map, coe_mapRingHom] using ext_iff.mp (Ideal.mem_bot.mp (mem_comap.mp hp)) n
