Sums of subspaces (Axler's Linear Algebra Done Right)

Stream: new members

[Arien Malec]

I've got Axler's Linear Algebra done up to (checks notes) page 20... at https://github.com/arienmalec/axler

I'm up to Sums of Subspaces which are defined as "the set of all possible sums of elements" of the respective subspaces. I see definitions for finite sums, and for direct sums, but not for (possibly infinite) sums, as Axler defines.

An example proof here is that if U = {<x, 0, 0>} and V = {<0, y, 0>} over R^3 then U + V = {<x, y, 0>}

What's the natural translation in Mathlib terms?

[Matt Diamond]

infinite sums are docs#tsum, I think...

[Arien Malec]

Hmm. Has a TopologicalSpace constraint....

[Arien Malec]

Is Axler's definition AoC under the hood?

[Timo Carlin-Burns]

The standard notation for this is U ⊔ V or if you open Pointwise, U + V.

[Arien Malec]

Googling, is this AKA the Minkowski sum

[Timo Carlin-Burns]

Infinite sums mean something different from pointwise sums of (possibly infinite) sets

[Arien Malec]

I'm down to this goal state, which should close easily, but unsure what closes it

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fin.VecNotation

example {y z: ℝ}: Add.add ![y, 0, 0] ![0, z, 0] = ![y, z, 0] := by sorry

[Ruben Van de Velde]

Maybe ext; simp, or with fin_cases in between?

[Ruben Van de Velde]

Though it's odd that you have Add.add rather than +

[Eric Wieser]

The subspace of elements formed from finite sums of an infinite family of subspaces is ⨆ i, p i

[Arien Malec]

Ruben Van de Velde said:

Though it's odd that you have Add.add rather than +

Overaggressive simp

[Kevin Buzzard]

But simp shouldn't change + to Add.add -- it should be the other way around!

[Arien Malec]

I requested simp of HAdd.hAdd, Set.add -- I'm sure there's a better way here...

[Arien Malec]

The original setup and current proof state are:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic

open Pointwise
def ex1_37_U : (Set (Fin 3 → ℝ)) :=
  { ![x₁, 0, 0] | (x₁: ℝ)}
def ex1_37_V : (Set (Fin 3 → ℝ)) :=
  { ![0, x₂, 0] |  (x₂ : ℝ)}

theorem ex1_37: ex1_37_U + ex1_37_V = { ![x₁, x₂, 0] | (x₁: ℝ) (x₂: ℝ)} := by
  simp [ex1_37_U,ex1_37_V]
  simp [HAdd.hAdd, Set.add, Set.image2]
  ext x; constructor <;> intro h
  . cases' h with y h
    cases' h with z h
    simp [Set.mem_setOf_eq, *] at *
    use y; use z
    rw [←h]; symm
    have h2: ![y, 0, 0] + ![0, z, 0] = ![y, z, 0] := by
      ext x ; fin_cases x <;> simp
    exact h2
  . simp at *
    rcases h with ⟨y,z, h⟩
    use y; use z
    rw [←h]
    have h2: ![y, 0, 0] + ![0, z, 0] = ![y, z, 0] := by
      ext x ; fin_cases x <;> simp
    exact h2

[Damiano Testa]

You could also do

theorem ex1_37: ex1_37_U + ex1_37_V = { ![x₁, x₂, 0] | (x₁: ℝ) (x₂: ℝ)} := by
  ext x
  simp [Set.mem_add, ex1_37_U,ex1_37_V]

[Damiano Testa]

(and if you used abbrev instead of defs, you would not even need to explicitly unfold ex1_37_U and ex1_37_V.)

[Arien Malec]

That's, uh, quite a bit simpler

[Damiano Testa]

If you look at the statement, it is simply saying that a double existential is the same a two consecutive existentials: this is something that simp should know about and you simply have to tell it what it means to be a member of the sum of two sets. Hence, simp [Set.mem_add] (+ the unfolding).

[Damiano Testa]

Also, as an almost universal rule: unfolding Add.add (or similar instances) means you are making your proof harder than it should be.

[Damiano Testa]

You should trust that whoever defined Add.add also introduced the useful statements about it. You could be in a situation where there is missing API, but then you should look for the missing API lemma, instead of embedding it into your proof.

[Arien Malec]

The trick was using ext prior -- I tried mem_add previously.

[Arien Malec]

Here's where this got to -- weird that add_mem' required a bunch of tactics where the others are simp. Digging around, it seems like some of the core lemmata in Mathlib.Data.Fin.VecNotation were dependent on bit0/1 in Mathlib3?

[Arien Malec]

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic

open Pointwise

def subspace_ex1_37_U: Submodule ℝ (Fin 3 → ℝ) where
  carrier :=  { ![x₁, 0, 0] | (x₁: ℝ)}
  zero_mem' := by simp
  add_mem' := by simp; intro _ _ x c y d; use (x + y); rw [←c, ←d]; ext z; simp; fin_cases z <;> simp
  smul_mem' := by simp

def subsdpace_ex1_37_V: Submodule ℝ (Fin 3 → ℝ) where
  carrier := { ![0, x₂, 0] |  (x₂ : ℝ)}
  zero_mem' := by simp
  smul_mem' := by simp
  add_mem' := by simp; intro _ _ x c y d; use (x + y); rw [←c, ←d]; ext z; simp; fin_cases z <;> simp

theorem ex1_37: { ![x₁, 0, 0] | (x₁: ℝ)} + { ![0, x₂, 0] |  (x₂ : ℝ)} = { ![x₁, x₂, 0] | (x₁: ℝ) (x₂: ℝ)} := by
  ext x ; simp [Set.mem_add]

#synth Module ℝ (subspace_ex1_37_U + subsdpace_ex1_37_V)

[Damiano Testa]

aesop proves your add_mem' fields.

[Arien Malec]

I'm a bit burnt by hint telling me to try aesop then aesop failing to do anything :-)

[Arien Malec]

How do I show that U + V is Submodule ℝ (Fin 3 → ℝ)?

[Arien Malec]

Ah #check

[Yakov Pechersky]

It follows from the definition of "Submodule" and the fact it has an Add instance, so it's a bit of a tautology. I think a more "rigorous" way would be to show that

def U_plus_V : Submodule R ... where
  carrier := pointwise addition of U as a set and V as a set
  prove the axioms of a Submodule

and then show that U_plus_V = U + V (either as submodules or as sets). I bet the proof will be ext; rfl or rfl.

[Yakov Pechersky]

which is basically the specialization of the proof that (. + .) as defined respects the submodule conditions

[Arien Malec]

Yeah, the instance for AddCommMonoid does the work to show the closure....

[Kim Morrison]

Arien Malec said:

I'm a bit burnt by hint telling me to try aesop then aesop failing to do anything :-)

@Arien Malec, do we have a repro for this? Please ping me and/or Jannis if so.

[Arien Malec]

Next time I see it, I'll #MWE

[Arien Malec]

#MWE for @Scott Morrison

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic

open Pointwise
def ex4_Subspace: Submodule ℝ (ℝ → ℝ) where
  carrier := { f | (∀ x ∈ Set.Ioo (0 : ℝ)  (3: ℝ), DifferentiableAt ℝ f x) ∧ (HasDerivAt f 0 2)}
  zero_mem' := by
    constructor
    . intro _ _
      exact differentiableAt_const 0
    . apply hasDerivAtFilter_const
  add_mem' := by aesop
    -- intro a b h1 h2
    -- constructor
    -- . intro x h
    --   rcases (h1.left x h) with ⟨ f'x, f_has ⟩
    --   rcases (h2.left x h) with ⟨ g'x, g_has ⟩
    --   use f'x + g'x
    --   exact f_has.add g_has
    -- . have h3:= h1.right.add h2.right
    --   simp [@Pi.add_def] at *
    --   assumption
  smul_mem' := by
    intro a f hf
    cases' hf with hf1 hf2
    constructor
    . intro b h
      have h2 := (hf1 b h).smul_const a
      simp [@Pi.smul_def] at *
      simp_rw [mul_comm a (f _)]
      exact h2
    . have h := hf2.smul_const a
      simp [@Pi.smul_def] at *
      simp_rw [mul_comm a (f _)]
      exact h

[Arien Malec]

hint here says to try aesop, but aesop does nothing.

[Eric Wieser]

Doesn't aesop do intros?

[Kevin Buzzard]

Note that hint gives suggestions plus what the goal will be after you try these suggestions, if hint can't close the goal. If hint closes the goal then the suggestion is in green, and if it doesn't then the suggestion is in blue.

[Arien Malec]

Here, the aesop goal state is a garble

 DifferentiableAt ℝ (_uniq.201000 + _uniq.201001) _uniq.233268
⊢ HasDerivAt (_uniq.201000 + _uniq.201001) 0 2

It's possible I just need to update Mathlib?

[Arien Malec]

Anyway, the lass proof in Axler is
"Suppose 𝑉_1, ..., 𝑉_𝑚 are subspaces of 𝑉. Then 𝑉_1 + ⋯ + 𝑉_𝑚 is the smallest subspace of 𝑉 containing 𝑉_1, ..., 𝑉_𝑚."

When I translate this to Lean and Mathlib the way I understand it (post exposure to Lean and Mathlib, I find myself staring at simple definitions not understanding what they are supposed to mean), I get something like:

variable (F V: Type*) [Field F] [AddCommGroup V] [Module F V]
example axler_1_40 {U V W: (Submodule F V)}: ∀ (x:V), x ∈ U.carrier ∨ x ∈ V.carrier → x ∈ W.carrier → (U + V).carrier ⊆ W.carrier := sorry

But not only doesn't this work, it's so set theoretic that it's certainly not the right way to express the proof statement and proofs in terms of carrier seem suspect anyway. Is this a one liner in Mathlib? What's the right way to express the proof statement?

[Arien Malec]

Arien Malec said:

Here, the aesop goal state is a garble

 DifferentiableAt ℝ (_uniq.201000 + _uniq.201001) _uniq.233268
⊢ HasDerivAt (_uniq.201000 + _uniq.201001) 0 2

It's possible I just need to update Mathlib?

Just tried to update Mathlib and same state.

[Timo Carlin-Burns]

Are you getting concerned because of the _uniq.N? I think those are just computer-generated variable names

[Timo Carlin-Burns]

That goal state is not necessarily indicative of a problem

[Patrick Massot]

It is definitely a bug in aseop, a missing context update.

[Patrick Massot]

@Arien Malec you are not getting help about your latest question because you didn’t provide a #mwe.

[Patrick Massot]

Otherwise I’d be happy to help.

[Arien Malec]

Thanks!

import Mathlib.Algebra.Module.Submodule.Basic
import Mathlib.Algebra.Module.Submodule.Pointwise


/-

Axler, Linear Algebra Done Right, Example 1.40:

"Suppose `𝑉_1, ..., 𝑉_𝑚` are subspaces of `𝑉`. Then `𝑉_1 + ⋯ + 𝑉_𝑚` is the smallest subspace of `𝑉`
containing `𝑉_1, ..., 𝑉_𝑚`."

We know `V_1 + ... + V_m` is a subspace because the `Submodule.pointwiseAddCommMonoid` instance
proves additive closure.

If we can prove the claim of "smallest" for pairs of subspaces `U` and `V` we can prove for arbitrary
additve chains by _waves hand_ *induction*
-/
open Pointwise

variable (F V: Type*) [Field F] [AddCommGroup V] [Module F V]
example {S T W: (Submodule F V)}: ∀ (x:V), (x ∈ S.carrier) ∨ (x ∈ T.carrier) → (x ∈ W.carrier) → (S + T).carrier ⊆ W.carrier := sorry

[Arien Malec]

The supplied translation is absolutely wrong for the reasons I mentioned above. The Axler paper proof is intuitive : "Conversely, every subspace of 𝑉 containing 𝑉1, ..., 𝑉𝑚 contains 𝑉1 + ⋯ + 𝑉𝑚 (because subspaces must contain all finite sums of their elements). Thus 𝑉1 +⋯+𝑉𝑚 is the smallest subspace of 𝑉 containing 𝑉1, ..., 𝑉𝑚."

[Arien Malec]

I don't even know the Mathlibism for proof over potentially countably infinite chains of operations. The computer scientist in me is content to think about this as recursion with the base case of a pair.

[Patrick Massot]

Why do you write all those carrier?

[Patrick Massot]

And you have several things called V

[Patrick Massot]

And you try to name an example so Lean is completely confused. Note that your binders choices are completely random but this isn’t a problem for an example since you cannot use it anyway.

[Patrick Massot]

You got your operator precedence wrong to. Your statement is not what you intended, even after fixing syntax issues.

[Arien Malec]

The textual proof claim is that V + U is the smallest subspace containing V and U. When I try to translate what "containing" is supposed to mean, I think I want "if v is in V then v is in W" or the type theoretic version of that. The carrier stuff is admittedly wrong -- as I wrote above: "But not only doesn't this work, it's so set theoretic that it's certainly not the right way to express the proof statement and proofs in terms of carrier seem suspect anyway."

[Arien Malec]

Fixed the syntax issues -- the V confusion hid the fact that example isn't named...

[Arien Malec]

Also parenthesized to make operator precedence clearer. But again, I'm not claiming this translation is correct -- the help I'm looking for is "what is the Mathlib statement that means "every subspace of 𝑉 containing 𝑉1, ..., 𝑉𝑚 contains 𝑉1 + ⋯ + 𝑉𝑚 ... thus 𝑉1 +⋯+𝑉𝑚 is the smallest subspace of 𝑉 containing 𝑉1, ..., 𝑉𝑚"

[Arien Malec]

(or the translation of that down to "every subspace of V containing V_1 and V_2 contains V_1 + V_2 thus....")

[Patrick Massot]

The parentheses are still wrong because the implication arrow is right-associative.

[Patrick Massot]

What you mean is

[Patrick Massot]

variable {F M : Type*} [Field F] [AddCommGroup M] [Module F M]

example {U V W : Submodule F M} : (∀ x : M, x ∈ U ∨ x ∈ V → x ∈ W) → U + V ≤ W

[Patrick Massot]

I don’t understand why aesop can’t do that without hand-holding.

example {U V W : Submodule F M} : (∀ x : M, x ∈ U ∨ x ∈ V → x ∈ W) → U + V ≤ W := by
  intros h
  simp
  constructor
  all_goals
  intro x hx
  aesop

[Patrick Massot]

Anyway the two lemmas you wanted are docs#Submodule.add_eq_sup and the very generic docs#sup_le_iff

[Patrick Massot]

The first one is getting rid of the pointwise addition stuff that is the very wrong way of thinking about this, and then it becomes a completely generic reasoning.

[Arien Malec]

:pray:

[Arien Malec]

Although I'm confused in general about Sup as a binary operator (rather than as a unary operator on a set), and in specific about how add_eq_sup in this case.... Any pointers to the underlying treatment here would be helpful.

[Patrick Massot]

Whenever the unary on the set version exists (which is a very strong assumption on an ordered type) then the binary one on elements a and b is the unary one on sets on {a, b}.

[Patrick Massot]

Maybe you should watch the beginning of https://www.slmath.org/summer-schools/1021/schedules/33442 which explains this stuff.

[Patrick Massot]

I think I mentioned the story of sums of subspaces during that lecture.

[Patrick Massot]

It also appears a bit in Chapter 8 of #mil when discussing subgroups.

[Arien Malec]

Thank you -- your lecture is incredibly helpful! There's so much embedded in the structure of Mathlib that, particularly in the exercise that I'm trying (formalizing second year linear algebra) I need to jump from the math that's in the text book to the more abstract concepts that Mathlib is built out of...