English
For a prime ideal P of B (P maximal), under the separability hypothesis, P does not divide the different ideal of A over B if and only if A/p is unramified over B/P.
Русский
Пусть P — главный (максимальный) идеал B. При условии сепарабильности верно: P не делит разностный идеал A над B тогда и только тогда, когда A/p неразветвлена над B/P.
LaTeX
$$$[ Algebra.IsSeparable (\mathrm{FractionRing } A) (\mathrm{FractionRing } B)] \Rightarrow (\neg P \mid \mathrm{differentIdeal } A B) \iff \mathrm{Algebra.IsUnramifiedAt } A P$$$
Lean4
/-- A prime does not divide the different ideal iff it is unramified. -/
theorem not_dvd_differentIdeal_iff [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B} [P.IsPrime] :
¬P ∣ differentIdeal A B ↔ Algebra.IsUnramifiedAt A P := by
classical
rcases eq_or_ne P ⊥ with rfl | hPbot
· simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
let K := FractionRing A
let L := FractionRing B
have : FiniteDimensional K L := .of_isLocalization A B A⁰
have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) :=
by
convert (inferInstanceAs (IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B))))
ext; simp [Ideal.primeCompl]
refine (Algebra.FormallyUnramified.iff_of_equiv (A := L) ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
have : Algebra.FormallyUnramified K L := by rwa [Algebra.FormallyUnramified.iff_isSeparable]
refine .comp A K L
have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
have hp' := (Ideal.map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
have := Ideal.IsPrime.isMaximal inferInstance hPbot
constructor
· intro H
· rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
constructor
· suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
contrapose! H
exact dvd_differentIdeal_of_not_isSeparable A hp P H
· rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
apply Ideal.ramificationIdx_spec
· simp [Ideal.map_le_iff_le_comap]
· contrapose! H
rw [← pow_one P, show 1 = 2 - 1 by simp]
apply pow_sub_one_dvd_differentIdeal _ _ _ hp
simpa [Ideal.dvd_iff_le] using H
· intro H
obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm
