linear_independent for families

Stream: maths

[Alexander Bentkamp]

For my work on eigenvectors, I need a definition of linear independence for families of vectors, not only sets, because I need to be able to talk about a family being linearly dependent if it contains the same vector twice. I've started working on this here:

https://github.com/leanprover-community/mathlib/commit/7a590e5a29469975798a6432e577826a81ea0b94

The crucial change I did is to replace the definition

@[reducible] def lc (α β) [ring α] [add_comm_group β] [module α β] : Type* := β →₀ α

by

@[reducible] def lc (ι : Type*) (α : Type*) (β : Type*) [has_zero α] (v : ι → β) := ι →₀ α

I'd like to get some feedback from you before I continue because this change breaks quite a lot of things that I need to repair.

[Kevin Buzzard]

Are you in the finite-dimensional setting? I have seen that in the finite-dimensional case one often has to deal with lists of vectors, whereas in the infinite-dimensional case it's often sets; the problems one works on are somehow different in the two cases.

[Johan Commelin]

@Alexander Bentkamp I'm not sure if it is worth it to replace lc with that definition. In particular, lc currently has some semantics that you won't be able to recover with your definition.

[Alexander Bentkamp]

Yes, I work in the finite-dimensional setting, but if we had a definition that uses families, both lists and sets would be special cases.

[Johan Commelin]

Maybe you should just make a new definition

[Johan Commelin]

lc is the type of all formal linear combinations. And you don't get that with the family version.

[Alexander Bentkamp]

The old definition is a special case of my new one by choosing the set of vectors itself as the index set and the identity as the map. Where it matters, we could restrict ourselves to that case.

[Johan Commelin]

That's true

[Johan Commelin]

If you pull this off, chapeau! But I agree that it is quite non-trivial. You might want to coordinate with @Mario Carneiro and @Chris Hughes. This will be quite an effort, and you'll want the merge into mathlib to be as smooth as possible.

[Kevin Buzzard]

Why not just make a new function lc' or whatever?

[Kevin Buzzard]

lc currently has some semantics that you won't be able to recover with your definition.

What does the word "semantics" mean?

[Johan Commelin]

Oooh, I don't actually know precisely. I meant "intended meaning".

[Johan Commelin]

And I retract the claim.

[Alexander Bentkamp]

Why not just make a new function lc' or whatever?

I don't want to duplicate the proofs that we have about lc.

[Johan Commelin]

I guess that several proofs will actually simplify

[Johan Commelin]

Other things will become a bit more verbose

[Neil Strickland]

I am strongly in favour of this. All sorts of things are awkward and unnatural if you define linear independence in terms of subsets, because of the fact that vectors can accidentally be equal for spurious reasons.

[Kevin Buzzard]

I must confess I was surprised when I first saw this. The justification I heard at the time was that to prove every vector space has a basis you want to use Zorn's lemma and then it's convenient to use subsets.

[Alexander Bentkamp]

That was easier than I thought: https://github.com/leanprover-community/mathlib/pull/943

[Chris Hughes]

Do we want the beta and iota - > beta arguments for lc, given that they're not used?

[Alexander Bentkamp]

Good point. I will try to remove them and see what happens.

[Mario Carneiro]

I agree that linear independence should be in terms of families rather than sets, and lc itself seems a bit overly specific, but the definition of lc in Alex's first post doesn't make any sense (EDIT: I see chris also noted this)

[Mario Carneiro]

It would be nice if there is an obvious generalization of lc that makes sense for families such that the submodule based definition of linear_independent stays the same

[Mario Carneiro]

In PR #943 the definition of linear_independent is still over a set, rather than a family?

[Alexander Bentkamp]

It's over a set of indices of the family

[Alexander Bentkamp]

So it can contain duplicate vectors

[Mario Carneiro]

I think it can just be the entire family, the set isn't needed

[Mario Carneiro]

we can compose with subtype.val to recover sets when needed

[Mario Carneiro]

Okay, so I'm catching up here, but I think what we want is for lc to denote iota ->0 alpha, that is, finitely supported coefficients, and lc.total now takes a separate argument iota -> beta for the family

[Mario Carneiro]

That's basically the same as what you have except that lc doesn't take the family as input

[Alexander Bentkamp]

Yes, I am already working on removing the arguments beta and v where they are not needed.

[Mario Carneiro]

so lc.supported isn't needed anymore in the definition of linear_independent, it can just be (lc.total alpha v).ker = bot where v : iota -> beta

[Mario Carneiro]

in place of lc.supported we have some rules about how lc.total interacts with composition of the valuation functions

[Alexander Bentkamp]

Ok, I'll try that.

[Alexander Bentkamp]

The first part (removing the unnecessary arguments) is done - see pull request.

[Alexander Bentkamp]

The second part (changing the definiton of linearly_independent to (lc.total alpha v).ker = bot) will be a lot of work. Are you sure it is the right thing to do? Having the additional set-argument may be more practical than forcing the user to use subtypes.

[Mario Carneiro]

I agree it's not trivial, but in hindsight I think that was a bad move on the library design side

[Mario Carneiro]

I actually think that in almost all cases we care about linearly independent families, not sets. The only counterexample is the zorn's lemma proof of existence of a basis, but that has more to do with the particulars of that proof and shouldn't affect the rest of the development

[Alexander Bentkamp]

How can lemmas like
- A subset of a lin. indep. set is lin. indep.
- If two sets are lin. indep. and their spans are disjoint, their union is lin. indep.
best be formulated then?

[Mario Carneiro]

subset is lin indep becomes f linind -> g injective -> g o f linind

[Mario Carneiro]

union linind becomes something about sum.elim f g (that function might not exist now that I come to think of it, it's nondependent sum.rec). If f : I -> A and g : J -> A are linind and span (range f) \cap span (range g) = bot then sum.elim f g : I + J -> A is linind

[Mario Carneiro]

I'm not totally happy with span (range f) but it does the job and I don't think there is another notation for it

[Alexander Bentkamp]

I am more worried about the I + J. This looks like dependent type hell :-)

[Mario Carneiro]

no dependent types

[Mario Carneiro]

that's just a plain old sum

[Mario Carneiro]

The theorems about postcomposition with injective functions will allow you to use equivs if that representation doesn't make you happy

[Mario Carneiro]

I don't think the original theorem ever applies when the union is not disjoint, so it should be fine

[Alexander Bentkamp]

Ok, that's right.

[Mario Carneiro]

except maybe in weird trivial cases like the zero ring

[Alexander Bentkamp]

I am worried about a user who actually would like to use sets, but is forced to use the subtypes corresponding to those sets. Then ↑s + ↑t would be a different type than ↑ (s ⋃ t), which can be annoying.

[Mario Carneiro]

This can be proven as a lemma

[Mario Carneiro]

the equiv is already there, you just have to apply it here

[Alexander Bentkamp]

Ok, sounds good

[Johan Commelin]

So now lc is just a type wrapper around finsupp. Is there any reason to not just use finsupp?

[Mario Carneiro]

no

[Mario Carneiro]

once upon a time it was a bad module because of the multiple base rings problem

[Johan Commelin]

Ok, then I suggest just using finsupp, because it means even less duplication.

[Johan Commelin]

@Alexander Bentkamp What is your opinion? In order to avoid duplicate work, do you think we should wait for a while with #943?

[Rob Lewis]

If @Johannes Hölzl has time to chime in here, I'd love to hear his opinion. He worked quite a bit with this part of the library for the cap set proof. But he's a few weeks into the new job and in California right now. Maybe he's too distracted by wealth and fame and shiny white electronics.

[Alexander Bentkamp]

@Alexander Bentkamp What is your opinion? In order to avoid duplicate work, do you think we should wait for a while with #943?

I'd be happy if you'd merge it. It may not be perfect, but it's a step in the right direction.

[Chris Hughes]

I'm not in favour of changing a definition with the intention of changing it straight away afterwards, just in case somebody ends up having to update their project twice, who didn't know they should wait until the second change.

[Johan Commelin]

@Alexander Bentkamp Thanks for the work on merging lc and finsupp. Well done!

[Alexander Bentkamp]

@Mario Carneiro As we discussed today in person, I will try to change the definiton of linearly_independent to (lc.total alpha v).ker = bot, i.e. remove the s : set argument. Do you think I should also redefine is_basis to use families instead of sets? It doesn't seem to make much sense there...

[Mario Carneiro]

Certainly. In fact I think the argument to use families instead of sets for a basis is even stronger than for linearly independent sets. A basis is necessarily injective so it might seem redundant, but we definitely want to think of basis elements as indexed by a family. In particular this seamlessly represents the concept of "ordered basis", since rather than asking for an ordering on some subset of the type (messy) we have an indexed family where the index type has a built in ordering (simple and provided by TC inference)

[Johan Commelin]

@Alexander Bentkamp I think this is a very good move. I'm looking forward to your PR.

[Kevin Buzzard]

