Documentation

Mathlib.LinearAlgebra.AffineSpace.Basis

Affine bases and barycentric coordinates #

Suppose P is an affine space modelled on the module V over the ring k, and p : ι → P is an affine-independent family of points spanning P. Given this data, each point q : P may be written uniquely as an affine combination: q = w₀ p₀ + w₁ p₁ + ⋯ for some (finitely-supported) weights wᵢ. For each i : ι, we thus have an affine map P →ᵃ[k] k, namely q ↦ wᵢ. This family of maps is known as the family of barycentric coordinates. It is defined in this file.

The construction #

Fixing i : ι, and allowing j : ι to range over the values j ≠ i, we obtain a basis bᵢ of V defined by bᵢ j = p j -ᵥ p i. Let fᵢ j : V →ₗ[k] k be the corresponding dual basis and let fᵢ = ∑ j, fᵢ j : V →ₗ[k] k be the corresponding "sum of all coordinates" form. Then the ith barycentric coordinate of q : P is 1 - fᵢ (q -ᵥ p i).

Main definitions #

TODO #

structure AffineBasis (ι : Type u₁) (k : Type u₂) {V : Type u₃} (P : Type u₄) [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] :
Type (max u₁ u₄)

An affine basis is a family of affine-independent points whose span is the top subspace.

Instances For

    The unique point in a single-point space is the simplest example of an affine basis.

    Equations
    • AffineBasis.instInhabitedAffineBasisPUnitPUnitAddCommGroupAddGroupIsAddTorsorToAddGroupToAddGroupWithOneToRingCommRingModuleToSemiring = { default := { toFun := id, ind' := , tot' := } }
    instance AffineBasis.instFunLike {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] :
    FunLike (AffineBasis ι k P) ι P
    Equations
    • AffineBasis.instFunLike = { coe := AffineBasis.toFun, coe_injective' := }
    theorem AffineBasis.ext {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] {b₁ : AffineBasis ι k P} {b₂ : AffineBasis ι k P} (h : b₁ = b₂) :
    b₁ = b₂
    theorem AffineBasis.ind {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) :
    theorem AffineBasis.tot {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) :
    theorem AffineBasis.nonempty {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) :
    def AffineBasis.reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ι') :
    AffineBasis ι' k P

    Composition of an affine basis and an equivalence of index types.

    Equations
    Instances For
      @[simp]
      theorem AffineBasis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ι') :
      (AffineBasis.reindex b e) = b e.symm
      @[simp]
      theorem AffineBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ι') (i' : ι') :
      (AffineBasis.reindex b e) i' = b (e.symm i')
      @[simp]
      theorem AffineBasis.reindex_refl {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) :
      noncomputable def AffineBasis.basisOf {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) :
      Basis { j : ι // j i } k V

      Given an affine basis for an affine space P, if we single out one member of the family, we obtain a linear basis for the model space V.

      The linear basis corresponding to the singled-out member i : ι is indexed by {j : ι // j ≠ i} and its jth element is b j -ᵥ b i. (See basisOf_apply.)

      Equations
      Instances For
        @[simp]
        theorem AffineBasis.basisOf_apply {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) (j : { j : ι // j i }) :
        (AffineBasis.basisOf b i) j = b j -ᵥ b i
        @[simp]
        theorem AffineBasis.basisOf_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ι') (i : ι') :
        noncomputable def AffineBasis.coord {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) :

        The ith barycentric coordinate of a point.

        Equations
        Instances For
          @[simp]
          theorem AffineBasis.linear_eq_sumCoords {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) :
          @[simp]
          theorem AffineBasis.coord_reindex {ι : Type u_1} {ι' : Type u_2} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (e : ι ι') (i : ι') :
          @[simp]
          theorem AffineBasis.coord_apply_eq {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (i : ι) :
          (AffineBasis.coord b i) (b i) = 1
          @[simp]
          theorem AffineBasis.coord_apply_ne {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {i : ι} {j : ι} (h : i j) :
          (AffineBasis.coord b i) (b j) = 0
          theorem AffineBasis.coord_apply {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [DecidableEq ι] (i : ι) (j : ι) :
          (AffineBasis.coord b i) (b j) = if i = j then 1 else 0
          @[simp]
          theorem AffineBasis.coord_apply_combination_of_mem {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i s) {w : ιk} (hw : Finset.sum s w = 1) :
          @[simp]
          theorem AffineBasis.coord_apply_combination_of_not_mem {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : is) {w : ιk} (hw : Finset.sum s w = 1) :
          @[simp]
          theorem AffineBasis.sum_coord_apply_eq_one {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] (q : P) :
          (Finset.sum Finset.univ fun (i : ι) => (AffineBasis.coord b i) q) = 1
          @[simp]
          theorem AffineBasis.affineCombination_coord_eq_self {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] (q : P) :
          ((Finset.affineCombination k Finset.univ b) fun (i : ι) => (AffineBasis.coord b i) q) = q
          @[simp]
          theorem AffineBasis.linear_combination_coord_eq_self {ι : Type u_1} {k : Type u_3} {V : Type u_4} [AddCommGroup V] [Ring k] [Module k V] [Fintype ι] (b : AffineBasis ι k V) (v : V) :
          (Finset.sum Finset.univ fun (i : ι) => (AffineBasis.coord b i) v b i) = v

          A variant of AffineBasis.affineCombination_coord_eq_self for the special case when the affine space is a module so we can talk about linear combinations.

          theorem AffineBasis.ext_elem {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Finite ι] {q₁ : P} {q₂ : P} (h : ∀ (i : ι), (AffineBasis.coord b i) q₁ = (AffineBasis.coord b i) q₂) :
          q₁ = q₂
          @[simp]
          theorem AffineBasis.coe_coord_of_subsingleton_eq_one {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Subsingleton ι] (i : ι) :
          (AffineBasis.coord b i) = 1
          theorem AffineBasis.surjective_coord {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Nontrivial ι] (i : ι) :
          noncomputable def AffineBasis.coords {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) :
          P →ᵃ[k] ιk

          Barycentric coordinates as an affine map.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem AffineBasis.coords_apply {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) (q : P) (i : ι) :
            @[simp]
            theorem AffineBasis.coord_apply_centroid {ι : Type u_1} {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i s) :
            (AffineBasis.coord b i) (Finset.centroid k s b) = (s.card)⁻¹
            theorem AffineBasis.exists_affine_subbasis {k : Type u_3} {V : Type u_4} {P : Type u_5} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] {t : Set P} (ht : affineSpan k t = ) :
            ∃ s ⊆ t, ∃ (b : AffineBasis (s) k P), b = Subtype.val
            theorem AffineBasis.exists_affineBasis (k : Type u_3) (V : Type u_4) (P : Type u_5) [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] :
            ∃ (s : Set P) (b : AffineBasis (s) k P), b = Subtype.val