not_dvd_differentIdeal_of_isCoprime

English

Let A and B be domains with A Dedekind and B Dedekind, and let p be a maximal ideal of A with a finite quotient A/p. Suppose P and Q are maximal ideals of B such that P and Q lie over p, are coprime, and the product P Q equals the image of p in B. Then P does not divide the different ideal of A over B.

Русский

Пусть A и B — области целых, каждая из которых Дедекиндова, пусть p — максимальная идеал в A с конечной факторной окружностью. Предположим, что P и Q — максимальные идеалы в B, лежащие над p, пара Coprime и P Q = image(p) в B. Тогда P не делит различный идеал A над B.

LaTeX

$$$\forall A K L B\, [\text{CommRing } A] [\text{Field } K] [\text{CommRing } B] [\text{Field } L] [\text{Algebra } A B] [\text{Algebra } A K] [\text{Algebra } K L] \ [\text{Algebra.IsSeparable } (\mathrm{FractionRing } A) (\mathrm{FractionRing } B)] {p : \mathsf{Ideal } A} [p. IsMaximal] [Finite (A / p)] (P Q : \mathsf{Ideal } B) [P.IsMaximal] (hPQ : IsCoprime P Q) (hP : P * Q = \mathsf{Ideal}.map (\mathrm{algebraMap } A B) p) : \neg P \mid \mathrm{differentIdeal } A B$$$

Lean4

theorem not_dvd_differentIdeal_of_isCoprime [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A}
    [p.IsMaximal] [Finite (A ⧸ p)] (P Q : Ideal B) [P.IsMaximal] (hPQ : IsCoprime P Q)
    (hP : P * Q = Ideal.map (algebraMap A B) p) : ¬P ∣ differentIdeal A B :=
  by
  have : P.LiesOver p := by
    constructor
    refine ‹p.IsMaximal›.eq_of_le ?_ ?_
    · simpa using ‹P.IsMaximal›.ne_top
    · rw [← Ideal.map_le_iff_le_comap, ← hP]
      exact Ideal.mul_le_right
  exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable A P Q hPQ hP

Похожие утверждения