English
In localization, there exists a finite set controlling spans under scalar multiplication.
Русский
В локализации существует конечный набор, контролирующий порожденные по скалярному умножению подпространства.
LaTeX
$$$\\operatorname{smul\\_mem\\_finsetIntegerMultiple\\_span}$$$
Lean4
/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`.
If the image of some `x : S` falls in the span of some finite `s ⊆ S'` over `R`,
then there exists some `m : M` such that `m • x` falls in the
span of `IsLocalization.finsetIntegerMultiple _ s` over `R`.
-/
theorem smul_mem_finsetIntegerMultiple_span [Algebra R S] [Algebra R S'] [IsScalarTower R S S']
[IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S')
(hx : algebraMap S S' x ∈ Submodule.span R (s : Set S')) :
∃ m : M, m • x ∈ Submodule.span R (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) :=
by
let g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') fun c x => by simp [Algebra.algebraMap_eq_smul_one]
have g_apply : ∀ x, g x = algebraMap S S' x := fun _ => rfl
let y := IsLocalization.commonDenomOfFinset (M.map (algebraMap R S)) s
have hx₁ : (y : S) • (s : Set S') = g '' _ := (IsLocalization.finsetIntegerMultiple_image _ s).symm
obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop
have : algebraMap R S y' • (s : Set S') = y' • (s : Set S') := by
simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
rw [← e, this] at hx₁
replace hx₁ := congr_arg (Submodule.span R) hx₁
rw [Submodule.span_smul] at hx₁
replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx
rw [hx₁, ← g_apply, ← map_smul g, g_apply, ← Algebra.linearMap_apply, ← Submodule.map_span] at hx
obtain ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx
obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ := (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx''
use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M)
convert
(Submodule.span R (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s : Set S)).smul_mem a
hx' using
1
convert ha₂.symm using 1
· rw [Subtype.coe_mk, Submonoid.smul_def, Submonoid.coe_mul, ← smul_smul]
exact Algebra.smul_def _ _
· exact Algebra.smul_def _ _
