English
Assume the same setting as above with primes P and p, and suppose that the extension is not separable at A/p over B/P. Then P divides the different ideal of A over B.
Русский
При тех же условиях, что и выше, если расслоение неразделимо на пару (A/p) над (B/P), то P делит разный идеал A над B.
LaTeX
$$$[\text{Assumptions as above}]\; (H : ¬ Algebra.IsSeparable (A / p) (B / P)) \Rightarrow P \mid \mathrm{differentIdeal } A B$$$
Lean4
theorem dvd_differentIdeal_of_not_isSeparable [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A}
[p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.IsMaximal] [P.LiesOver p] (H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)) :
P ∣ differentIdeal A B :=
by
obtain ⟨a, ha⟩ : P ∣ p.map (algebraMap A B) :=
Ideal.dvd_iff_le.mpr (Ideal.map_le_iff_le_comap.mpr Ideal.LiesOver.over.le)
by_cases hPa : P ∣ a
· simpa using pow_sub_one_dvd_differentIdeal A P 2 hp (by rw [pow_two, ha]; exact mul_dvd_mul_left _ hPa)
let K := FractionRing A
let L := FractionRing B
have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L := IsIntegralClosure.isLocalization _ K _ _
have : FiniteDimensional K L := .of_isLocalization A B A⁰
have hp' := (Ideal.map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)
have hPbot : P ≠ ⊥ := by
rintro rfl; apply hp'
rwa [Ideal.bot_mul] at ha
suffices ∀ x ∈ a, Algebra.intTrace A B x ∈ p
by
have hP : ((P :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) :=
by
apply inv_involutive.injective
simp only [ha, FractionalIdeal.coeIdeal_mul, inv_div, mul_div_assoc]
rw [div_self (by simpa), mul_one, inv_inv]
rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) hPbot, hP, Submodule.map_le_iff_le_comap]
intro x hx
rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
FractionalIdeal.mem_div_iff_of_nonzero (by simpa using hp')] at hx
rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one, ←
div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp), FractionalIdeal.mem_coe,
FractionalIdeal.mem_div_iff_of_nonzero (by simpa using hp)]
simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hx
intro y hy'
obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'
obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
have : Algebra.trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) :=
by
rw [← Algebra.algebraMap_intTrace (A := A)]
exact ⟨Algebra.intTrace A B z, this z hz, rfl⟩
rwa [mul_comm, ← smul_eq_mul, ← LinearMap.map_smul, Algebra.smul_def, mul_comm, ← IsScalarTower.algebraMap_apply,
IsScalarTower.algebraMap_apply A B L, ← hz']
intro x hx
rw [← Ideal.Quotient.eq_zero_iff_mem, ← Algebra.trace_quotient_eq_of_isDedekindDomain]
letI : Algebra (A ⧸ p) (B ⧸ a) :=
Ideal.Quotient.algebraQuotientOfLEComap
(Ideal.map_le_iff_le_comap.mp (Ideal.dvd_iff_le.mp ⟨_, ha.trans (mul_comm _ _)⟩))
have : IsScalarTower A (A ⧸ p) (B ⧸ a) := .of_algebraMap_eq' rfl
have : Module.Finite (A ⧸ p) (B ⧸ a) := .of_restrictScalars_finite A _ _
have := ((Ideal.prime_iff_isPrime hPbot).mpr inferInstance)
rw [← this.irreducible.gcd_eq_one_iff, ← Ideal.isCoprime_iff_gcd] at hPa
letI e : (B ⧸ p.map (algebraMap A B)) ≃ₐ[A ⧸ p] ((B ⧸ P) × B ⧸ a) :=
{ __ := (Ideal.quotEquivOfEq ha).trans (Ideal.quotientMulEquivQuotientProd P a hPa),
commutes' := Quotient.ind fun _ ↦ rfl }
have hx' : (e (Ideal.Quotient.mk _ x)).2 = 0 := by simpa [e, Ideal.Quotient.eq_zero_iff_mem]
rw [← Algebra.trace_eq_of_algEquiv e, Algebra.trace_prod_apply, Algebra.trace_eq_zero_of_not_isSeparable H,
LinearMap.zero_apply, zero_add, hx', map_zero]
