How to work with LinearIndependent?

Stream: new members

[Abdullah Uyu]

How can I prove this?

import Mathlib.LinearAlgebra.Projectivization.Basic

variable [DivisionRing K] [AddCommGroup V] [Module K V]

theorem l2_rep (a b p q : V) : ¬ LinearIndependent K ![a, p, q] ->
¬ LinearIndependent K ![b, p, q] -> LinearIndependent K ![p, q] ->
¬ LinearIndependent K ![a, b, p] := by
sorry

[Abdullah Uyu]

Maybe I should start with a less intimidating goal. How can I prove something like this?

import Mathlib.LinearAlgebra.Projectivization.Basic

variable [DivisionRing K] [AddCommGroup V] [Module K V]

theorem lindep_imp_span (a b c : V) : ¬ LinearIndependent K ![a, b, c] →
a ∈ Submodule.span K {b, c} := by sorry

[Jireh Loreaux]

That's not true? Consider b = c and a which is not a scalar multiple of them.

[Jireh Loreaux]

Did you mean to assume that b and c a linearly independent?

[Jireh Loreaux]

I think you want to apply docs#not_iff_not to docs#linearIndependent_fin_succ

[Jireh Loreaux]

import Mathlib.LinearAlgebra.LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V]

theorem lindep_imp_span (a b c : V) (h₁ : LinearIndependent K ![b, c])
    (h₂ : ¬ LinearIndependent K ![a, b, c]) : a ∈ Submodule.span K {b, c} := by
  rw [not_iff_not.mpr linearIndependent_fin_succ] at h₂
  push_neg at h₂
  simp only [Fin.isValue, Matrix.cons_val_zero] at h₂
  convert h₂ h₁
  ext x
  simp [show Fin.tail ![a, b, c] = ![b, c] from rfl]
  rw [or_comm]

[Abdullah Uyu]

Jireh Loreaux said:

That's not true? Consider b = c and a which is not a scalar multiple of them.

Yep, late night confusion I guess. band cbeing linearly independent is fine. Thank you!

[Abdullah Uyu]

Here is my progression so far:

theorem l2_rep (a b p q : V) (apq_dep : ¬ LinearIndependent K ![a, p, q])
(bpq_dep : ¬ LinearIndependent K ![b, p, q]) (pq_indep : LinearIndependent K ![p, q]) :
¬ LinearIndependent K ![a, b, p] := by
have a_span_pq : a ∈ Submodule.span K {p, q} := by {
apply lin_dep_imp_span a p q pq_indep apq_dep
}
have b_span_pq : b ∈ Submodule.span K {p, q} := by {
apply lin_dep_imp_span b p q pq_indep bpq_dep
}
have ppq_dep : ¬ LinearIndependent K ![p, p, q] := by apply (lin_dep_aab p q)
have qpq_dep : ¬ LinearIndependent K ![q, p, q] := by apply (lin_dep_bab q p)
have p_span_pq : p ∈ Submodule.span K {p, q} := by {
apply lin_dep_imp_span p p q pq_indep ppq_dep
}
have q_span_pq : q ∈ Submodule.span K {p, q} := by {
apply lin_dep_imp_span q p q pq_indep qpq_dep
}

I have $a,b,p,q$ in the span of $p,q$. Now I want to say that any three of $a,b,p,q$ is linearly dependent, and conclude that $a,b,p$ are linearly dependent. @Jireh Loreaux Do we have such a lemma in the library, I couldn't find any.

[Abdullah Uyu]

To reformulate: Any family from a span is linearly dependent.

[Sophie Morel]

It's true because the span of p, qis at most 2 (cf finrank_span_finset_le_card) and a family of linearly independent vectors has cardinal at most the dimension (cf LinearIndependent.finset_card_le_finrank). I doubt there is a direct lemma doing exactly what you want.

[Abdullah Uyu]

Oh, I never thought cardinalities would be useful here. But of course, yeah. Thank you, I'll try this direction.

[Abdullah Uyu]

Sophie Morel said:

It's true because the span of p, qis at most 2 (cf finrank_span_finset_le_card) and a family of linearly independent vectors has cardinal at most the dimension (cf LinearIndependent.finset_card_le_finrank). I doubt there is a direct lemma doing exactly what you want.

