Zulip Chat Archive

Stream: maths

Topic: linear_independent for families


view this post on Zulip Alexander Bentkamp (Apr 16 2019 at 20:08):

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.

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 20:13):

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.

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:15):

@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.

view this post on Zulip Alexander Bentkamp (Apr 16 2019 at 20:15):

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.

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:15):

Maybe you should just make a new definition

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:16):

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

view this post on Zulip Alexander Bentkamp (Apr 16 2019 at 20:18):

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.

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:19):

That's true

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:20):

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.

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 20:20):

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

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 20:21):

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

What does the word "semantics" mean?

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:22):

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

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:22):

And I retract the claim.

view this post on Zulip Alexander Bentkamp (Apr 16 2019 at 20:22):

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

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

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:23):

I guess that several proofs will actually simplify

view this post on Zulip Johan Commelin (Apr 16 2019 at 20:23):

Other things will become a bit more verbose

view this post on Zulip Neil Strickland (Apr 16 2019 at 20:24):

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.

view this post on Zulip Kevin Buzzard (Apr 16 2019 at 20:43):

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.

view this post on Zulip Alexander Bentkamp (Apr 16 2019 at 22:22):

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

view this post on Zulip Chris Hughes (Apr 17 2019 at 00:27):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 00:34):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:40):

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)

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:41):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:43):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 00:44):

It's over a set of indices of the family

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 00:44):

So it can contain duplicate vectors

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:44):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:45):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:48):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:48):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 00:49):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:50):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 00:51):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 00:56):

Ok, I'll try that.

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 01:39):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 01:44):

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.

view this post on Zulip Mario Carneiro (Apr 17 2019 at 01:56):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 01:57):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 03:04):

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?

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:10):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:15):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:15):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 03:16):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:16):

no dependent types

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:17):

that's just a plain old sum

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:17):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:19):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 03:19):

Ok, that's right.

view this post on Zulip Mario Carneiro (Apr 17 2019 at 03:19):

except maybe in weird trivial cases like the zero ring

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 03:23):

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.

view this post on Zulip Mario Carneiro (Apr 17 2019 at 04:22):

This can be proven as a lemma

view this post on Zulip Mario Carneiro (Apr 17 2019 at 04:23):

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

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 04:33):

Ok, sounds good

view this post on Zulip Johan Commelin (Apr 17 2019 at 06:43):

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

view this post on Zulip Mario Carneiro (Apr 17 2019 at 07:18):

no

view this post on Zulip Mario Carneiro (Apr 17 2019 at 07:18):

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

view this post on Zulip Johan Commelin (Apr 17 2019 at 07:19):

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

view this post on Zulip Johan Commelin (Apr 17 2019 at 07:22):

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

view this post on Zulip Rob Lewis (Apr 17 2019 at 08:05):

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.

view this post on Zulip Alexander Bentkamp (Apr 17 2019 at 12:51):

@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.

view this post on Zulip Chris Hughes (Apr 18 2019 at 12:40):

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.

view this post on Zulip Johan Commelin (Apr 19 2019 at 05:27):

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

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 01:24):

@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...

view this post on Zulip Mario Carneiro (Apr 23 2019 at 03:57):

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)

view this post on Zulip Johan Commelin (Apr 23 2019 at 06:08):

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

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 06:17):

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.

view this post on Zulip Johan Commelin (Apr 23 2019 at 06:22):

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

view this post on Zulip Johan Commelin (Apr 23 2019 at 06:24):

The zero ring is the one ring...

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 15:17):

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 ⍺?

view this post on Zulip Mario Carneiro (Apr 23 2019 at 15:43):

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

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 20:11):

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?

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 20:13):

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

view this post on Zulip Mario Carneiro (Apr 23 2019 at 20:13):

map_domain inl?

view this post on Zulip Mario Carneiro (Apr 23 2019 at 20:14):

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

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 20:17):

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?

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 20:21):

/-- 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

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 20:21):

no that's still the wrong way round

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 20:33):

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.

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 20:34):

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.

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 20:53):

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...

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 22:16):

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

view this post on Zulip Mario Carneiro (Apr 23 2019 at 22:20):

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

view this post on Zulip Mario Carneiro (Apr 23 2019 at 22:21):

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

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 22:23):

map_domain works only if beta is a add_comm_monoid.

view this post on Zulip Mario Carneiro (Apr 23 2019 at 22:28):

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

view this post on Zulip Alexander Bentkamp (Apr 23 2019 at 22:29):

I'll see what I can do.

view this post on Zulip Johan Commelin (Apr 24 2019 at 04:15):

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

Aka "finite maps"?

view this post on Zulip Alexander Bentkamp (Apr 24 2019 at 15:24):

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

view this post on Zulip Alexander Bentkamp (Apr 24 2019 at 15:25):

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 :)

view this post on Zulip Alexander Bentkamp (Apr 24 2019 at 17:00):

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?

view this post on Zulip Alexander Bentkamp (Apr 24 2019 at 19:14):

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


Last updated: May 11 2021 at 00:31 UTC