English
Let N be an AddCommMonoid with R- and S-actions forming a scalar tower, and a set a ⊆ N. Then x ∈ Submodule.span_S a iff there exist y ∈ Submodule.span_R a and z ∈ M with x = (mk'_S 1 z) • y.
Русский
Пусть N — аддитивное коммутативное моноидальное пространство с действиями R и S образующим тензорную башню; для множества a ⊆ N верно: x ∈ Submodule.span_S a тогда и только тогда, exists y ∈ Submodule.span_R a и z ∈ M с x = (mk'_S 1 z) • y.
LaTeX
$$mem_span_iff : ∀ {N} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {x : N} {a : Set N}, x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z : M, x = mk' S 1 z • y$$
Lean4
theorem mem_span_iff {N : Type*} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {x : N} {a : Set N} :
x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z : M, x = mk' S 1 z • y :=
by
constructor
· intro h
refine Submodule.span_induction ?_ ?_ ?_ ?_ h
· rintro x hx
exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, map_one, one_smul]⟩
· exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, map_one, one_smul]⟩
· rintro _ _ _ _ ⟨y, hy, z, rfl⟩ ⟨y', hy', z', rfl⟩
refine
⟨(z' : R) • y + (z : R) • y', Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'),
z * z', ?_⟩
rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ← IsScalarTower.algebraMap_smul S (z' : R), smul_smul,
smul_smul]
congr 1
· rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
· rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]
· rintro a _ _ ⟨y, hy, z, rfl⟩
obtain ⟨y', z', rfl⟩ := mk'_surjective M a
refine ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, ?_⟩
rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul, mul_comm (mk' S _ _),
mul_mk'_eq_mk'_of_mul]
· rintro ⟨y, hy, z, rfl⟩
exact Submodule.smul_mem _ _ (Submodule.span_subset_span R S _ hy)
