submodule.supr_mul

Stream: Is there code for X?

[Eric Wieser]

Is this statement true?

import algebra.algebra.operations

lemma submodule.supr_mul {ι R A} [comm_semiring R] [semiring A] [algebra R A] (s : ι → submodule R A) (t : submodule R A) :
  (⨆ i, s i) * t = ⨆ i, (s i * t) :=
begin
  dsimp [(*)],
  refine supr_subtype.trans _,
  change _ = ⨆ i (x : subtype (∈ s i)), _,
  simp_rw supr_subtype,
  dsimp only [subtype.coe_mk],
  sorry,
end

[Filippo A. E. Nuccio]

I can't find a has_sup (submodule R A) instance, where is it? I find the has_inf one...

[Oliver Nash]

It comes from docs#submodule.complete_lattice

[Oliver Nash]

There might be a better way but In situations like this I sometimes use library_search like this:

import linear_algebra

variables (R M : Type*) [semiring R] [add_comm_monoid M] [module R M]

example : has_sup (submodule R M) := by library_search

[Filippo A. E. Nuccio]

Ah great, I did not think about library_search for this. Thanks!

[Oliver Nash]

You might (and in this case do) need to iterate this but it should get you there.

[Oliver Nash]

Eric Wieser said:

Is this statement true?

Yes I think it is but it might be a bit fiddly to prove. Presumably one direction of inclusion is easy.

[Eric Wieser]

Looking again it's much nicer looking with the multiplication by t on the left

[Filippo A. E. Nuccio]

Strange!

[Kevin Buzzard]

Both sides are finite sums of s*t with s in the union of what you called s and what I would have called S, and t in what I would have called T

[Eric Wieser]

The fact that it ends up finite still baffles me, but I've seen enough of the mathlib API to convince me it's true. That handwave doesn't translate painlessly to a formalization I don't think

[Oliver Nash]

Consider the collection of all finite sums where the elements belong to some s i. This is obviously a submodule, and obviously contains all the s i so it must contain ⨆ i, s i. On the other hand, any element of ⨆ i, s i must contain such finite sums so in fact this is ⨆ i, s i. Similar remarks apply to the product of two submodules of an algebra.

[Alex J. Best]

Took me way longer than I wanted but I found a galois connection heavy proof:

import algebra.algebra.operations
open_locale pointwise
open submodule

lemma submodule.mul_eq_span_mul_set {R A} [comm_semiring R] [semiring A] [algebra R A]
  (s t : submodule R A) : s * t = span R ((s : set A) * (t : set A)) :=
by rw [← span_mul_span, span_eq, span_eq]

@[to_additive]
lemma set.Union_mul {α ι : Type*} [has_mul α] (s : ι → set α) (t : set α): (⋃ i, s i) * t = ⋃ i, (s i * t) :=
begin
  ext,
  simp [set.mem_mul, set.mem_Union],
  fsplit, work_on_goal 0 { intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_right, cases ᾰ_h_left, cases ᾰ_h_right_h, induction ᾰ_h_right_h_right, fsplit, work_on_goal 1 { fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { assumption }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { assumption }, refl } } } }, intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_h, cases ᾰ_h_h_right, cases ᾰ_h_h_right_h, induction ᾰ_h_h_right_h_right, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { assumption } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { assumption }, refl } },
end

lemma submodule.supr_mul {ι R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
  (s : ι → submodule R A) (t : submodule R A) : (⨆ i, s i) * t = ⨆ i, (s i * t) :=
begin
  conv_rhs { simp only [submodule.mul_eq_span_mul_set], },
  rw [← (submodule.gi R A).gc.l_supr, set.supr_eq_Union, ← set.Union_mul, ← set.supr_eq_Union,
    ← span_eq (span R ((⨆ (i : ι), ↑(s i)) * ↑t)), ← submodule.span_mul_span, span_eq, span_eq,
    ← (submodule.gi R A).l_supr_u],
end

[Kevin Buzzard]

Write a blog post for me :-)

[Eric Wieser]

set.Union_mul has a one line proof using docs#set.image2_Union_left _ _ _

[Alex J. Best]

Great! I was surprised not to find that lemma, as you can see my proof was just being lazy and hitting it with tidy :see_no_evil:

[Eric Wieser]

#8923