## Stream: new members

### Topic: Span and restriction of scalars

#### Riccardo Brasca (Jan 19 2021 at 16:00):

I would like to prove the following: $A$ is an $R$-algebra and $M$ an $A$-module. For $X \subseteq M$ a subset, then $\langle X \rangle_R \subseteq \langle X \rangle_A$, where $\langle X \rangle_R$ is the the submodule generated by $X$ as $R$-module, and similarly for $\langle X \rangle_A$. This is easy writing an element of $\langle X \rangle_R$ as an $R$-linear combination, but I do not see this description in mathlib. I am able to prove the lemma if $X$ is finite, as follows

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : finset M) : span R (X : set M)  restrict_scalars R (span A X) :=
begin
induction X using finset.induction with a X haX h,
{ exact classical.dec_eq M },
{ simp only [span_empty, finset.coe_empty, restrict_scalars_bot, le_bot_iff] },
{ rw [submodule.le_def] at h ,
intros m hm,
rw [finset.coe_insert, mem_coe] at hm ,
obtain r, n, hn, hmsum := mem_span_insert.1 hm,
rw [restrict_scalars_mem, mem_span_insert],
replace hz := h hn,
rw [mem_coe, restrict_scalars_mem] at hz,
use [(algebra_map R A) r, n, hz],
simp only [hmsum, algebra_map_smul] }
end

using finset.induction. This is enough for what I want to do later (about finitely generated submodule), but it would be nice to have the general result. Does someone see a quick way to prove it? Thanks!

#### Adam Topaz (Jan 19 2021 at 16:06):

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : set M) : span R (X : set M)  restrict_scalars R (span A X) :=
begin
rw submodule.span_le,
exact submodule.subset_span,
end

#### Adam Topaz (Jan 19 2021 at 16:08):

Golfed:

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : set M) : span R (X : set M)  restrict_scalars R (span A X) :=
submodule.span_le.mpr submodule.subset_span

#### Riccardo Brasca (Jan 19 2021 at 16:16):

Time to have a coffee after missing this :coffee:

#### Riccardo Brasca (Jan 19 2021 at 16:41):

On the other hand to prove the other inclusion (assuming that $R \to A$ is surjective) seems to need to play with the linear combinations, so it is ok for finset, but trickier for set.

#### Riccardo Brasca (Jan 19 2021 at 17:07):

Something like this

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : set M) : span R (X : set M)  restrict_scalars R (span A X) :=
submodule.span_le.mpr submodule.subset_span

lemma test1 (X : finset M) (hsur : function.surjective (algebra_map R A)) :
span R (X : set M) = restrict_scalars R (span A X) :=
begin
apply le_antisymm (test R A M X),
induction X using finset.induction with x X haX h,
{ exact classical.dec_eq M },
{ simp only [span_empty, finset.coe_empty, restrict_scalars_bot, le_bot_iff] },
{ rw [submodule.le_def] at h ,
intros n hn,
rw [finset.coe_insert, mem_coe] at hn ,
rw [restrict_scalars_mem] at hn,
obtain a, m, hm, hnsum := mem_span_insert.1 hn,
rw [mem_span_insert],
obtain r, hr := hsur a,
use [r, m],
split,
{ exact h ((restrict_scalars_mem R _ m).2 hm) },
{ rw [ hr] at hnsum,
simp only [hnsum, algebra_map_smul] } }
end

#### Adam Topaz (Jan 19 2021 at 17:43):

For this you can use docs#submodule.span_induction

#### Adam Topaz (Jan 19 2021 at 17:43):

(in general, not just for a finset)

#### Riccardo Brasca (Jan 19 2021 at 17:49):

Very nice, thank you!

#### Adam Topaz (Jan 19 2021 at 17:52):

This should be golfed (and has a nonterminal simp), but you get the idea:

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : set M) : span R (X : set M)  restrict_scalars R (span A X) :=
submodule.span_le.mpr submodule.subset_span

lemma test1 (X : set M) (hsur : function.surjective (algebra_map R A)) :
span R (X : set M) = restrict_scalars R (span A X) :=
begin
refine le_antisymm _ _,
apply test,
intros x hx,
refine submodule.span_induction hx submodule.subset_span (submodule.zero_mem _) _ _,
intros x y hx hy,
intros a x hx,
rcases hsur a with a,rfl⟩,
simp,
refine submodule.smul_mem (span R X) _ hx,
end

#### Riccardo Brasca (Jan 19 2021 at 18:09):

Wow, I basically wrote exactly the same proof as you! (I was just slower :joy: )

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : set M) : span R (X : set M)  restrict_scalars R (span A X) :=
submodule.span_le.mpr submodule.subset_span

lemma test1 (X : set M) (hsur : function.surjective (algebra_map R A)) :
span R X = restrict_scalars R (span A X) :=
begin
apply le_antisymm (test R A M X),
intros m hm,
refine span_induction hm subset_span (zero_mem _) _ _,
{ intros m₁ m₂ hm₁ hm₂,
exact (submodule.add_mem _ hm₁ hm₂) },
{ intros a m hm,
obtain r, rfl := hsur a,
rw [algebra_map_smul],
exact smul_mem _ r hm }
end

#### Adam Topaz (Jan 19 2021 at 18:49):

Golfed a bit:

import algebra.algebra.basic

variables (R : Type*) (A : Type*) (M : Type*)
variables [comm_semiring R] [semiring A] [algebra R A]
variables [add_comm_monoid M] [semimodule R M][semimodule A M] [is_scalar_tower R A M]

open submodule

lemma test (X : set M) : span R (X : set M)  restrict_scalars R (span A X) :=
submodule.span_le.mpr submodule.subset_span

lemma test1 (X : set M) (hsur : function.surjective (algebra_map R A)) :
span R (X : set M) = restrict_scalars R (span A X) :=
begin
refine le_antisymm (test _ _ _ _) (λ x hx, _),
refine submodule.span_induction hx subset_span (zero_mem _) (λ _ _, add_mem _) (λ a x hx, _),
rcases hsur a with a,rfl⟩,
rw algebra_map_smul,
refine submodule.smul_mem (span R X) _ hx,
end

Last updated: May 07 2021 at 00:30 UTC