[Merged by Bors] - feat(linear_algebra/affine_space/independent): affine.simplex.reindex
#17566
Conversation
Add a definition for remapping a simplex along an `equiv` of index types, and associated basic API. (Typically of course the two index types are defeq and this is a permutation of indices within the same type, but the definition covers the general case where they might not be defeq.)
jsm28
added
awaiting-review
leanprover-community-bot-assistant
added
ready-to-merge
| @[simps] | ||
| def reindex {m n : ℕ} (s : simplex k P m) (e : fin (m + 1) ≃ fin (n + 1)) : simplex k P n := | ||
| ⟨s.points ∘ e.symm, (affine_independent_equiv e.symm).2 s.independent⟩ |
There was a problem hiding this comment.
This works more generally for an embedding or a embedding_class, right?
There was a problem hiding this comment.
Well, we have face to extract a simplex with a given subset of points, but yes, it would be possible to define a variant using an embedding and derive various things from that. It would be good to have proper documentation on the leanprover-community website of conventions for reindexing and similar operations (and ensure existing APIs follow them). For example, when should the operation be reindex (basis) versus comp_equiv (affine_basis) versus dom_dom_congr (multilinear_map)? Which way round should an equiv of index types be specified, when an equiv is used?
| /-- Reindexing by the composition of two equivalences is the same as reindexing twice. -/ | ||
| @[simp] lemma reindex_trans {n₁ n₂ n₃ : ℕ} (e₁₂ : fin (n₁ + 1) ≃ fin (n₂ + 1)) | ||
| (e₂₃ : fin (n₂ + 1) ≃ fin (n₃ + 1)) (s : simplex k P n₁) : | ||
| s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃ := | ||
| rfl |
There was a problem hiding this comment.
This might be more convenient as a simp lemma in the reverse direction; do you have a reason for preferring this direction?
There was a problem hiding this comment.
This is another case where I don't think we have any defined convention for whether to prefer trans (and other similar composition operations) or whether to prefer a form where each operation is applied in succession, and again might benefit from documentation saying what the simp normal form should generally be for lemmas involving applying the results of trans, comp or similar.
…x` (#17566) Add a definition for remapping a simplex along an `equiv` of index types, and associated basic API. (Typically of course the two index types are defeq and this is a permutation of indices within the same type, but the definition covers the general case where they might not be defeq.)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
affine.simplex.reindexaffine.simplex.reindex
Add lemmas that reindexing a simplex along an `equiv` of index types does not change the `circumsphere`, `circumcenter` or `circumradius`. --- Regarding the comments in #17566 about reindexing along an embedding rather than just an `equiv`, the lemmas here do need an `equiv` to get all three equalities (which is thus why I was thinking of `equiv` when writing that PR). With an embedding you only get a weaker statement about orthogonal projections (see the existing `orthogonal_projection_circumcenter`).
Add a definition for remapping a simplex along an
equivof index types, and associated basic API. (Typically of course the two index types are defeq and this is a permutation of indices within the same type, but the definition covers the general case where they might not be defeq.)