Stream: maths

Topic: linear_independent for families

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.

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.

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.

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.

Johan Commelin (Apr 16 2019 at 20:15):

Maybe you should just make a new definition

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.

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.

That's true

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.

Kevin Buzzard (Apr 16 2019 at 20:20):

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

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?

Johan Commelin (Apr 16 2019 at 20:22):

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

Johan Commelin (Apr 16 2019 at 20:22):

And I retract the claim.

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.

Johan Commelin (Apr 16 2019 at 20:23):

I guess that several proofs will actually simplify

Johan Commelin (Apr 16 2019 at 20:23):

Other things will become a bit more verbose

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.

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.

Alexander Bentkamp (Apr 16 2019 at 22:22):

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

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?

Alexander Bentkamp (Apr 17 2019 at 00:34):

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

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)

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

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?

Alexander Bentkamp (Apr 17 2019 at 00:44):

It's over a set of indices of the family

Alexander Bentkamp (Apr 17 2019 at 00:44):

So it can contain duplicate vectors

Mario Carneiro (Apr 17 2019 at 00:44):

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

Mario Carneiro (Apr 17 2019 at 00:45):

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

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

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

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.

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

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

Alexander Bentkamp (Apr 17 2019 at 00:56):

Ok, I'll try that.

Alexander Bentkamp (Apr 17 2019 at 01:39):

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

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.

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

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

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?

Mario Carneiro (Apr 17 2019 at 03:10):

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

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

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

Alexander Bentkamp (Apr 17 2019 at 03:16):

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

Mario Carneiro (Apr 17 2019 at 03:16):

no dependent types

Mario Carneiro (Apr 17 2019 at 03:17):

that's just a plain old sum

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

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

Alexander Bentkamp (Apr 17 2019 at 03:19):

Ok, that's right.

Mario Carneiro (Apr 17 2019 at 03:19):

except maybe in weird trivial cases like the zero ring

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.

Mario Carneiro (Apr 17 2019 at 04:22):

This can be proven as a lemma

Mario Carneiro (Apr 17 2019 at 04:23):

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

Ok, sounds good

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?

no

Mario Carneiro (Apr 17 2019 at 07:18):

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

Johan Commelin (Apr 17 2019 at 07:19):

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

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?

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.

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.

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.

Johan Commelin (Apr 19 2019 at 05:27):

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

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

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)

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.

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.

Johan Commelin (Apr 23 2019 at 06:22):

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

Johan Commelin (Apr 23 2019 at 06:24):

The zero ring is the one ring...

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

Mario Carneiro (Apr 23 2019 at 15:43):

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

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?

Kevin Buzzard (Apr 23 2019 at 20:13):

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

Mario Carneiro (Apr 23 2019 at 20:13):

map_domain inl?

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

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?

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

Kevin Buzzard (Apr 23 2019 at 20:21):

no that's still the wrong way round

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.

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.

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

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

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

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?

Alexander Bentkamp (Apr 23 2019 at 22:23):

map_domain works only if beta is a add_comm_monoid.

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

Alexander Bentkamp (Apr 23 2019 at 22:29):

I'll see what I can do.

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

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.

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

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?

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