English
Under suitable hypotheses, containment of a principal ideal in an S-span descends to a corresponding containment after base change to a larger localization L.
Русский
При надлежащих условиях включение главной идеальной оболочки в S-образный подмодуль распространяется на соответствующее включение после перехода по базису к большему локализационному кольцу L.
LaTeX
$$$ (\operatorname{Ideal.span}\{a\} : S) \subseteq \operatorname{Submodule.span}_R(b) \Rightarrow (\operatorname{Ideal.span}\{\mathrm{algebraMap}_{S\to L}(a)\} : L) \subseteq \operatorname{Submodule.span}_K(\mathrm{algebraMap}_{S\to L}(b)) $$$
Lean4
/-- If the `S`-multiples of `a` are contained in some `R`-span, then `Frac(S)`-multiples of `a`
are contained in the equivalent `Frac(R)`-span. -/
theorem ideal_span_singleton_map_subset {L : Type*} [IsDomain R] [IsDomain S] [Field K] [Field L] [Algebra R K]
[Algebra R L] [Algebra S L] [Algebra.IsAlgebraic R S] [IsFractionRing S L] [Algebra K L] [IsScalarTower R S L]
[IsScalarTower R K L] {a : S} {b : Set S} (inj : Function.Injective (algebraMap R L))
(h : (Ideal.span ({ a } : Set S) : Set S) ⊆ Submodule.span R b) :
(Ideal.span ({algebraMap S L a} : Set L) : Set L) ⊆ Submodule.span K (algebraMap S L '' b) :=
by
intro x hx
obtain ⟨x', rfl⟩ := Ideal.mem_span_singleton.mp hx
obtain ⟨y', z', rfl⟩ := IsLocalization.mk'_surjective S⁰ x'
obtain ⟨y, z, hz0, yz_eq⟩ := Algebra.IsAlgebraic.exists_smul_eq_mul R y' (nonZeroDivisors.coe_ne_zero z')
have injRS : Function.Injective (algebraMap R S) :=
by
refine Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from ?_)
rwa [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]
have hz0' : algebraMap R S z ∈ S⁰ :=
map_mem_nonZeroDivisors (algebraMap R S) injRS (mem_nonZeroDivisors_of_ne_zero hz0)
have mk_yz_eq : IsLocalization.mk' L y' z' = IsLocalization.mk' L y ⟨_, hz0'⟩ :=
by
rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq
exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])
suffices hy : algebraMap S L (a * y) ∈ Submodule.span K ((algebraMap S L) '' b)
by
rw [mk_yz_eq, IsFractionRing.mk'_eq_div, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R K L,
div_eq_mul_inv, ← mul_assoc, mul_comm, ← map_inv₀, ← Algebra.smul_def, ← map_mul]
exact (Submodule.span K _).smul_mem _ hy
refine Submodule.span_subset_span R K _ ?_
rw [Submodule.span_algebraMap_image_of_tower]
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify the value of `f` here:
exact Submodule.mem_map_of_mem (f := LinearMap.restrictScalars _ _) (h (Ideal.mem_span_singleton.mpr ⟨y, rfl⟩))
