English
The coeIdeal of a span singleton equals the span singleton of the mapped generator.
Русский
Коэффициентный идеал спана единицы равен spanSingleton образа генератора через маппинг.
LaTeX
$$(↑(Ideal.span { x } : Ideal R) : FractionalIdeal S P) = spanSingleton S (algebraMap R P x)$$
Lean4
theorem exists_eq_spanSingleton_mul (I : FractionalIdeal R₁⁰ K) :
∃ (a : R₁) (aI : Ideal R₁), a ≠ 0 ∧ I = spanSingleton R₁⁰ (algebraMap R₁ K a)⁻¹ * aI :=
by
obtain ⟨a_inv, nonzero, ha⟩ := I.isFractional
have nonzero := mem_nonZeroDivisors_iff_ne_zero.mp nonzero
have map_a_nonzero : algebraMap R₁ K a_inv ≠ 0 := mt IsFractionRing.to_map_eq_zero_iff.mp nonzero
refine
⟨a_inv, Submodule.comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ (algebraMap R₁ K a_inv) * I), nonzero,
ext fun x => Iff.trans ⟨?_, ?_⟩ mem_singleton_mul.symm⟩
· intro hx
obtain ⟨x', hx'⟩ := ha x hx
rw [Algebra.smul_def] at hx'
refine ⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩
· exact ⟨x, hx, hx'⟩
· rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
· rintro ⟨y, hy, rfl⟩
obtain ⟨x', hx', rfl⟩ := (mem_coeIdeal _).mp hy
obtain ⟨y', hy', hx'⟩ := mem_singleton_mul.mp hx'
rw [Algebra.linearMap_apply] at hx'
rwa [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]
