From a1338d6293cabc1d66975a77fa5ea10e26fa592a Mon Sep 17 00:00:00 2001
From: Oliver Nash <github@olivernash.org>
Date: Tue, 23 Nov 2021 16:49:23 +0000
Subject: [PATCH] feat(linear_algebra/affine_space/barycentric_coords): affine
 bases exist over fields (#10333)

Formalized as part of the Sphere Eversion project.
---
 .../affine_space/barycentric_coords.lean      | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/src/linear_algebra/affine_space/barycentric_coords.lean b/src/linear_algebra/affine_space/barycentric_coords.lean
index 42cdfbdfc281f..ef1cb7858788a 100644
--- a/src/linear_algebra/affine_space/barycentric_coords.lean
+++ b/src/linear_algebra/affine_space/barycentric_coords.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import linear_algebra.affine_space.independent
+import linear_algebra.affine_space.finite_dimensional
 import linear_algebra.determinant
 
 /-!
@@ -265,4 +266,37 @@ end
 
 end comm_ring
 
+section field
+
+-- TODO Relax `field` to `division_ring` (results are still true)
+variables [field k] [module k V]
+include V
+
+variables (k V P)
+
+lemma exists_affine_basis : ∃ (s : set P), nonempty (affine_basis ↥s k P) :=
+begin
+  obtain ⟨s, -, h_tot, h_ind⟩ := exists_affine_independent k V (set.univ : set P),
+  refine ⟨s, ⟨⟨(coe : s → P), h_ind, _⟩⟩⟩,
+  rw [subtype.range_coe, h_tot, affine_subspace.span_univ],
+end
+
+variables {k V P}
+
+lemma exists_affine_basis_of_finite_dimensional {ι : Type*} [fintype ι] [finite_dimensional k V]
+  (h : fintype.card ι = finite_dimensional.finrank k V + 1) :
+  nonempty (affine_basis ι k P) :=
+begin
+  obtain ⟨s, ⟨⟨incl, h_ind, h_tot⟩⟩⟩ := affine_basis.exists_affine_basis k V P,
+  haveI : fintype s := fintype_of_fin_dim_affine_independent k h_ind,
+  have hs : fintype.card ι = fintype.card s,
+  { rw h, exact (h_ind.affine_span_eq_top_iff_card_eq_finrank_add_one.mp h_tot).symm, },
+  rw ← affine_independent_equiv (fintype.equiv_of_card_eq hs) at h_ind,
+  refine ⟨⟨_, h_ind, _⟩⟩,
+  rw range_comp,
+  simp [h_tot],
+end
+
+end field
+
 end affine_basis