vector spaces

Stream: new members

[bumby bumby]

hi i m new in lean i m reading mathematics in lean, what libraries can i use to prove general vector spaces or if a set is a vector space? because in the book explains for rings but i see those are little different that vector spaces

[Anne Baanen]

Hi, welcome! We have a quick tour through the linear algebra library of mathlib here: https://leanprover-community.github.io/theories/linear_algebra.html

So I understand your question as: "I have a set V along with some operations + and •, how can I show this is a vector space?"

[Kevin Buzzard]

A "thing" isn't a vector space by itself, you have to make it a vector space by defining stuff like addition and multiplication. I think this conversation would be easier if we focussed on a much more precise question.

[Eric Wieser]

You'll probably end up wanting docs#vector_space (aka docs#module aka docs#semimodule), but I think it would be valuable for you to expand on your question

[Anne Baanen]

Or maybe docs#submodule since we're starting with a set.

[bumby bumby]

exactly

[Johan Commelin]

@bumby bumby Have you played the natural number game? It's a great way to get started with Lean.

[bumby bumby]

i started reading mathematics_in_lean and is great i started prove small theorems of real numbers

[bumby bumby]

interesting i will try thanks

[Esteban Estupinan]

hi zulip members, I comment you I m trying prove that the intersection of subspaces of a vector space is another subspace. I was reading some of indexed families in logic and proof book to write the collection of subspaces in lean. I think it is right in my code. I have a little idea to prove. The problem is that I dont know how introduce W as the intersection of the subspaces. I think this should be written in the "carrier" part of the code. I would appreciate a lot if you can help me in this part, I give you my code

[Esteban Estupinan]

import linear_algebra.basic

variables {R V I : Type*}

theorem t14 [field R] [add_comm_group V] [module R V]
{C: I → submodule R V} : submodule R V :=
{ carrier   := {},
  zero_mem' :=
      begin

      end,
    add_mem' :=
      begin

      end,
    smul_mem' :=
      begin

      end, }

[Alex J. Best]

Sure, as you say the carrier should be the intersection of the carriers of the submodules in C, if we write that lean will insert the right coercion from the submodules to sets for us:

import linear_algebra.basic

variables {R V I : Type*}

theorem t14 [field R] [add_comm_group V] [module R V]
{C: I → submodule R V} : submodule R V :=
{ carrier   := ⋂ i, C i,
  zero_mem' :=
      begin

      end,
    add_mem' :=
      begin

      end,
    smul_mem' :=
      begin

      end, }

[Alex J. Best]

This should really be a def rather than a theorem I guess, as you are reallly defining the intersection of submodules as a submodule here.

[Kevin Buzzard]

I think that the morally correct and least confusing way to formalise such a question would be using unbundled subspaces. One could define is_subspace (S : set V) to be the predicate that S is (the underlying subset of) a subspace and then use set lemmas to prove the result. This is not how these things are handled in Lean but it seems to be easier to understand than our approach.

[Esteban Estupinan]

ok, after intro some hypothesis, I don't know if it's correct but I wanted using the simp only tactic maybe to simplify the general intersections and using rw tactic better, It is posible use simp only tactic with some Inter theorem ? if is not what would be another alternative?

[Esteban Estupinan]

import linear_algebra.basic

variables {R V I : Type*}

theorem t14 [field R] [add_comm_group V] [module R V]
{C: I → submodule R V} : submodule R V :=
{ carrier   := ⋂ i, C i,
  zero_mem' :=
      begin
       simp only [] at ⊢,
       rw
      end,
    add_mem' :=
      begin
        intros x y hx hy,
        simp only [] at hx hy ⊢,
        rw
      end,
    smul_mem' :=
      begin
        intros c x hx,
        simp only [] at hx ⊢,
        rw
      end, }

[Eric Wieser]

Does simp only do anything at all here? simp is far more likely to be helpful

[Esteban Estupinan]

hi how are you, i'm trying to prove the following 3 theorems related to subspaces. first I started entering the hypothesis and thesis here I notice that there is a common error, especially when entering the "if and only if". Please if someone can help me to see what is wrong and how I can correct it this first part, thank you very much

[Esteban Estupinan]

imagen.png

[Eric Wieser]

What exactly do you mean? We can't help you with an error if you don't show the error.

[Esteban Estupinan]

now the codes

[Esteban Estupinan]

import linear_algebra.basic

