linear suffering

Stream: maths

[Patrick Massot]

@Anne Baanen and @Joseph Myers I spend two days trying to work with the linear algebra and affine geometry library but it's 100% suffering. Everything around linear independence, bases, affine independence... can be expressed in terms of indexed families, sets, finsets, subtypes and it's a nightmare when there is more than only set/family involved, especially when I want to extend of modify a family. I don't know if it means the API lacks millions of lemmas to go back and forth between various representations, or there is a secret way to consistently use the right one and switch only at the beginning and end of proofs.

For instance, I'd need something like:

import linear_algebra.affine_space

open finite_dimensional set

variables  (k : Type*)  [field k] (V : Type*) [add_comm_group V] [vector_space k V]
           {P : Type*} [affine_space k V P]

example {ι : Type*} [finite_dimensional k V] {n : ℕ} {p : ι → P} (hp : affine_independent k V p) :
  ∃ q : fin (findim k V + 1) → P, affine_independent k V q ∧ range p ⊆ range q :=
sorry

I tried to define intermediate stuff like

def affine_independent_set (s : set P) : Prop := affine_independent k V (λ p, p : {i // i ∈ s} → P)

example  {S : set P} (h : affine_independent_set k V S) :
  ∃ T : set P, S ⊆ T ∧ affine_independent_set k V T ∧ affine_span k V T = ⊤ :=
sorry

example {S : finset P} (hp : affine_independent_set k V (↑S : set P)) (h' : affine_span k V (↑S : set P) = ⊤) :
  S.card = findim k V :=
sorry

but everything seem so painful. Do you have any advice?

[Patrick Massot]

For instance, the things I tried to glue are docs#exists_subset_is_basis and docs#affine_independent_iff_linear_independent_vsub

[Joseph Myers]

I've found that generally manipulating subtypes, and manipulating sums when there are multiple subtypes and finsets involved, is painful. That's why affine_independent_iff_linear_independent_vsub has a long proof with essentially no mathematical content, it needs to convert between sums over (a finset of) ι and sums over (a finset of) a subtype of all but one value of ι.

My guess is that for your intermediate result using affine_independent_set, it would be helpful to prove a version of affine_independent_iff_linear_independent_vsub that relates affine_independent_set on a set of points to linear_independent for the identity map on a set of vectors (i.e. linear_independent in exactly the form used by exists_subset_is_basis). There's a bijection between the index type you'd get from affine_independent_iff_linear_independent_vsub when using a set (a subtype of points) and the one you'd need for exists_subset_is_basis (a subtype of vectors), given in one direction by vadd_const composed on either side with the manipulations needed to go between type and subtype, so it should be possible to use injectivity plus linear_independent.comp to go between linear independence of the same vectors with the two different index types. There will still be quite a lot of fiddling around with subtypes involved, but hopefully you don't actually need to get into explicit summation over the different types.

[Patrick Massot]

Thanks for your answer Joseph. Too bad it confirms what I feared. There must be a better way. Again we should probably have a look at what other libraries do.

[Joseph Myers]

I guess look at how other systems handle this sort of moving between types and subtypes, and between two types related by an injection or bijection, since that's where most of the pain seems to come from.

[Patrick Massot]

This is probably very different in Isabelle or Mizar, but people using Coq have almost certainly met those issues ten years ago.

[Yury G. Kudryashov]

We can use finsets, then we won't need subtypes.

[Patrick Massot]

finset don't even have a coercion to Sort, which makes them even more painful to convert to indexed families.

[Joseph Myers]

The main definitions of linear_independent and affine_independent use indexed families (for good reason, it's desirable to be able to talk about a family with multiple identical vectors not being linearly independent). Using a subtype in some way thus seems unavoidable when relating affine_independent to linear_independent, because the independent family of vectors is one smaller than the family of points. Unless you complicate the definitions so they aren't "this family is independent" but "the subset of this family given by this subset of the index type is independent", I suppose.

[Joseph Myers]

What would be good to avoid is all the tedious fiddling around with trivialities that results from involving subtypes.

[Joseph Myers]

I remember someone explaining to me some years ago an argument that it's wrong (in maths, not just in formalization) to say that a basis is a "set" of vectors with certain properties, because sets go wrong there as soon as you do any manipulations that might involve two vectors being or becoming equal. (I think he was arguing for "multiset" as the right thing to use, but in Lean it seems to be "indexed family".)

[Floris van Doorn]

My first guess would be to make the primitive notion "this family of sets is linear/affine independent on this subset of \i":

variables (k : Type*) (V : Type*) {P : Type*} [ring k] [add_comm_group V] [module k V]
variables [affine_space k V P] {ι : Type*}
def my_affine_independent (p : ι → P) (s : set ι) : Prop :=
∀ (t : finset ι) (h : ↑t ⊆ s) (w : ι → k), ∑ i in t, w i = 0 → t.weighted_vsub V p w = 0 →
  ∀ i ∈ t, w i = 0

(you could argue whether the domain of p should be \i or s. I think \i is more convenient to work with)
The fact that you add a set as an argument means you don't have to talk about subtypes, but can talk about subsets, intersections of sets and so on.
This also makes it more convenient to formulate Patrick extension problem:

variables  (k : Type*) [field k] (V : Type*) [add_comm_group V] [vector_space k V]
           {P : Type*} [affine_space k V P]
example {ι : Type*} [finite_dimensional k V] {n : ℕ} {p : ι → P} {s : set ι}
  (hp : my_affine_independent k V p s) (h : ↑(findim k V) < cardinal.mk ι) :
  ∃ t : set ι, s ⊆ t ∧ cardinal.mk t = findim k V + 1 ∧ my_affine_independent k V p t :=
sorry

(though maybe the use of cardinal.mk for finite things is not ideal)

[Patrick Massot]

Maybe Floris is right, and we could have a notation to handle the case s = univ.

[Patrick Massot]

In the mean I think I have found a way to bypass the issue. But this is the first time I really feel like dependent types don't allow me to easily express a statement.

[Anne Baanen]

It makes sense that we try dividing responsibilities between re-indexing a family and taking a subset. Perhaps the ∀ (t : finset ι) (w : ι -> k) should be bundled into a finsupp?

[Joseph Myers]

Using a finsupp would probably run into the usual issues with there being a much better API for manipulating sums over finsets than those over finsupps. But there are lemmas relating linear_independent to both finset and finsupp, so if finsupp helps here you can always use a different lemma to get it.

As it turns out, a proof of the version of affine_independent_iff_linear_independent_vsub for sets (which should be usable with exists_subset_is_basis) is short, but painful to write because it involves dealing with a subtype of a subtype.

import linear_algebra.affine_space.independent

section add_torsor

open add_torsor

variables (G : Type*) {P : Type*} [add_group G] [add_torsor G P]

lemma vsub_left_injective (p : P) : function.injective (λ p1 : P, (p1 -ᵥ p : G)) :=
λ p2 p3 h, vsub_left_cancel G h

end add_torsor

open add_action add_torsor affine_space

variables (k : Type*) (V : Type*) {P : Type*} [ring k] [add_comm_group V] [module k V]
variables [affine_space k V P]

/-- A set is affinely independent if and only if the differences from
a base point in that set are linearly independent. -/
lemma affine_independent_set_iff_linear_independent_vsub (s : set P) {p1 : P} (hp1 : p1 ∈ s) :
  affine_independent k V (λ p, p : s → P) ↔
    linear_independent k (λ v, v : (λ p, (p -ᵥ p1 : V)) '' (s \ {p1}) → V) :=
begin
  rw affine_independent_iff_linear_independent_vsub k V (λ p, p : s → P) ⟨p1, hp1⟩,
  split,
  { intro h,
    have hv : ∀ v : (λ p, (p -ᵥ p1 : V)) '' (s \ {p1}), (v : V) +ᵥ p1 ∈ s \ {p1} :=
      λ v, (set.mem_image_of_injective (vsub_left_injective V p1)).1
             ((vadd_vsub V (v : V) p1).symm ▸ v.property),
    let f : (λ p : P, (p -ᵥ p1 : V)) '' (s \ {p1}) → {x : s // x ≠ ⟨p1, hp1⟩} :=
      λ x, ⟨⟨(x : V) +ᵥ p1, set.mem_of_mem_diff (hv x)⟩,
            λ hx, set.not_mem_of_mem_diff (hv x) (subtype.ext_iff.1 hx)⟩,
    convert h.comp f
      (λ x1 x2 hx, (subtype.ext (vadd_right_cancel p1 (subtype.ext_iff.1 (subtype.ext_iff.1 hx))))),
    ext v,
    exact (vadd_vsub V (v : V) p1).symm },
  { intro h,
    let f : {x : s // x ≠ ⟨p1, hp1⟩} → (λ p : P, (p -ᵥ p1 : V)) '' (s \ {p1}) :=
      λ x, ⟨((x : s) : P) -ᵥ p1, ⟨x, ⟨⟨(x : s).property, λ hx, x.property (subtype.ext hx)⟩, rfl⟩⟩⟩,
    convert h.comp f
      (λ x1 x2 hx, subtype.ext (subtype.ext (vsub_left_cancel V (subtype.ext_iff.1 hx)))) }
end

[Joseph Myers]

I've now got the result extending an affine independent set to one that is also spanning. I'll PR once #3727 is in, to avoid introducing more complications to the merges for that PR. Part of the difficulty here is certainly the difficulty of manipulating subtypes, but part is also that the API for affine spaces is still being built out and more lemmas like this still need adding to mathlib. (I don't plan to try to prove the results about finite dimension and cardinality for now.)

/-- An affinely independent set of vectors can be extended to such a
set that spans the whole space. -/
lemma exists_subset_affine_independent_affine_span_eq_top {s : set P}
    (h : affine_independent k V (λ p, p : s → P)) :
  ∃ t : set P, s ⊆ t ∧ affine_independent k V (λ p, p : t → P) ∧ affine_span k V t = ⊤ :=
-- proof omitted here

[Patrick Massot]

Nice! I'm also experimenting (in a slightly different direction), but everything is difficult because cardinal universes come in, as well as the usual inconvenience of finite types.

[Joseph Myers]

#3794 has the proof that an affine independent set of points can be extended to one that is spanning.

[Patrick Massot]

Great. What is the status of convexity? Is there anything I can do to help?

[Joseph Myers]

I guess maybe merging master into convex-affine and fixing things up until it builds? (#2910 has a summary of some things that should be done.)

[Patrick Massot]

Ok, I'll try to work on this tomorrow.

[Jacques Carette]

Is there a way to bookmark threads on Zulip? I ask because the discussion here has information that I want to come back to: roughly speaking that some ways of doing math "on paper" when you can hand-wave away all the details doesn't make for a pleasant experience when formalized. Things like "finite types", which are an obvious translation of what is done by hand, seem to end up causing more pain than not.

I should go through the Lean docs and see what 'conventional-formalization-in-Lean' wisdom you've already accumulated + documented.

[Kevin Buzzard]

you can star messages

[Johan Commelin]

You can also hit S to focus on this stream, and then bookmark it in your browser.

[Jacques Carette]

I'm using the Zulip desktop app to view this. S didn't seem to do anything?

[Johan Commelin]

Aah, I guess that the second part of my sentence doesn't make sense either, in that case.

[Patrick Massot]

Joseph Myers said:

I guess maybe merging master into convex-affine and fixing things up until it builds? (#2910 has a summary of some things that should be done.)

I should report on this: I think too many things have changed so to allow merging, but I'll look at it for inspiration. I'm waiting for #3728 to land anyway.

[Shing Tak Lam]

Jacques Carette said:

I'm using the Zulip desktop app to view this. S didn't seem to do anything?

It's Ctrl-S for me.

[Kevin Buzzard]

the keyboard shortcuts in the Zulip app can be accessed with by clicking the cog in the top right and then selecting keyboard shortcuts. Perhaps the shortcuts are OS-dependent?

[Kevin Buzzard]

On linux narrow-to-stream is S and star message is Ctrl-S

[Shing Tak Lam]

wait. I misunderstood Jacques' message. It's the same for me :face_palm:

[Shing Tak Lam]

@Jacques Carette If you're viewing "All messages" then pressing S will focus to the stream that the message highlighted is in.

[Jacques Carette]

Ah, I see. I'm actually navigating to each of the streams one-by-one. It lets me more easily catch up (and also mark-read the ones I am not interested in).

[Reid Barton]

You can do that navigation automatically with n