Certainly. In fact I think the argument to use families instead of sets for a basis is even stronger than for linearly independent sets. A basis is necessarily injective so it might seem redundant, but we definitely want to think of basis elements as indexed by a family. In particular this seamlessly represents the concept of "ordered basis", since rather than asking for an ordering on some subset of the type (messy) we have an indexed family where the index type has a built in ordering (simple and provided by TC inference)

For a free module over the zero ring, a basis might not be injective! R is isomorphic to R^2 as an R-module.

[Johan Commelin]

If you squint a bit you can easily see that punit is defeq to p0wnd

[Johan Commelin]

The zero ring is the one ring...

[Alexander Bentkamp]

The empty set should then be replaced by a family with an empty type as index set. How do I best describe an empty type? Not every empty type is equal to empty, right? So maybe ∀ x : ⍺, false? Or ¬ nonempty ⍺?

[Mario Carneiro]

For the theorem I would use not nonempty as an assumption, so it is maximally applicable

[Alexander Bentkamp]

I am trying to define def finsupp.sum_elim_left {α β γ : Type*} [has_zero γ] (l : α ⊕ β →₀ γ) : α →₀ γ, which should simply ignore the values on β. Anything that I can come up with seems far too complicated. Any suggestions?

[Kevin Buzzard]

I would just precompose with the injection alpha -> alpha + beta I guess.

[Mario Carneiro]

map_domain inl?

[Mario Carneiro]

I guess you need to know some finiteness property of the function in order for preimages to work like that

[Kevin Buzzard]

If you use map_domain, don't you need a map from alpha+beta to alpha? This might be problematic if alpha is empty and beta is not. Or have I got things the wrong way around?

[Kevin Buzzard]

/-- Given `f : α₁ ↪ α₂` and `v : α₁ →₀ β`, `emb_domain f v : α₂ →₀ β` is the finitely supported
function whose value at `f a : α₂` is `v a`. For a `a : α₁` outside the domain of `f` it is zero. -/
def emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) : α₂ →₀ β :=

I think that's what you're after

[Kevin Buzzard]

no that's still the wrong way round

[Kevin Buzzard]

The closest I can find is

/-- `subtype_domain p f` is the restriction of the finitely supported function
  `f` to the subtype `p`. -/
def subtype_domain (p : α → Prop) [decidable_pred p] (f : α →₀ β) : (subtype p →₀ β) :=

But this is not ideal -- it should be Stricklandized into a definition which works for an arbitrary injection gamma -> alpha, not just a subtype.

[Kevin Buzzard]

What I am surprised by here is that finsupp has been used extensively in a lot of APIs so I am pretty sure I must have missed it -- someone would surely have spotted this by now.

[Alexander Bentkamp]

Yes, map_domain and emb_domain are in the wrong direction. And I don't see how I could modify subtype_domain to work with an injection...

[Alexander Bentkamp]

I found this solution, which is quite ok I think:

def finsupp.sum_elim_left {α β γ : Type*} [has_zero γ] (l : α ⊕ β →₀ γ) : α →₀ γ :=
{ support := (set.finite_preimage (@sum.inl.inj _ _) l.support.finite_to_set).to_finset,
  to_fun := (λ a, l (sum.inl a)),
  mem_support_to_fun :=
    begin
      intros a,
      simp [set.finite.to_finset]
    end }

*Edit: I removed a few spurious type assumptions

[Mario Carneiro]

I think emb_domain should work the other way around, using essentially the proof you gave with a variable in place of sum.inl.inj

[Mario Carneiro]

Actually I'm surprised emb_domain exists at all, since it's a special case of map_domain. Maybe it's for the defeqs?

[Alexander Bentkamp]

map_domain works only if beta is a add_comm_monoid.

[Mario Carneiro]

I guess the most general precondition for which precomp is well defined is that the fibers of the function are fintypes

[Alexander Bentkamp]

I'll see what I can do.

[Johan Commelin]

I guess the most general precondition for which precomp is well defined is that the fibers of the function are fintypes

Aka "finite maps"?

[Alexander Bentkamp]

I didn't know that they were called that either, but I think that's what Mario meant.

[Alexander Bentkamp]

I will stick to injective maps for now though, because that is what the theorems in finite.lean are about. If I try to make everything as general as possible I will never get it done :)

[Alexander Bentkamp]

Is α ⊕ β a sigma type? For example, in big_operators.lean there are no lemmas about α ⊕ β, but there are some about sigma. Can I use those?

[Alexander Bentkamp]

OK, I managed to establish a connection between ⊕ and sigma with Simon's help.