proving that sum_coords are equal

Stream: general

[Mantas Baksys]

Hey everyone! I have encountered the following problem, which I seem to not be able to solve on my own. Given two affine bases, whose points are a permutation of each other, I want to show that the sum_coords of any point in the space are equal under the basis, where the same vector is taken out from the two basis_of constructed from the affine bases. Here's an MWE :

import geometry.euclidean
import linear_algebra.affine_space.basis
import tactic.basic

variables {V : Type*} [inner_product_space ℝ V]
include V

open equiv

lemma sum_coords_eq {ι : Type*} (S T : affine_basis ι ℝ V) (σ : perm ι) (h : S.points = T.points ∘ σ) (i : ι) :
  (S.basis_of i).sum_coords = (T.basis_of (σ i)).sum_coords := sorry

I'm struggling to find the right generality for this as I'm not sure what kind of equivalence relation for the bases I'd need (or even if that's the right way to proceed).

[Yaël Dillies]

Note that we've thought about it a bit together and one should be able to state that with basis directly. Something like (b : basis ι ℝ V) (c : basis ι' ℝ V) (e : ι ≃ ι') (hbc : something) : b.sum_coords = c.sum_coords.

[Joseph Myers]

basis.reindex is probably the way to go for two bases related by an equiv of their index types (and then you might need to define affine_basis.reindex and set up API for that as well).

[Oliver Nash]

I was on holiday (sans laptop) last week so I might be too late to help. Here goes anyway.

[Oliver Nash]

Joseph is of course completely correct. It looks like what you really want is an affine_basis.reindex definition + API. It would be great if you developed that.

[Oliver Nash]

In the meantime, here's the sort of thing you can do with what we currently have:

import linear_algebra.affine_space.basis

open_locale affine

variables {ι ι' R V P : Type*} [ring R] [add_comm_group V] [module R V] [affine_space V P]
variables [fintype ι] [fintype ι'] -- Redundant but convenient because of missing API
variables (b : affine_basis ι R P) (b' : affine_basis ι' R P)

lemma foo (e : ι ≃ ι') (h :  b'.points ∘ e = b.points) (i : ι) :
  b.coord i = b'.coord (e i) :=
begin
  ext p,
  conv_rhs { rw ← b.affine_combination_coord_eq_self p, },
  classical,
  simp [finset.univ.map_affine_combination _ _ (b.sum_coord_apply_eq_one p), ← h, b'.coord_apply],
end

-- Needs PR #10637
lemma bar (e : ι ≃ ι') (h :  b'.points ∘ e = b.points) (i : ι) :
  (b.basis_of i).sum_coords = (b'.basis_of (e i)).sum_coords :=
by rw [← neg_inj, ← b.linear_eq_sum_coords, ← b'.linear_eq_sum_coords, foo b b' e h i]

[Oliver Nash]

I should also add that I'm surprised you needed results about basis_of and sum_coords. I suspect this is because what you really wanted were results about affine bases and you were trying to prove them by unfolding the definition, which will then require you to use results about basis_of and sum_coords.

[Yaël Dillies]

For reference, this is about Ceva's theorem, which really is about coordinates.

[Oliver Nash]

However you should never _need_ to use (and probably never actually use) the definitions because we have enough of an API to characterise barycentric coordinates, as seen above.

[Oliver Nash]

Yaël Dillies said:

For reference, this is about Ceva's theorem, which really is about coordinates.

Oh cool. The original imports suggested it was one of these sorts of results. It would be nice to see Ceva proved. I'm still not sure this is best expressed in terms of sum_coords but I'm happy to wait and see.