English
FaithfullyFlat is stable under base change (repeat of general property).
Русский
FaithfullyFlat устойчива к базовым изменениям (общая свойство).
LaTeX
$$$\\operatorname{IsStableUnderBaseChange}(\\text{FaithfullyFlat})$$$
Lean4
/-- If `M` is an `R' = S⁻¹R` module, and `x ∈ span R' s`,
then `t • x ∈ span R s` for some `t : S`. -/
theorem multiple_mem_span_of_mem_localization_span {N : Type*} [AddCommMonoid N] [Module R N] [Module R' N]
[IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) (hx : x ∈ Submodule.span R' s) :
∃ (t : M), t • x ∈ Submodule.span R s := by
classical
obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
· exact ⟨t, Submodule.span_mono hss' ht⟩
clear hx hss' s
induction s' using Finset.induction_on generalizing x with
| empty => use 1; simpa using hs'
| insert a s _ hs =>
simp only [Finset.coe_insert, Submodule.mem_span_insert] at hs' ⊢
rcases hs' with ⟨y, z, hz, rfl⟩
rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
apply congrArg (fun x ↦ x • a)at e
simp only [algebraMap_smul] at e
rcases hs _ hz with ⟨t, ht⟩
refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
simp [Submonoid.smul_def]
