Span and restriction of scalars

Stream: new members

[Riccardo Brasca]

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]

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]

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]

Time to have a coffee after missing this :coffee:

[Riccardo Brasca]

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]

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]

For this you can use docs#submodule.span_induction

[Adam Topaz]

(in general, not just for a finset)

[Riccardo Brasca]

Very nice, thank you!

[Adam Topaz]

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,
  exact submodule.add_mem _ hx hy,
  intros a x hx,
  rcases hsur a with ⟨a,rfl⟩,
  simp,
  refine submodule.smul_mem (span R X) _ hx,
end

[Riccardo Brasca]

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]

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

[Eric Wieser]

Did any of these lemmas get PR'd?

[Riccardo Brasca]

Mmh, I think so. Let me check my past PR

[Eric Wieser]

I just posted #10167, let me know if you see duplicates

[Riccardo Brasca]

It was #9363, let me see

[Eric Wieser]

Ah, it's in algebra.algebra.basic

[Riccardo Brasca]

docs#submodule.span_eq_restrict_scalars

[Riccardo Brasca]

Ah you already found it

[Eric Wieser]

I should have searched for the proof, that would have found it earlier! I've update the PR to remove the duplicate and fix the name clash