English
In a separable extension, coprimality gives a non-divisibility result for the different ideal.
Русский
В сепарабельном расширении взаимная простота приводит к неразделимости различного идеала.
LaTeX
$$IsCoprime(P,Q) → ¬P ∣ differentIdeal(A,B)$$
Lean4
theorem not_dvd_differentIdeal_of_isCoprime_of_isSeparable [Algebra.IsSeparable (FractionRing A) (FractionRing B)]
{p : Ideal A} [p.IsMaximal] (P Q : Ideal B) [P.IsMaximal] [P.LiesOver p] (hPQ : IsCoprime P Q)
(hP : P * Q = Ideal.map (algebraMap A B) p) [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] : ¬P ∣ differentIdeal A B :=
by
letI : Algebra (A ⧸ p) (B ⧸ Q) :=
Ideal.Quotient.algebraQuotientOfLEComap
(by
rw [← Ideal.map_le_iff_le_comap, ← hP]
exact Ideal.mul_le_left)
have : IsScalarTower A (A ⧸ p) (B ⧸ Q) := .of_algebraMap_eq' rfl
have : Module.Finite (A ⧸ p) (B ⧸ Q) := Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ Q)
letI e : (B ⧸ p.map (algebraMap A B)) ≃ₐ[A ⧸ p] ((B ⧸ P) × B ⧸ Q) :=
{ __ := (Ideal.quotEquivOfEq hP.symm).trans (Ideal.quotientMulEquivQuotientProd P Q hPQ),
commutes' := Quotient.ind fun _ ↦ rfl }
obtain ⟨x, hx⟩ : ∃ x, Algebra.trace (A ⧸ p) (B ⧸ P) x ≠ 0 := by
simpa [LinearMap.ext_iff] using Algebra.trace_ne_zero (A ⧸ p) (B ⧸ P)
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (e.symm (x, 0))
refine not_dvd_differentIdeal_of_intTrace_not_mem A P Q hP y ?_ ?_
· simpa [e, Ideal.Quotient.eq_zero_iff_mem] using congr((e $hy).2)
· rw [← Ideal.Quotient.eq_zero_iff_mem, ← Algebra.trace_quotient_eq_of_isDedekindDomain, hy,
Algebra.trace_eq_of_algEquiv, Algebra.trace_prod_apply]
simpa
