English
The class of mk0(I) equals the class of I via integralRep, aligning mk0 with mk.
Русский
Класс mk0(I) совпадает с классом через integralRep, согласуя mk0 и mk.
LaTeX
$$$\mathrm{ClassGroup.mk0}(\langle \mathrm{ClassGroup.integralRep}(I), \mathrm{mem}\rangle) = \mathrm{ClassGroup.mk}(I).$$$
Lean4
theorem mk0_integralRep [IsDedekindDomain R] (I : (FractionalIdeal R⁰ (FractionRing R))ˣ) :
ClassGroup.mk0 ⟨ClassGroup.integralRep I, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩ = ClassGroup.mk I :=
by
rw [← ClassGroup.mk_mk0 (FractionRing R), eq_comm, ClassGroup.mk_eq_mk]
have fd_ne_zero : (algebraMap R (FractionRing R)) I.1.den ≠ 0 := by
exact IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (SetLike.coe_mem _)
refine ⟨Units.mk0 (algebraMap R _ I.1.den) fd_ne_zero, ?_⟩
apply Units.ext
rw [mul_comm, val_mul, coe_toPrincipalIdeal, val_mk0]
exact FractionalIdeal.den_mul_self_eq_num' R⁰ (FractionRing R) I
