Zulip Chat Archive

Stream: new members

Topic: Span and restriction of scalars


view this post on Zulip Riccardo Brasca (Jan 19 2021 at 16:00):

I would like to prove the following: AA is an RR-algebra and MM an AA-module. For XMX \subseteq M a subset, then XRXA\langle X \rangle_R \subseteq \langle X \rangle_A, where XR\langle X \rangle_R is the the submodule generated by XX as RR-module, and similarly for XA\langle X \rangle_A. This is easy writing an element of XR\langle X \rangle_R as an RR-linear combination, but I do not see this description in mathlib. I am able to prove the lemma if XX 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Jan 19 2021 at 16:16):

Time to have a coffee after missing this :coffee:

view this post on Zulip Riccardo Brasca (Jan 19 2021 at 16:41):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Jan 19 2021 at 17:43):

For this you can use docs#submodule.span_induction

view this post on Zulip Adam Topaz (Jan 19 2021 at 17:43):

(in general, not just for a finset)

view this post on Zulip Riccardo Brasca (Jan 19 2021 at 17:49):

Very nice, thank you!

view this post on Zulip 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,
  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

view this post on Zulip 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

view this post on Zulip 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