English
Core inductive step linking powers of ideals to the different ideal in a Dedekind setting with separability.
Русский
Ключевой шаг индукции, связывающий степени идеалов с различным идеалом в условиях Дедекинд и сепарабельности.
LaTeX
$$P^{e} ∣ p.map(AlgebraMap A B) \Rightarrow P^{e-1} ∣ \mathrm{differentIdeal}(A,B)$$
Lean4
theorem pow_sub_one_dvd_differentIdeal_aux {p : Ideal A} [p.IsMaximal] (P : Ideal B) {e : ℕ} (he : e ≠ 0) (hp : p ≠ ⊥)
(hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B :=
by
obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP
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.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
have : p.map (algebraMap A B) ∣ a ^ e := by
obtain ⟨b, hb⟩ := hP
apply_fun (· ^ e : Ideal B → _) at ha
apply_fun (· ^ (e - 1) : Ideal B → _) at hb
simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
exact ⟨_, ha.symm⟩
suffices ∀ x ∈ a, intTrace A B x ∈ p
by
have hP : ((P ^ (e - 1) :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) :=
by
apply inv_involutive.injective
simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div, mul_div_assoc]
rw [div_self (by simpa), mul_one]
rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ 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 : trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) :=
by
rw [← algebraMap_intTrace (A := A)]
exact ⟨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, ← trace_quotient_eq_of_isDedekindDomain, ← isNilpotent_iff_eq_zero]
refine trace_isNilpotent_of_isNilpotent ⟨e, ?_⟩
rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]
exact (Ideal.dvd_iff_le.mp this) <| Ideal.pow_mem_pow hx _
