English
Fractional ideals form a cancellative monoid with zero in a Dedekind domain.
Русский
Дробные идеалы образуют отменяемый моноид с нулём в Дедекинд домене.
LaTeX
$$$$\\text{CancelCommMonoidWithZero}(\\text{FractionalIdeal}(A^0 K)),$$$$
Lean4
/-- Nonzero integral ideals in a Dedekind domain are invertible.
We will use this to show that nonzero fractional ideals are invertible,
and finally conclude that fractional ideals in a Dedekind domain form a group with zero.
-/
theorem coe_ideal_mul_inv [h : IsDedekindDomain A] (I : Ideal A) (hI0 : I ≠ ⊥) : I * (I : FractionalIdeal A⁰ K)⁻¹ = 1 :=
by
-- We'll show `1 ≤ J⁻¹ = (I * I⁻¹)⁻¹ ≤ 1`.
apply mul_inv_cancel_of_le_one hI0
by_cases hJ0 : I * (I : FractionalIdeal A⁰ K)⁻¹ = 0
· rw [hJ0, inv_zero']; exact zero_le _
intro x hx
suffices x ∈ integralClosure A K by
rwa [IsIntegrallyClosed.integralClosure_eq_bot, Algebra.mem_bot, Set.mem_range, ← mem_one_iff] at this
rw [mem_integralClosure_iff_mem_fg]
have x_mul_mem : ∀ b ∈ (I⁻¹ : FractionalIdeal A⁰ K), x * b ∈ (I⁻¹ : FractionalIdeal A⁰ K) :=
by
intro b hb
rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI0)]
dsimp only at hx
rw [val_eq_coe, mem_coe, mem_inv_iff hJ0] at hx
simp only [mul_assoc, mul_comm b] at hx ⊢
intro y hy
exact
hx _
(mul_mem_mul hy hb)
-- It turns out the subalgebra consisting of all `p(x)` for `p : A[X]` works.
refine
⟨AlgHom.range (Polynomial.aeval x : A[X] →ₐ[A] K),
isNoetherian_submodule.mp (isNoetherian (I : FractionalIdeal A⁰ K)⁻¹) _ fun y hy => ?_,
⟨Polynomial.X, Polynomial.aeval_X x⟩⟩
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp hy
rw [Polynomial.aeval_eq_sum_range]
refine Submodule.sum_mem _ fun i hi => Submodule.smul_mem _ _ ?_
clear hi
induction i with
| zero => rw [pow_zero]; exact one_mem_inv_coe_ideal hI0
| succ i ih => rw [pow_succ']; exact x_mul_mem _ ih
