English
The conductor times the different ideal equals an explicit span of an evaluation in minpoly's derivative, relating to A and B via K,L.
Русский
Кондуктор умножает различное идеал на явное порождение минимуга, связанное с производной, через A,B и их поля K,L.
LaTeX
$$conductor(A,x) * differentIdeal(A,B) = Ideal.span{ aeval(x, derivative(minpoly A x)) }$$
Lean4
theorem conductor_mul_differentIdeal (x : B) (hx : Algebra.adjoin K {algebraMap B L x} = ⊤) :
(conductor A x) * differentIdeal A B = Ideal.span {aeval x (derivative (minpoly A x))} := by
classical
have hAx : IsIntegral A x := IsIntegralClosure.isIntegral A L x
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
apply FractionalIdeal.coeIdeal_injective (K := L)
simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton]
rw [coeIdeal_differentIdeal A K L B, mul_inv_eq_iff_eq_mul₀]
swap
· exact FractionalIdeal.dual_ne_zero A K one_ne_zero
apply FractionalIdeal.coeToSubmodule_injective
simp only [FractionalIdeal.coe_coeIdeal, FractionalIdeal.coe_mul, FractionalIdeal.coe_spanSingleton,
Submodule.span_singleton_mul]
ext y
have hne₁ : aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))) ≠ 0 :=
(Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0 := by
rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map, aeval_map_algebraMap,
aeval_algebraMap_apply] at hne₁
rw [Submodule.mem_smul_iff_inv_mul_mem this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual,
mem_coeSubmodule_conductor]
swap
· exact one_ne_zero
have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 := by
rwa [ne_eq, inv_eq_zero]
have : IsIntegral A (algebraMap B L x) := IsIntegral.map (IsScalarTower.toAlgHom A B L) hAx
simp_rw [← Subalgebra.mem_toSubmodule, ←
Submodule.mul_mem_smul_iff (y := y * _) (mem_nonZeroDivisors_of_ne_zero hne₂)]
rw [← traceForm_dualSubmodule_adjoin A K hx this]
simp only [LinearMap.BilinForm.mem_dualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule,
minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply,
mul_assoc, FractionalIdeal.mem_one_iff, forall_exists_index, forall_apply_eq_imp_iff]
simp_rw [← IsScalarTower.toAlgHom_apply A B L x, ← AlgHom.map_adjoin_singleton]
simp only [Subalgebra.mem_map, IsScalarTower.coe_toAlgHom', Submodule.one_eq_range, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂, ← map_mul]
exact ⟨fun H b ↦ (mul_one b) ▸ H b 1 (one_mem _), fun H _ _ _ ↦ H _⟩
