English
In a Dedekind domain that is not a field, for any nonzero, non-top ideal I, its inverse I^{-1} is not contained in the unit interval, i.e., I^{-1} ≰ 1.
Русский
В Дедекинд домене, не являющемся полем, для любого ненулевого и не-топ идеала I обратный I^{-1} не содержится в единичном интервале: I^{-1} ≰ 1.
LaTeX
$$$$I \\neq 0,\\ I \\neq 1 \\Rightarrow \\neg\\big( I^{-1} \\le 1 \\big).$$$$
Lean4
theorem not_inv_le_one_of_ne_bot [IsDedekindDomain A] {I : Ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) :
¬(I⁻¹ : FractionalIdeal A⁰ K) ≤ 1 :=
by
have hNF : ¬IsField A := fun h ↦
letI := h.toField;
(eq_bot_or_eq_top I).elim hI0 hI1
wlog hM : I.IsMaximal generalizing I
· rcases I.exists_le_maximal hI1 with ⟨M, hmax, hIM⟩
have hMbot : M ≠ ⊥ := (M.bot_lt_of_maximal hNF).ne'
refine mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax) <;>
simpa only [coeIdeal_ne_zero, coeIdeal_le_coeIdeal]
have hI0 : ⊥ < I := I.bot_lt_of_maximal hNF
obtain ⟨⟨a, haI⟩, ha0⟩ := Submodule.nonzero_mem_of_bot_lt hI0
replace ha0 : a ≠ 0 := Subtype.coe_injective.ne ha0
let J : Ideal A := Ideal.span { a }
have hJ0 : J ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp ha0
have hJI : J ≤ I := I.span_singleton_le_iff_mem.2 haI
obtain ⟨Z, hle, hnle⟩ := exists_multiset_prod_cons_le_and_prod_not_le hNF hJ0 hJI
obtain ⟨b, hbZ, hbJ⟩ := SetLike.not_le_iff_exists.mp hnle
have hnz_fa : algebraMap A K a ≠ 0 := mt ((injective_iff_map_eq_zero _).mp (IsFractionRing.injective A K) a) ha0
refine Set.not_subset.2 ⟨algebraMap A K b * (algebraMap A K a)⁻¹, (mem_inv_iff ?_).mpr ?_, ?_⟩
· exact coeIdeal_ne_zero.mpr hI0.ne'
· rintro y₀ hy₀
obtain ⟨y, h_Iy, rfl⟩ := (mem_coeIdeal _).mp hy₀
rw [mul_comm, ← mul_assoc, ← RingHom.map_mul]
have h_yb : y * b ∈ J := by
apply hle
rw [Multiset.prod_cons]
exact Submodule.smul_mem_smul h_Iy hbZ
rw [Ideal.mem_span_singleton'] at h_yb
rcases h_yb with ⟨c, hc⟩
rw [← hc, RingHom.map_mul, mul_assoc, mul_inv_cancel₀ hnz_fa, mul_one]
apply coe_mem_one
· refine mt (mem_one_iff _).mp ?_
rintro ⟨x', h₂_abs⟩
rw [← div_eq_mul_inv, eq_div_iff_mul_eq hnz_fa, ← RingHom.map_mul] at h₂_abs
have := Ideal.mem_span_singleton'.mpr ⟨x', IsFractionRing.injective A K h₂_abs⟩
contradiction
