Direct Sums over vector spaces

Stream: new members

[Arien Malec]

Sorry to do this again, but I can't make heads or tails of the DirectSum notation.

The goal in Axler is to show that the direct sum of subspaces in F^3 {<x, y, 0>} ⊕ {<0, 0,z>} = F^3`

Here's where I got to, where the example is completely borked because I can't grok the syntax of direct sums in Mathlib

import Mathlib.Algebra.Module.Submodule.Basic
import Mathlib.Algebra.DirectSum.Basic
import Mathlib.Data.Fin.VecNotation

variable (F: Type*) [Field F]
def ex1_42_U: Submodule F (Fin 3 → F) where
  carrier := { ![x, y, y] | (x: F) (y: F) }
  add_mem' := by aesop
  smul_mem' := by aesop
  zero_mem' := by simp

def ex1_42_V: Submodule F (Fin 3 → F) where
  carrier := { ![0, 0, z] | (z: F)}
  add_mem' := by aesop
  smul_mem' := by aesop
  zero_mem' := by simp

open DirectSum
-- example: (⨁ (ex1_42_U) (ex1_42_V), f ex1_42_U ex1_42_V) = (Fin 3 → F) := by sorry

[Timo Carlin-Burns]

DirectSum operates on an indexed family of spaces. To use it on just two, use an indexing type of cardinality 2, such as Bool or Fin 2. You can express U ⨁ V as ⨁ i: Bool, if i then U else V

[Timo Carlin-Burns]

Or ⨁ i, ![U, V] i. Or DirectSum _ ![U, V]

[Timo Carlin-Burns]

Not sure what's preferred

[Eric Wieser]

Or U × V

[Eric Wieser]

Or since we're talking about subspaces, this is U ⊔ V, or perhaps IsCompl U V

[Kevin Buzzard]

@Arien Malec the definitions of things like sums, direct sums etc in mathlib are different to the ones used in Axler and this is a great example of the kind of problem you run into when you want to "go through a textbook in Lean". One approach which avoids all this confusion would be to just write your own definitions. Of course, if you do this, you'll discover why Lean's definitions are different -- Lean's definitions are chosen to be the ones which cause the least pain when using them in Lean. This is the problem you face with formalising a maths book.

[Patrick Massot]

This has nothing to do with Lean, Axler is using a very standard abuse of notations and here you simply need to be precise.

[Patrick Massot]

We could use the confusing notation in Lean but there is not much point doing it.

[Arien Malec]

It's funny -- I see any number of Github repositories of people trying to do the same thing as I, and generally bomb out at the end of Chapter 1.... I'm following a thread, which I can't find in the Zulip, that the most interesting way to do this would be to cover the same ground in Lean rather than translate too closely. This kind of gear meshing is the inevitable result.

[Arien Malec]

My approach is what @Scott Morrison recommended here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Showing.20a.20subset.20that's.20a.20vector.20space.20contains.20zero/near/365098675

[Arien Malec]

(which is the thread I was thinking of).

[Arien Malec]

And perhaps direct sums are not the right construct -- the definition Axler is looking for is something like: U ⊔ V ∧ U ∩ V = ∅

[Eric Wieser]

The LHS of your ∧ is not a proposition; it doesn't mean anything for "U ⊔ V" to be true.

[Eric Wieser]

And the RHS is always false, because even the "empty" vector space has a zero, so is not the empty set

[Eric Wieser]

docs#IsCompl is probably what you meant

[Arien Malec]

Probably -- the sense is that a vector space is composed of multiple disjoint vector spaces.

[Arien Malec]

Building to an intuition of a basis.

[Arien Malec]

Right, instead of empty I should have written {0}

[Eric Wieser]

U ∩ V = {0} would be written in mathlib as Disjoint U V (see docs#disjoint_iff for a proof this is the same)

[Arien Malec]

We want something like W = U ⊔ V ∧ U ∩ V = {0} then

[Eric Wieser]

Yes, and I told you how to spell exactly that in mathlib :)

[Arien Malec]

I'm still struggling with the setup to Axler's example above.... , that F^3 is the combination of the two disjoint subsets.

[Arien Malec]

So maybe the statement is: example: ((ex1_42_U ⊔ ex1_42_V) = Fin 3 → F) ∧ Disjoint ex1_42_U ex1_42_V := by sorry? But I can't get this to typecheck. Perhaps I'm missing an import...

[Arien Malec]

Parentheses and stuff, but Mathlib/Lean doesn't like turning a collection of Submodules into a Module

[Patrick Massot]

Arien I think you would have a much easier job if you could accept to first learn a bit about mathlib and then come back to your project. Guessing everything is not so fun. A lot of things are not documented but what you are struggling with is documented. I think there is not much point doing what you are doing without first reading the algebra chapter of #mil or some other resource covering the same material.

[Richard Copley]

With those defs, ex1_42_U isn't a submodule, ex1_42_U F is.

[Arien Malec]

Patrick Massot said:

Arien I think you would have a much easier job if you could accept to first learn a bit about mathlib and then come back to your project. Guessing everything is not so fun. A lot of things are not documented but what you are struggling with is documented. I think there is not much point doing what you are doing without first reading the algebra chapter of #mil or some other resource covering the same material.

I've read though #mil but not done the exercises. I'll commit to doing so. At the same time, I suspect that knowing the abstract algebra hierarchy will not lead to clarity in the gear meshing I'm working through...

[Patrick Massot]

It should be enough to get you to understand why (ex1_42_U ⊔ ex1_42_V) = Fin 3 → F is wrong.

[Patrick Massot]

I mean it stays wrong even after inserting the missing arguments.

[Arien Malec]

When I look at it, it's obviously wrong -- I should have written Module F (Fin 3 → F)

[Arien Malec]

Which is probably still wrong, but at least a more right sort of wrong.

[Arien Malec]

Perhaps I can approach this problem in a different direction. How would one say that (span(<1, 0, 0>) +span(<0,1,0>) + span(<0,0,1>)) = ℝ^3

[Patrick Massot]

This is not the issue, the issue is the right hand side of your (ex1_42_U ⊔ ex1_42_V) = Fin 3 → F

[Patrick Massot]

You need to put a submodule there.

[Arien Malec]

OK, now I'm super confused. The exercise that Axler is leading us through is to show that vector spaces are "composed of" subspaces each of which can be generated by a basis vector. In Mathlib, can we show that composition of subspaces that form the required vector space? We'd then want submodules on the LHS and a module on the RHS....

[Arien Malec]

I guess I've been super confused all along and now I just have a new dimension of confusion added.

[Patrick Massot]

I can see you are confused, that’s why I told you to read the explanations instead of trying to guess.

[Patrick Massot]

Or watch the lecture I mentioned earlier.

[Patrick Massot]

There is a submodule whose elements are all the elements of the ambiant module, and it’s name is Top.

[Patrick Massot]

So the statement you want is example: ex1_42_U F ⊔ ex1_42_V F = ⊤ ∧ Disjoint ex1_42_U ex1_42_V

[Patrick Massot]

where ⊤ is the notation for top.

[Arien Malec]

And ⊥ would be the submodule {0}?

[Eric Wieser]

Patrick Massot said:

So the statement you want is example: ex1_42_U F ⊔ ex1_42_V F = ⊤ ∧ Disjoint ex1_42_U ex1_42_V

Another spelling In mathlib for ex1_42_U F ⊔ ex1_42_V F = ⊤ is Codisjoint (ex1_42_U F) (ex1_42_V F), and combined with the ∧ Disjoint _ _ this is exactly IsCompl (ex1_42_U F) (ex1_42_V F)

[Eric Wieser]

(Not something you should care about now, but: the original problem in this thread of showing a vector space "is" a direct sum of two subspaces ends up being more complicated if you start talking about semimodules instead of vector spaces, and the sup / inf / IsCompl spellings no longer work! I can say more once you've solved your current exercise)

[Arien Malec]

I made things slightly easier on myself to see the shape of the proof rather than faffing with the right use and have this down to

import Mathlib

variable (F: Type*) [Field F]
def ex1_42_U: Submodule F (Fin 3 → F) where
  carrier := { ![x, y, 0] | (x: F) (y: F) }
  add_mem' := by aesop
  smul_mem' := by aesop
  zero_mem' := by simp

def ex1_42_V: Submodule F (Fin 3 → F) where
  carrier := { ![0, 0, z] | (z: F)}
  add_mem' := by aesop
  smul_mem' := by aesop
  zero_mem' := by simp

example: (ex1_42_U F ⊔ ex1_42_V F) = ⊤ ∧ Disjoint (ex1_42_U F) (ex1_42_V F) := by
  constructor
  . rw [Submodule.eq_top_iff']
    intro x
    rw [Submodule.mem_sup]
    use ![x 0, x 1, 0]
    constructor
    . sorry
    . use ![0, 0, x 2]
      constructor
      . sorry
      . simp
        ext f
        fin_cases f <;> simp ; aesop
  . rw [disjoint_iff, Submodule.eq_bot_iff (ex1_42_U F ⊓ ex1_42_V F)]
    intro x h
    cases' h with h1 h2
    ext f
    fin_cases f <;>
    simp <;>
    rcases h1 with ⟨x₁, x₂, h1⟩ <;>
    rcases h2 with ⟨x₃, h2⟩
    . rw [←h2]; simp
    . rw [←h2]; simp
    . rw [←h1]; simp

where the two sorrys have the same shape: proof of membership in the subset....

[Arien Malec]

But I don't know how to prove membership in a Submodule

[Eric Wieser]

Your issue is that you made a new def, but didn't tell Lean anything about it

[Richard Osborn]

You'll want to unfold ex1_42_U and unfold ex1_42_V.

[Eric Wieser]

Or better yet,

theorem mem_ex1_42_U_iff {x} : x ∈ ex1_42_U F ↔ x ∈ { ![x, y, 0] | (x: F) (y: F) } := Iff.rfl

[Eric Wieser]

Unfolding gives you a monstrosity thanks to nested structures, and set_option pp.proofs.withType false not being the default

[Richard Osborn]

Yea, though simp or aesop clean it up nicely.

[Arien Malec]

Eric Wieser said:

Or better yet,

theorem mem_ex1_42_U_iff {x} : x ∈ ex1_42_U F ↔ x ∈ { ![x, y, 0] | (x: F) (y: F) } := Iff.rfl

Is there any way to make this generic over Submodule F (Fin 3 → F)

[Eric Wieser]

No, in the same way that it's not possible to generalize:

def foo : Set Nat := {1, 2, 3}

theorem mem_foo (n : Nat) : n ∈ foo ↔ n ∈ {1, 2, 3}

[Eric Wieser]

It would be reasonable to ask something to autogenerate mem_foo and mem_ex1_42_U_iff, but that's not the same as generalization

[Arien Malec]

I see -- at some point we need to expand the definition of the carrier....

[Eric Wieser]

Yes, exactly; either by unfold, which makes a mess, or by writing a lemma that does exactly the expansion you want

[Eric Wieser]

In many cases @[simps] could do this, but it doesn't know about \mem

[Arien Malec]

OK, can I repeat back what I've learned here, to check for understanding:

Mathlib uses the fact that the submodules of a module form a complete lattice to generalize the proofs around modules to proofs of lattice structures; in particular, Mathlib uses the ⊔ (least upper bound) operator, or lattice join, to represent sums of submodules. What Axler terms the Direct Sum is, in Mathlib, the statement that the least upper bound of submodules is ⊤ (AKA the submodule identical to the module) along with the assertion that the submodules are disjoint.

[Arien Malec]

(these last are packaged into the statement IsCompl)

[Eric Wieser]

Note that you're not using the fact that the lattice is complete in this case, as you only used finite lattice meets / joins

[Eric Wieser]

That sounds like a fair summary to me

[Arien Malec]

We'd use the complete versions if we were dealing with infinite dimensional vector spaces?

[Eric Wieser]

No, only if you were talking about an infinite family of submodules rather than just two

[Arien Malec]

I'd like to recover Axler's original definition: "The sum 𝑉_1 + ⋯ + 𝑉_𝑚 is called a direct sum if each element of 𝑉_1 + ⋯ + 𝑉_𝑚 can be written in only one way as a sum 𝑣_1 + ⋯ + 𝑣_𝑚, where each 𝑣_𝑘 ∈ 𝑉_𝑘"

The existence of such a sum is given in docs#Submodule.mem_sup -- is there any ready made proof for the uniqueness of that sum? (My intuition is that if the existence runs through Codisjoint the uniqueness runs through Disjoint but where I see a proof that the left and right of IsCompl are unique (e.g., docs#IsCompl.right_unique) I don't see anything obvious that leads to the proof that the sum is unique).

[Eric Wieser]

I think the literal interpretation of this is to show that Function.bijective (LinearMap.coprod P.subtype Q.subtype : P × Q →ₗ[R] M)

[Eric Wieser]

(docs#LinearMap.coprod)

[Eric Wieser]

Which says "there is a two-sided inverse to the map that adds together the two pieces"

[Eric Wieser]

(this is also the solution to the semimodule version I alluded to above)