English
For a fractional ideal I, spanSingleton S (algebraMap R P I.den) ⋅ I = I.num, connecting the denominator and numerator.
Русский
Для дробного идеала I имеется равенство между деноминатором и числителем: spanSingleton S (algebraMap R P I.den) · I = I.num.
LaTeX
$$$ \operatorname{spanSingleton}_S(\alpha) \cdot I = I_{\text{num}} , \text{ where } \alpha = (\text{algebraMap } R P I.den) $$$
Lean4
/-- `FractionalIdeal.span_finset R₁ s f` is the fractional ideal of `R₁` generated by `f '' s`. -/
-- Porting note: `@[simps]` generated a `Subtype.val` coercion instead of a
-- `FractionalIdeal.coeToSubmodule` coercion
def spanFinset {ι : Type*} (s : Finset ι) (f : ι → K) : FractionalIdeal R₁⁰ K :=
⟨Submodule.span R₁ (f '' s),
by
obtain ⟨a', ha'⟩ := IsLocalization.exist_integer_multiples R₁⁰ s f
refine ⟨a', a'.2, fun x hx => Submodule.span_induction ?_ ?_ ?_ ?_ hx⟩
· rintro _ ⟨i, hi, rfl⟩
exact ha' i hi
· rw [smul_zero]
exact IsLocalization.isInteger_zero
· intro x y _ _ hx hy
rw [smul_add]
exact IsLocalization.isInteger_add hx hy
· intro c x _ hx
rw [smul_comm]
exact IsLocalization.isInteger_smul hx⟩
