Affine equivalences between affine bases

Two affine bases indexed by the same type are related by an affine equivalence: there is an affine equivalence sending the points of one basis to the corresponding points of the other (AffineBasis.exists_affineEquiv_apply_eq), and every affine map that does so preserves barycentric coordinates (AffineBasis.coord_apply_of_forall_apply_eq). This is how a statement about barycentric coordinates relative to an arbitrary affine basis is reduced to one about a fixed reference basis.

The file also computes the barycentric coordinates of a point after a homothety about the centroid of an affine basis (AffineBasis.coord_homothety_centroid), which describes the homothetic images of the simplex spanned by the basis, and those of a point of the segment between two points of the basis (AffineBasis.coord_lineMap).

Main statements

• AffineBasis.coord_apply_of_forall_apply_eq: an affine map sending the affine basis b to the affine basis b₂ carries barycentric coordinates relative to b to those relative to b₂;
• AffineBasis.exists_affineEquiv_apply_eq: there is an affine equivalence sending b to b₂;
• AffineBasis.coord_homothety_centroid: the barycentric coordinates of the image of a point under a homothety about the centroid of an affine basis;
• AffineBasis.coord_lineMap: the barycentric coordinates of a point of the segment between two points of an affine basis.

theorem AffineBasis.coord_apply_of_forall_apply_eq {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (b : AffineBasis ι k P) (b₂ : AffineBasis ι k P₂) {f : P →ᵃ[k] P₂} (hf : ∀ (i : ι), f (b i) = b₂ i) (i : ι) (x : P) : (b₂.coord i) (f x) = (b.coord i) x

An affine map sending each point b i of an affine basis to the point b₂ i of another affine basis preserves barycentric coordinates.

theorem AffineBasis.exists_affineEquiv_apply_eq {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (b : AffineBasis ι k P) (b₂ : AffineBasis ι k P₂) : ∃ (T : P ≃ᵃ[k] P₂), ∀ (i : ι), T (b i) = b₂ i

Two affine bases indexed by the same type are related by an affine equivalence sending each point of the first basis to the corresponding point of the second.

theorem AffineBasis.coord_lineMap {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (b : AffineBasis ι k P) [DecidableEq ι] (i j l : ι) (t : k) : (b.coord i) ((AffineMap.lineMap (b j) (b l)) t) = (AffineMap.lineMap (if i = j then 1 else 0) (if i = l then 1 else 0)) t

The barycentric coordinates relative to an affine basis b of a point of the segment between two of its points: coordinate i of lineMap (b j) (b l) t is the point at t of the segment between the i-th coordinates of b j and b l, each 1 or 0.

theorem AffineBasis.coord_homothety_centroid {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [Fintype ι] [Field k] [CharZero k] [AddCommGroup V] [Module k V] [AddTorsor V P] (b : AffineBasis ι k P) (t : k) (z : P) (i : ι) : (b.coord i) ((AffineMap.homothety (Finset.centroid k Finset.univ ⇑b) t) z) = (1 - t) / ↑(Fintype.card ι) + t * (b.coord i) z

The barycentric coordinates relative to an affine basis b of the image of a point z under the homothety of ratio t about the centroid of b: the homothety moves each coordinate b.coord i z towards the centroid's coordinate 1 / card ι by the factor t.