English
There is a localized-module isomorphism connecting a fractional ideal and its coefficient submodule via restriction of scalars to ℤ.
Русский
Существует изоморфизм локализованного модуля, соединяющий дробный идеал и его коэффициентный подсубмодуль через ограничение скаляра к ℤ.
LaTeX
$$$I \\mathrm{.equivNum} \\text{( localisation isomorphism )}$$$
Lean4
instance (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) :
IsLocalizedModule ℤ⁰ ((Submodule.subtype (I : Submodule (𝓞 K) K)).restrictScalars ℤ)
where
map_units
x :=
by
rw [← (Algebra.lmul _ _).commutes, Algebra.lmul_isUnit_iff, isUnit_iff_ne_zero, eq_intCast, Int.cast_ne_zero]
exact nonZeroDivisors.coe_ne_zero x
surj
x := by
obtain ⟨⟨a, _, d, hd, rfl⟩, h⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) x
refine ⟨⟨⟨Ideal.absNorm I.1.num * (algebraMap _ K a), I.1.num_le ?_⟩, d * Ideal.absNorm I.1.num, ?_⟩, ?_⟩
· simp_rw [FractionalIdeal.val_eq_coe, FractionalIdeal.coe_coeIdeal]
refine (IsLocalization.mem_coeSubmodule _ _).mpr ⟨Ideal.absNorm I.1.num * a, ?_, ?_⟩
· exact Ideal.mul_mem_right _ _ I.1.num.absNorm_mem
· rw [map_mul, map_natCast]
· refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)
rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff]
exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I
· simp_rw [LinearMap.coe_restrictScalars, Submodule.coe_subtype] at h ⊢
rw [← h]
simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, algebraMap_int_eq, eq_intCast,
map_intCast]
ring
exists_of_eq h := ⟨1, by rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]⟩