Why does Lean fail to convert this Set to a Finset?

import Mathlib.LinearAlgebra.Basic

open Set

variable [AddCommGroup V]

variable (p q : V)
def a : Finset V := toFinset {p, q}
-- failed to synthesize instance
--   Fintype ↑{p, q}

[Kevin Buzzard]

You can see the error. Fintype and Finset are constructive so maybe you need some constructivist stuff to make it work. Does adding [DecidableEq V] help? Maybe the issue is that Lean doesn't know if p=q which will stop it from proving that {p,q} is constructively finite.

[Sophie Morel]

If you add [DecidableEq V], then you can just write

def a : Finset V := {p,q}

[Abdullah Uyu]

Kevin Buzzard said:

You can see the error. Fintype and Finset are constructive so maybe you need some constructivist stuff to make it work. Does adding [DecidableEq V] help? Maybe the issue is that Lean doesn't know if p=q which will stop it from proving that {p,q} is constructively finite.

Yes, that works. Also yes, I actually can get $p \neq q$ in the original context. Although, I guess I have some other problem there, will write more soon.

[Abdullah Uyu]

Sophie Morel said:

If you add [DecidableEq V], then you can just write

def a : Finset V := {p,q}

That's handy.

[Eric Wieser]

If you have that p and q are different, you could also use docs#Finset.cons instead of set notation, which avoids the decidable instance; but either spelling is fine

[Abdullah Uyu]

Sophie Morel said:

It's true because the span of p, qis at most 2 (cf finrank_span_finset_le_card) and a family of linearly independent vectors has cardinal at most the dimension (cf LinearIndependent.finset_card_le_finrank). I doubt there is a direct lemma doing exactly what you want.

I figured out the fist one:

import Mathlib.LinearAlgebra.FiniteDimensional

open Finset Submodule FiniteDimensional LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V] [DecidableEq V]

theorem pq_span_dim_ineq (p q : V) (pq_diff : p ≠ q) : Set.finrank (R := K) (toSet {p, q}) ≤ 2 := by
have pq_card : (card {p, q}) = 2 := by aesop
rw [<- pq_card]
apply finrank_span_finset_le_card {p, q}

In the second one, I am a bit tired at:

import Mathlib.LinearAlgebra.FiniteDimensional

open Finset Submodule FiniteDimensional LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V] [DecidableEq V]

theorem abp_rank_le_span_rank (a b p q : V)
(pq_diff : p ≠ q)
(abp_indep : LinearIndependent K ![a, b, p])
(a_span_pq : a ∈ span K {p, q})
(b_span_pq : b ∈ span K {p, q}) :
(card {a, b, p}) ≤ finrank K (span K {p, q}) := by
apply finset_card_le_finrank (R := K) (M := (span K {p, q})) {a, b, p}
-- failed to synthesize instance
--   Module.Finite K ↥(span K {p, q})

Should I chase something like:

instance (p q : V) : Module.Finite (R := K) (M := span K {p, q}) :=

[Sophie Morel]

You can add something like

set M := span K ({p, q} : Finset V).toSet
letI : FiniteDimensional K M := span_finset _ _

in your code to get the instance, but you'll also have to prove that a,b,p are linearly independent in M and not in V to give to finset_card_le_finrank as an argument. You can use LinearIndependent.of_comp M.subtype for this. (Maybe there is a better solution, I don't know.)

[Abdullah Uyu]

Sophie Morel said:

You can add something like

set M := span K ({p, q} : Finset V).toSet
letI : FiniteDimensional K M := span_finset _ _

in your code to get the instance, but you'll also have to prove that a,b,p are linearly independent in M and not in V to give to finset_card_le_finrank as an argument. You can use LinearIndependent.of_comp M.subtype for this. (Maybe there is a better solution, I don't know.)

Hmm, this became a bit tricky, but you mean that I put these after by, right?

theorem abp_rank_le_span_rank (a b p q : V)
(pq_diff : p ≠ q)
(abp_indep : LinearIndependent K ![a, b, p])
(a_span_pq : a ∈ span K {p, q})
(b_span_pq : b ∈ span K {p, q}) :
(card {a, b, p}) ≤ finrank K (span K {p, q}) := by
set M := span K ({p, q} : Finset V).toSet
letI : FiniteDimensional K M := span_finset K {p, q}
apply finset_card_le_finrank (R := K) (M := (span K {p, q})) {a, b, p}

