submodule.sup basic lemma

Stream: Is there code for X?

[Patrick Massot]

I'm not able to find

import linear_algebra.basic

open submodule
variables {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [semiring R] [semiring R₂]
  [add_comm_monoid M] [add_comm_monoid M₂] {σ₁₂ : R →+* R₂} [module R M]
  [module R₂ M₂]

lemma submodule.sup_eq_span_union (s t : submodule R M) : s ⊔ t = span R (s ∪ t) :=
by rw [span_union, span_eq s, span_eq t]

lemma linear_map.eq_on_sup  {s t : submodule R M} {f g : M →ₛₗ[σ₁₂] M₂} (hs : ∀ x ∈ s, f x = g x)
  (ht : ∀ x ∈ t, f x = g x) {x : M} (hx : x ∈ s ⊔ t) : f x = g x :=
linear_map.eq_on_span (show ∀ x ∈ (s : set M) ∪ t, f x = g x, by { rintros x (h|h) ; tauto })
  ((s.sup_eq_span_union t) ▸ hx)

Am I missing something?

[Eric Wieser]

The first lemma strikes me as a bit specialized, unless we already have something analogous for supr

[Eric Wieser]

The second feels like it might be nice to also have stated as an ext lemma for f g : s ⊔ t →ₗ M, with hypotheses f.comp (submodule.of_le le_sup_left) = g.comp (submodule.of_le le_sup_left) and similar for right

[Eric Wieser]

Probably we haven't bothered with many of these lemmas because docs#submodule.mem_sup is easy enough to use.

[Kevin Buzzard]

Do we have span_union in the form span (a ∪ b) = span a ⊔ span b? This is true for lots of subobjects

[Patrick Massot]

Yes Kevin, span_union already says that.

[Patrick Massot]

Eric, I'm not convinced at all by your arguments, and the variation you suggest would be a lot less convenient to use (and we indeed already have the supr version). So I'm going to PR that at some point (it will first go to the sphere eversion project).

[Eric Wieser]

We don't appear to have linear_map.eq_on_supr, unless if has another name

[Eric Wieser]

But you're right, docs#supr_eq_span (_Union) does exist. Perhaps we should rename it to match your suggested sup_eq_span_union.