basis.sum_extend

Stream: maths

[Patrick Massot]

docs#basis.sum_extend creates really nasty types which appear in the context as:

basis (fin n ⊕ ↥(_.extend basis.sum_extend._proof_2 \ range v)) ℝ F

for instance. @Anne Baanen do you think there is anyway we could improve that?

[Anne Baanen]

The alternative I see is having the return type look like Σ (s : set V), basis (ι + s) K V (or putting this s in a separate definition). Do you have an example of sum_extend being applied, so I can see what we need to know about the return type?

[Eric Rodriguez]

Anne, I used it here when rewriting sphere-eversion; I assume this is where Patrick saw it

[Gabriel Ebner]

I guess it would already look better if linear_independent.extend didn't have the proof arguments, i.e. if it was linear_independent.extend (s t : V) (w/o a linear_independent argument) meaning a "minimal subset of t containing s and spanning t".

[Patrick Massot]

@Anne Baanen did anything came out of this discussion?

[Anne Baanen]

I agree with Gabriel's suggestion, that linear_independent.extend shouldn't take a proof argument. AFAIK, nobody has written code (yet) to implement that.

[Anne Baanen]

I have some time now to implement the suggestion, look forward to making a PR soon!

[Anne Baanen]

It was more difficult than I was hoping, but here's an ungolfed, messy commit: branch#linear_independent_extend

[Anne Baanen]

@Patrick Massot, would you be willing to help with PR'ing this?

[Jakob von Raumer]

Oh, that's the stuff I need :)

[Patrick Massot]

I'll try to have a look tonight

[Anne Baanen]

Thanks!

[Patrick Massot]

I had a look but I'm puzzled. Why this super convoluted exists_extend? Why not simply stating there are subsets s0 of s and t0 of t such that the union of s0 and t0 is linear independent and spans the same subspace as t?

[Anne Baanen]

Well, you need to apply Zorn's lemma in some way to get this result, so unless I missed an easy way to apply exists_linear_independent as-is, you essentially have to redo its proof in the more general setting.

[Anne Baanen]

Patrick Massot said:

there are subsets s0 of s and t0 of t such that the union of s0 and t0 is linear independent and spans the same subspace as t?

I don't think that's strong enough to prove linear_independent_extend, since we could just choose s0 empty and t0 outside of s, making linear_independent_extend false.