Like this?

[Abdullah Uyu]

Oh, I never passed it to finset_card_le_finrank. I should look at this a bit more.

[Sophie Morel]

Yes, I meant that you put the letI lines after by. It lets you introduce an instance to be used during a proof (and then forgotten).

[Abdullah Uyu]

There only left to rectify the type of the {a, b, p} in the declaration. It should also be of Finset M, so I also need M before by. I tried to put it there hard-coded for testing purposes, but I now get this:

theorem abp_rank_le_span_rank (a b p q : V)
(pq_diff : p ≠ q)
(abp_indep : LinearIndependent K ![a, b, p])
(a_span_pq : a ∈ (span K ({p, q} : Finset V).toSet))
(b_span_pq : b ∈ (span K ({p, q} : Finset V).toSet)) :
({a, b, p} : Finset (span K ({p, q} : Finset V).toSet)).card ≤
finrank K (span K ({p, q} : Finset V).toSet) := by
set M := span K ({p, q} : Finset V).toSet
letI : FiniteDimensional K M := span_finset K {p, q}
apply finset_card_le_finrank (R := K) (M := M) {a, b, p}
-- overloaded, errors
--   failed to synthesize instance
--     Singleton V (Finset ↥(span K ↑{p, q}))
--
--   32:2 'a' is not a field of structure 'Finset'

[Abdullah Uyu]

So, if I am understanding correctly, the problem is arising from the fact that a is of type V, and I should somehow point to the fact I have (a_span_pq : a ∈ (span K ({p, q} : Finset V).toSet)).

[Jireh Loreaux]

Sophie Morel said:

Yes, I meant that you put the letI lines after by. It lets you introduce an instance to be used during a proof (and then forgotten).