variables {R V W : Type*}

theorem e18 [field R] [add_comm_group V] [module R V]
{x y : W} {a : R} (W ≠ ∅) : submodule R V ↔ (a * x ∈ W) ∧ (x + y ∈ W)
{ carrier   := W ⊆ V,
  zero_mem' :=
      begin

      end,
    add_mem' :=
      begin

      end,
    smul_mem' :=
      begin

      end, }

[Eric Wieser]

(ah - you might not be aware there's a "press enter to send" checkbox at the bottom right that lets you put multiple lines in a single message)

[Esteban Estupinan]

ok a wil try

[Eric Wieser]

If you're doing 18, why do you have W ≠ ∅ which is an assumption from 17?

[Patrick Massot]

You messed up the quantifiers

[Patrick Massot]

But the text you are following is pretty sloppy with quantifiers, so this is not too suprising.

[Esteban Estupinan]

the code is of 17 and here is w is empty

[Eric Wieser]

Why did you call it e18 if it's for 17?

[Esteban Estupinan]

ups is error because in vsc I have with 17 sorry

[Eric Wieser]

Your syntax errors are:

• Hypotheses needs names. It should be (hW : W ≠ ∅) not (W ≠ ∅)
• The format should be statement := proof not statement proof- you're missing the :=

[Patrick Massot]

I think the math errors are much more serious here.

[Eric Wieser]

I agree the math errors are also bad, but there's no hope of getting the binders right if you don't even know the syntax for binders well enough.

[Eric Wieser]

Part of your trouble here is that submodule is not used in the same way as "is a submodule". A rough translation of "is a submodule" is:

/-- The set `W` is a submodule of `V` if there exists a submodule `W'` whose elements are equal to
`W`. -/
abbreviation is_submodule (W : set V) : Prop := ∃ W' : submodule R V, W = ↑W'

[Esteban Estupinan]

the part of carrier until the end is correct?

[Eric Wieser]

Until you have the statement written down, that question isn't even meaningful - right now it's nonsense. You should start off by writing

lemma e17 (your assumptions) : your_statement := sorry

Only once lean accepts that you should you try to replace the sorry with a proof.

[Esteban Estupinan]

ok I will try

[Esteban Estupinan]

amm i tried it but I keep getting errors

import linear_algebra.basic

variables {R V W : Type*}

lemma e17 [field R] [add_comm_group V] [module R V]
(W set : V) : ∃ W' : submodule R V, W = ↑W' ↔ W ≠ ∅ := sorry

[Eric Wieser]

(W set : V) means "let W be a V and let setbe a V"

[Patrick Massot]

Esteban, I think you need to work much more on the basic syntax of Lean before trying to prove anything in linear algebra. Did you try any of the learning resources listed on https://leanprover-community.github.io/learn.html?

[Patrick Massot]

Otherwise you'll only gain frustration.

[Esteban Estupinan]

i trying proof set theory and with help few linear algebra

[Esteban Estupinan]

Lean has helped me to be more precise in the mathematical demonstrations like today that in the book they do not mention quantifiers or Eric Wieser's explanation of the sub-modules, thanks. I have a confusion, for each github project it is advisable to create an independent project in lean, right?

[Eric Wieser]

I think you're running into trouble because you're having to learn the lean syntax and the mathlib linear algebra library and what it means to state theorems precisely all at once. I agree with Patrick, you would do well to try out one of the many lean tutorial / exercise projects rather than picking your own problems to formalize.

[Esteban Estupinan]

Could you please tell me if the following reasoning is correct? To understand the theorem 1.9 red underline, I supposed start reasoning from the thesis of the theorem 1.5 ( stating that span (beta) contains span (S) = V) like "apply" tactic in lean, so to prove this thesis I need to prove the hipothesis, that I think is "show that S is subset of span(beta)", is correct this backward reasonning? thank you for your answers imagen.png imagen.png

[Eric Wieser]

Have you managed to state theorem 1.9 in lean?

[Esteban Estupinan]

not yet though i wish i could. First I wanted to see if my reasoning was correct and maybe then pass it on Lean

[Martin Dvořák]

The informal proof seems correct to me. Just be careful that β in Theorem 1.9 corresponds to S in Theorem 1.5

[Martin Dvořák]

IMO, the part that is underlined in red will be easy to formalize. I am more worried about not knowing how to formalize the local definition of β.