English
Characterization of membership in an extended fractional ideal via span of mapped elements.
Русский
Характеризация принадлежности в расширенном дробном идеале через отображение элементов и порождение их зоной span.
LaTeX
$$$x \in I.extended L hf \iff x \in \mathrm{span}_B (map_f '' I)$$$
Lean4
/-- Given commutative rings `A` and `B` with respective localizations `IsLocalization M K` and
`IsLocalization N L`, and a ring homomorphism `f : A →+* B` satisfying `M ≤ Submonoid.comap f N`, a
fractional ideal `I` of `A` can be extended along `f` to a fractional ideal of `B`. -/
def extended (I : FractionalIdeal M K) : FractionalIdeal N L
where
val := span B <| (IsLocalization.map (S := K) L f hf) '' I
property := by
have ⟨a, ha, frac⟩ := I.isFractional
refine ⟨f a, hf ha, fun b hb ↦ ?_⟩
refine
span_induction (fun x hx ↦ ?_) ⟨0, by simp⟩ (fun x y _ _ hx hy ↦ smul_add (f a) x y ▸ isInteger_add hx hy)
(fun b c _ hc ↦ ?_) hb
· rcases hx with ⟨k, kI, rfl⟩
obtain ⟨c, hc⟩ := frac k kI
exact ⟨f c, by simp [← IsLocalization.map_smul, ← hc]⟩
· rw [← smul_assoc, smul_eq_mul, mul_comm (f a), ← smul_eq_mul, smul_assoc]
exact isInteger_smul hc