For that you generally just want let. The `letI| additionally inlines the instance, which is not always desirable.

Note also, the meaning of letI changed between Lean 3 and Lean 4

[Jireh Loreaux]

Oh, and in this case you can just use have because the instance doesn't contain any data.

[Sophie Morel]

Ah, nice, I didn't know that let was enough!
I didn't know what it means to "inline" an instance, so I looked stuff up and found this; is it the same meaning?

[Jireh Loreaux]

Yes.

[Abdullah Uyu]

If I start with a b with type span, then I can apply the theorem, but then of course I lose my original form. I will post that example when I got home.

[Abdullah Uyu]

I guess I need some kind of type casting for this?

[Abdullah Uyu]

So let me post the example I talked above @Sophie Morel and @Jireh Loreaux . This one works:

theorem test (p q : V) (a b : (span K ({p, q} : Finset V).toSet)) (ab_neq : a ≠ b):
({a, b} : Finset (span K ({p, q} : Finset V).toSet)).card = 2 := by aesop

If I forget about the hypothesis for now and focus on the types: I want to make the following type-check:

theorem abp_rank_le_span_rank (a b p q : V) :
({a, b} : Finset (span K ({p, q} : Finset V).toSet)).card ≤
finrank K (span K ({p, q} : Finset V).toSet) := by
set M := span K ({p, q} : Finset V).toSet
letI : FiniteDimensional K M := span_finset K {p, q}
apply finset_card_le_finrank (R := K) (M := M) {a, b}
-- overloaded, errors
--   failed to synthesize instance
--     Singleton V (Finset ↥(span K ↑{p, q}))
--
--   28:2 'a' is not a field of structure 'Finset'

[Jireh Loreaux]

On the third line, is that docs#Set.finrank or docs#FiniteDimensional.finrank ?

[Jireh Loreaux]

Because the lemma to you are applying is apparently docs#LinearIndependent.finset_card_le_finrank, which is about the latter of these.

[Abdullah Uyu]

Right now I'm outside, so i can't look at my source, but yes, that should be the case. I'm also checking above the open line, and I think I never opened Set.

[Jireh Loreaux]

So which one is on the third line?

[Abdullah Uyu]

Sorry, just realized my wording was implicit. Checked now, it's FiniteDimensional.finrank.

[Sophie Morel]

On the second line, the expression ({a, b} : Finset (span K ({p, q} : Finset V) is not well-typed, as a and b are of type V, not of type span K ({p,q} : Finset V).toSet. Also, you cannot apply finset_card_le_finrank if you don't assume that a and b are linearly independent.
Finally, when you post code like that, please include all imports, open namespaces and variable declarations, otherwise I have to guess myself what you have opened if I want to play with the code (and, as Jireh pointed, if we don't know which namespaces are open then some expressions become ambiguous). This wastes a lot of time, and I will not do it again. Here your problem might just be that you forgot to declare [DecidableEq V], but I cannot tell because you did not include that part.

[Sophie Morel]

To prove that the subspace generated by p and q is finite-dimensional, I am really starting to think that it would be easier to use Module.Finite.span_of_finite, so you can write Submodule.span K {p,q} (but you'll have to prove that Set.Finite {p,q}, which should not be hard).

[Kevin Buzzard]

Yes this post is a great example of why #mwe s are important. Right now most of the comments here are asking for clarifications of the code; this would not have been necessary if a mwe was posted first time around. And it's still not too late to post one!

[Abdullah Uyu]

Lesson learned :saluting_face: Here it is:

import Mathlib.LinearAlgebra.FiniteDimensional

open Finset Submodule FiniteDimensional LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V] [DecidableEq V]

theorem abp_rank_le_span_rank (a b p q : V)
(pq_neq : p ≠ q)
(abp_indep : LinearIndependent K ![a, b, p])
(a_span_pq : a ∈ (span K ({p, q} : Finset V).toSet))
(b_span_pq : b ∈ (span K ({p, q} : Finset V).toSet)) :
({a, b, p} : Finset (span K ({p, q} : Finset V).toSet)).card ≤
finrank K (span K ({p, q} : Finset V).toSet) := by
set M := span K ({p, q} : Finset V).toSet
letI : FiniteDimensional K M := span_finset K {p, q}
apply finset_card_le_finrank (R := K) (M := M) {a, b, p}
-- overloaded, errors
--   failed to synthesize instance
--     Singleton V (Finset ↥(span K ↑{p, q}))
--
--   28:2 'a' is not a field of structure 'Finset'

[Abdullah Uyu]

Sophie Morel said:

To prove that the subspace generated by p and q is finite-dimensional, I am really starting to think that it would be easier to use Module.Finite.span_of_finite, so you can write Submodule.span K {p,q} (but you'll have to prove that Set.Finite {p,q}, which should not be hard).

Alright, thank you. I will look into this.

[Abdullah Uyu]

This has follow-ups but let me start with the following, hopefully this time with proper mwes. I proved submodule generated by p and q is finite dimensional.

import Mathlib.LinearAlgebra.FiniteDimensional

open Submodule FiniteDimensional

variable [DivisionRing K] [AddCommGroup V] [Module K V]

theorem pq_subspace_finite
(p q : V) :
Module.Finite K (span K {p, q}) := by
apply Module.Finite.span_of_finite
aesop -- proves Set.Finite {p,q}

But there are a few things that surprised me. The first is that this didn't need [DecidableEq V]. The second is that Module.Finite.span_of_finite worked without providing {p, q} as a parameter. Last but not least, providing it explicitly returned the following error in the comment:

import Mathlib.LinearAlgebra.FiniteDimensional

open Submodule FiniteDimensional

variable [DivisionRing K] [AddCommGroup V] [Module K V]

theorem pq_subspace_finite
(p q : V) :
Module.Finite K (span K {p, q}) := by
(apply Module.Finite.span_of_finite {p, q})
aesop -- proves Set.Finite {p,q}
-- overloaded, errors
--   failed to synthesize instance
--     Singleton V (Type ?u.1977)
--
--   invalid {...} notation, expected type is not of the form (C ...)
--     Type ?u.1977

What does Lean inferred as parameter there, how did Lean do it?

[Kevin Buzzard]

You only need DecidableEq if you're doing constructivist stuff, which you're not doing.

apply Module.Finite.span_of_finite {p, q} is nonsense because the first thing Module.Finite.span_of_finite wants to eat is (hA : Set.Finite A) (edit : R : Type*) and you've given it {p, q} which is not a term of that type, so Lean is just completely confused.

[Kevin Buzzard]

By the way, the usual way to do the indentation is this:

theorem pq_subspace_finite  (p q : V) :
    Module.Finite K (span K {p, q}) := by
  apply Module.Finite.span_of_finite
  aesop

[Richard Copley]

@Abdullah Uyu, if you look up the parameters of docs#Module.Finite.span_of_finite, you will see that the explicit parameters are R (the semiring for the module) and hA (the proof that A is a finite set).

In your first example, R can be deduced (by comparing, on the one hand, the expected type Module.Finite K ↥(Submodule.span K {p, q}), and on the other hand, the resulting type Module.Finite R ↥(Submodule.span R A) from Module.Finite.span_of_finite). The implicit arguments can all be deduced or inferred too, leaving only the goal Set.Finite {p, q}, which aesop proves. (exact? would also have given you a proof.)

In your second example, you supplied {p, q} for the explicit parameter R : Type*.

The error message says:

-- overloaded, errors

Lean tried to elaborate the notation {p, q} in more than one way (it is overloaded notation), but none succeeded.

--   failed to synthesize instance
--     Singleton V (Type ?u.1977)

First, it tried to interpret {p, q} as set-builder notation. It was unable to deduce the element type, and in consequence was unable to infer the Singleton type class for the element type; that type class is needed for set-builder notation, so the attempt failed.

--   invalid {...} notation, expected type is not of the form (C ...)
--     Type ?u.1977

The error message for the second attempt is not very good, but it doesn't matter: Lean tried something else, and that didn't work either.

This works:

import Mathlib.LinearAlgebra.FiniteDimensional

theorem pq_subspace_finite [DivisionRing K] [AddCommGroup V] [Module K V] (p q : V) :
    Module.Finite K (Submodule.span K {p, q}) := by
  exact Module.Finite.span_of_finite K (Set.toFinite {p, q})

[Abdullah Uyu]

Richard Copley said:

Abdullah Uyu, if you look up the parameters of docs#Module.Finite.span_of_finite, you will see that the explicit parameters are R (the semiring for the module) and hA (the proof that A is a finite set).

In your first example, R can be deduced (by comparing, on the one hand, the expected type Module.Finite K ↥(Submodule.span K {p, q}), and on the other hand, the resulting type Module.Finite R ↥(Submodule.span R A) from Module.Finite.span_of_finite). The implicit arguments can all be deduced or inferred too, leaving only the goal Set.Finite {p, q}, which aesop proves. (exact? would also have given you a proof.)

In your second example, you supplied {p, q} for the explicit parameter R : Type*.

The error message says:

-- overloaded, errors

Lean tried to elaborate the notation {p, q} in more than one way (it is overloaded notation), but none succeeded.

--   failed to synthesize instance
--     Singleton V (Type ?u.1977)

First, it tried to interpret {p, q} as set-builder notation. It was unable to deduce the element type, and in consequence was unable to infer the Singleton type class for the element type; that type class is needed for set-builder notation, so the attempt failed.

--   invalid {...} notation, expected type is not of the form (C ...)
--     Type ?u.1977

The error message for the second attempt is not very good, but it doesn't matter: Lean tried something else, and that didn't work either.

This works:

import Mathlib.LinearAlgebra.FiniteDimensional

theorem pq_subspace_finite [DivisionRing K] [AddCommGroup V] [Module K V] (p q : V) :
    Module.Finite K (Submodule.span K {p, q}) := by
  exact Module.Finite.span_of_finite K (Set.toFinite {p, q})

Thank you so much, it it much more clear now! I should sit and read some basics apparently, going intuitively has limited efficiency.

[Abdullah Uyu]

Let me then continue with this: I can now pass the instance Module.Finite K (Submodule.span K {p, q}) to my ultimate theorem:

import Mathlib.LinearAlgebra.FiniteDimensional

open Finset Submodule FiniteDimensional LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V] [DecidableEq V]

theorem pq_subspace_finite (p q : V) :
    Module.Finite K (Submodule.span K {p, q}) := by
  exact Module.Finite.span_of_finite K (Set.toFinite {p, q})

theorem abp_card_le_span_rank
    (a b p q : V)
    (finite_submodule_instance := pq_subspace_finite (K := K) (V := V) p q)
    (pq_neq : p ≠ q)
    (abp_indep : LinearIndependent K ![a, b, p])
    (a_span_pq : a ∈ (span K {p, q}))
    (b_span_pq : b ∈ (span K {p, q})) :
    (card {a, b, p}) ≤ finrank K (span K {p, q}) := by
  apply finset_card_le_finrank (R := K) (M := (span K {p, q})) {a, b, p}
  -- tactic 'apply' failed, failed to unify
  --   ?m.9988.card ≤ finrank K ↥(span K {p, q})
  -- with
  --   {a, b, p}.card ≤ finrank K ↥(span K {p, q})

Though, I still don't quite know how to state {a, b, p} as a finite set of (span K {p, q}).

[Richard Copley]

You could probably use something like this:

  have p_span_pq : p ∈ span K {p, q} := Submodule.subset_span (Set.mem_insert p {q})
  let s : Finset (span K {p, q}) := {⟨a, a_span_pq⟩, ⟨b, b_span_pq⟩, ⟨p, p_span_pq⟩}
  have : s.card = Finset.card {a, b, p} := by
    rw [← Finset.card_image_of_injective s Subtype.val_injective]
    aesop

[Abdullah Uyu]

Lean didn't automatically use the equality let introduced there, so I had to explicitly rewrite. Nevertheless, that worked like a charm. That syntax will be handy in my future struggles.

I will now have to supply the condition that a, b, p are linearly independent in span K {p, q}. So I will somehow convert my hypothesis LinearIndependent K ![a, b, p]. With a sorry, I wrote:

import Mathlib.LinearAlgebra.FiniteDimensional

open Finset Submodule FiniteDimensional LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V] [DecidableEq V]

theorem pq_subspace_finite (p q : V) :
    Module.Finite K (Submodule.span K {p, q}) := by
  exact Module.Finite.span_of_finite K (Set.toFinite {p, q})

def indexer
  (a b p q : V)
  (a_span_pq : a ∈ (span K {p, q}))
  (b_span_pq : b ∈ (span K {p, q}))
  (p_span_pq : p ∈ (span K {p, q})) :
    Fin 3 → (span K {p, q}) :=
  fun i : Fin 3 => match i with
  | 0 => ⟨a, a_span_pq⟩
  | 1 => ⟨b, b_span_pq⟩
  | 2 => ⟨p, p_span_pq⟩

theorem abp_card_le_span_rank
  (a b p q : V)
  (finite_submodule_instance := pq_subspace_finite (K := K) (V := V) p q)
  (pq_neq : p ≠ q)
  (abp_indep : LinearIndependent K ![a, b, p])
  (a_span_pq : a ∈ (span K {p, q}))
  (b_span_pq : b ∈ (span K {p, q})) :
    (card {a, b, p}) ≤ finrank K (span K {p, q}) := by
  have p_span_pq : p ∈ span K {p, q} := Submodule.subset_span (Set.mem_insert p {q})
  let s : Finset (span K {p, q}) := {⟨a, a_span_pq⟩, ⟨b, b_span_pq⟩, ⟨p, p_span_pq⟩}
  have card_eq : s.card = Finset.card {a, b, p} := by
    rw [← Finset.card_image_of_injective s Subtype.val_injective]
    aesop
  rw [← card_eq]
  apply finset_card_le_finrank (R := K) (M := (span K {p, q})) (b := s)
  have abp_indep_sub : LinearIndependent K (indexer a b p q a_span_pq b_span_pq p_span_pq) := by sorry
  exact abp_indep_sub
  -- type mismatch
  --   abp_indep_sub
  -- has type
  --   LinearIndependent K (indexer a b p q a_span_pq b_span_pq p_span_pq) : Prop
  -- but is expected to have type
  --   LinearIndependent K fun x => ↑x : Prop

I can't wrap my head around why LinearIndependent expects a function that takes a vector, shouldn't it expect an indexing function? For example, before, we passed ![a, b, p] which is of type Fin 3 → V.

[Richard Copley]

At this time it might be helpful for you to read the comments at the top of the source file LinearIndependent.lean. There it's explained how statements about linearly independent sets are formalized.