English
Nonzero fractional ideals have inverses with I · I^{-1} = 1.
Русский
Не нулевые дробные идеалы имеют обратные: I · I^{-1} = 1.
LaTeX
$$$$\\forall I \\neq 0:\\; I \\cdot I^{-1} = 1.$$$$
Lean4
/-- Nonzero fractional ideals in a Dedekind domain are units.
This is also available as `_root_.mul_inv_cancel`, using the
`Semifield` instance defined below.
-/
protected theorem mul_inv_cancel [IsDedekindDomain A] {I : FractionalIdeal A⁰ K} (hne : I ≠ 0) : I * I⁻¹ = 1 :=
by
obtain ⟨a, J, ha, hJ⟩ : ∃ (a : A) (aI : Ideal A), a ≠ 0 ∧ I = spanSingleton A⁰ (algebraMap A K a)⁻¹ * aI :=
exists_eq_spanSingleton_mul I
suffices h₂ : I * (spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ K)⁻¹) = 1
by
rw [mul_inv_cancel_iff]
exact ⟨spanSingleton A⁰ (algebraMap _ _ a) * (J : FractionalIdeal A⁰ K)⁻¹, h₂⟩
subst hJ
rw [mul_assoc, mul_left_comm (J : FractionalIdeal A⁰ K), coe_ideal_mul_inv, mul_one, spanSingleton_mul_spanSingleton,
inv_mul_cancel₀, spanSingleton_one]
· exact mt ((injective_iff_map_eq_zero (algebraMap A K)).mp (IsFractionRing.injective A K) _) ha
· exact coeIdeal_ne_zero.mp (right_ne_zero_of_mul hne)
