coprod and prod on submodules

Stream: Is there code for X?

[Eric Wieser]

Do we have anything that be used to make this proof shorter?

import linear_algebra.prod

variables {R M M₂ M₃} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
variables [module R M] [module R M₂] [module R M₃]

lemma coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃)
  (S : submodule R M) (S' : submodule R M₂) :
  (submodule.prod S S').map (linear_map.coprod f g) = (S.map f) ⊔ (S'.map g) :=
set_like.coe_injective $ begin
  ext,
  simp [submodule.mem_sup],
  simp_rw ←exists_and_distrib_left,
  simp_rw ←and_assoc,
end

[Eric Wieser]

I suspect a variant of docs#submodule.mem_sup that expressed the RHS as a sum would help

[Yakov Pechersky]

A term-mode-like proof:

lemma coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃)
  (S : submodule R M) (S' : submodule R M₂) :
  (submodule.prod S S').map (linear_map.coprod f g) = (S.map f) ⊔ (S'.map g) :=
begin
  ext,
  simp only [mem_sup, mem_map, linear_map.coprod_apply, mem_prod, prod.exists, exists_prop],
  exact ⟨λ ⟨y, z, ⟨hy, hz⟩, h⟩, ⟨f y, mem_map_of_mem hy, g z, mem_map_of_mem hz, h⟩,
         λ ⟨_, ⟨y, hy, rfl⟩, _, ⟨z, hz, rfl⟩, h⟩, ⟨y, z, ⟨hy, hz⟩, h⟩⟩
end

[Eric Wieser]

I think this was the lemma I wanted:

lemma coe_sup : ↑(p ⊔ p') = (p + p' : set M) :=
begin
  ext,
  rw [set_like.mem_coe, mem_sup, set.mem_add],
  simp,
end

[Eric Wieser]

#8220 adds coprod_map_prod and coe_sup. coe_supr is probably not far out of reach, but I didn't care enough to try.

[Alex J. Best]

@Eric Wieser maybe you are on holiday already, but which of the lemma you added here and docs#map_coprod_prod should we keep?

[Eric Wieser]

That link doesn't seem to work and the search page fails on mobile (I'm on holiday, but happy to do things that don't require lean access)

[Alex J. Best]

Oops sorry docs#linear_map.map_coprod_prod, its the same lemma as docs#linear_map.coprod_map_prod, just the new one has a nicer proof I suppose?

[Alex J. Best]

The naming convention is confusing me a lot though

[Eric Wieser]

Ouch, did I introduce that for other subobjects too?

[Eric Wieser]

Can we make a linter to catch this type of thing?

[Alex J. Best]

@Eric Wieser yes I found this with a "duplicate lemma finder" metaprogram!

[Eric Wieser]

How many others did you find?

[Alex J. Best]

Hard to say, some are still false positives but 30-50 maybe?

[Alex J. Best]

Just picked some that seemed easyish to fix up first in branch#alexjbest/dedup/1. But some are a bit subtle to choose which versions are better