A vector followed by a basis of a hyperplane

Let V be a vector space of dimension k + 1, W a subspace and b a basis of W indexed by Fin k. For any v ∉ W, the vectors v, b 0, …, b (k - 1) form a basis of V (Module.Basis.mkFinConsOfNotMem). This is Mathlib's Module.Basis.mkFinCons for vector spaces, where the dimension count replaces the hypothesis that v and W together span V.

Over any commutative ring, if a basis c of V is v followed by a basis b of W, then u ↦ c.det (v, u) is the determinant with respect to b (Module.Basis.det_finCons_eq_det). In particular, v followed by a basis of W has nonzero determinant with respect to every basis of V (Module.Basis.det_finCons_ne_zero).

Reindexing a basis along finCongr and then precomposing with a Fin.cast is the original basis precomposed with the composite cast (Module.Basis.reindex_finCongr_comp_cast). This identifies the families on which top-degree forms are evaluated when the dimension is written in different but equal ways.

The product of bases b of M and c of N indexed by Fin m and Fin n, reindexed by Fin (m + n), is (b 0, 0), …, (b (m - 1), 0), (0, c 0), …, (0, c (n - 1)) (Module.Basis.coe_prod_reindex_finSumFinEquiv). After a further reindexing it begins with a chosen vector of either factor, followed by the remaining vectors in their order (Module.Basis.coe_prod_reindex_finSumFinEquiv_finCongr, Module.Basis.coe_prod_reindex_finSumFinEquiv_cycleRange). These are the bases of M × N that begin with a vector transverse to a hyperplane of one factor.

Main definitions

• Module.Basis.mkFinConsOfNotMem: the basis v, b 0, …, b (k - 1) of V.

Main results

• Module.Basis.det_finCons_eq_det: the determinant of v followed by a family in W, with respect to a basis beginning with v and continuing with b, is its determinant with respect to b.
• Module.Basis.det_finCons_ne_zero: v followed by a basis of W has nonzero determinant.
• Module.Basis.exists_repr_zero_ne_zero: a nonzero vector has nonzero zeroth coordinate in some basis indexed by Fin (k + 1).
• Module.Basis.exists_basis_finCons_of_apply_eq_one: if a linear functional takes the value one on v, then v followed by a basis of its kernel is a basis.
• Module.Basis.reindex_finCongr_comp_cast: a basis reindexed along finCongr and precomposed with a Fin.cast is the original basis precomposed with a Fin.cast.
• Module.Basis.coe_prod_reindex_finSumFinEquiv: the product basis indexed by Fin (m + n).
• Module.Basis.coe_prod_reindex_finSumFinEquiv_finCongr, Module.Basis.coe_prod_reindex_finSumFinEquiv_cycleRange: the product basis beginning with the first vector of the first or of the second factor.

theorem Module.Basis.reindex_finCongr_comp_cast {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {k m m' : ℕ} (b : Basis (Fin m) R M) (h : m = m') (h' : k = m') : ⇑(b.reindex (finCongr h)) ∘ Fin.cast h' = ⇑b ∘ Fin.cast ⋯

A basis reindexed along finCongr h and precomposed with Fin.cast h' is the original basis precomposed with the composite cast.

theorem Module.Basis.coe_prod_reindex_finSumFinEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {m n : ℕ} (b : Basis (Fin m) R M) (c : Basis (Fin n) R N) : ⇑((b.prod c).reindex finSumFinEquiv) = Fin.append (fun (i : Fin m) => (b i, 0)) fun (j : Fin n) => (0, c j)

The product of bases b and c indexed by Fin m and Fin n, reindexed by Fin (m + n), is (b 0, 0), …, (b (m - 1), 0), (0, c 0), …, (0, c (n - 1)).

theorem Module.Basis.coe_prod_reindex_finSumFinEquiv_finCongr {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {m n : ℕ} (b : Basis (Fin (m + 1)) R M) (c : Basis (Fin n) R N) : ⇑(((b.prod c).reindex finSumFinEquiv).reindex (finCongr ⋯)) = Fin.cons (b 0, 0) (Fin.append (fun (i : Fin m) => (b i.succ, 0)) fun (j : Fin n) => (0, c j))

The product basis of b and c begins with (b 0, 0): reindexed by Fin (m + n + 1), it is (b 0, 0) followed by (b 1, 0), …, (b m, 0), (0, c 0), …, (0, c (n - 1)).

theorem Module.Basis.coe_prod_reindex_finSumFinEquiv_cycleRange {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {m n : ℕ} (b : Basis (Fin m) R M) (c : Basis (Fin (n + 1)) R N) : ⇑(((b.prod c).reindex finSumFinEquiv).reindex ⟨m, ⋯⟩.cycleRange) = Fin.cons (0, c 0) (Fin.append (fun (i : Fin m) => (b i, 0)) fun (j : Fin n) => (0, c j.succ))

Moving (0, c 0) to the front of the product basis of b and c with the cycle Fin.cycleRange m gives (0, c 0) followed by (b 0, 0), …, (b (m - 1), 0), (0, c 1), …, (0, c n).

theorem Module.Basis.det_finCons_eq_det {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {k : ℕ} {W : Submodule R V} {v : V} (b : Basis (Fin k) R ↥W) (c : Basis (Fin (k + 1)) R V) (hc : ⇑c = Fin.cons v (⇑W.subtype ∘ ⇑b)) (u : Fin k → ↥W) : c.det (Fin.cons v (⇑W.subtype ∘ u)) = b.det u

For a basis c of V beginning with v and continuing with a basis b of W, and a family u in W, the determinant of v, u 0, …, u (k - 1) with respect to c is that of u with respect to b: u ↦ c.det (v, u) is an alternating form on W taking the value 1 on b.

noncomputable def Module.Basis.mkFinConsOfNotMem {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {k : ℕ} {W : Submodule K V} (v : V) (b : Basis (Fin k) K ↥W) (hv : v ∉ W) (hV : finrank K V = k + 1) : Basis (Fin (k + 1)) K V

A vector outside a hyperplane, followed by a basis of the hyperplane, is a basis. For a space V of dimension k + 1, a basis b of a subspace W indexed by Fin k and v ∉ W, the vectors v, b 0, …, b (k - 1) form a basis of V.

@[simp]

theorem Module.Basis.coe_mkFinConsOfNotMem {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {k : ℕ} {W : Submodule K V} (v : V) (b : Basis (Fin k) K ↥W) (hv : v ∉ W) (hV : finrank K V = k + 1) : ⇑(mkFinConsOfNotMem v b hv hV) = Fin.cons v (⇑W.subtype ∘ ⇑b)

theorem Module.Basis.det_finCons_ne_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {k : ℕ} {W : Submodule K V} (e : Basis (Fin (k + 1)) K V) (b : Basis (Fin k) K ↥W) {v : V} (hv : v ∉ W) : e.det (Fin.cons v (⇑W.subtype ∘ ⇑b)) ≠ 0

The vectors v, b 0, …, b (k - 1) form a basis. For a basis b of a subspace W of codimension one and v ∉ W, their determinant with respect to any basis of V is nonzero.

theorem Module.Basis.exists_repr_zero_ne_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {k : ℕ} [FiniteDimensional K V] (hk : finrank K V = k + 1) {v : V} (hv : v ≠ 0) : ∃ (b : Basis (Fin (k + 1)) K V), (b.repr v) 0 ≠ 0

A nonzero vector of a finite-dimensional space of dimension k + 1 has nonzero zeroth coordinate in some basis indexed by Fin (k + 1).

theorem Module.Basis.exists_basis_finCons_of_apply_eq_one {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {f : M →ₗ[R] R} {v : M} (hf : f v = 1) {m : ℕ} (b : Basis (Fin m) R ↥f.ker) : ∃ (c : Basis (Fin (m + 1)) R M), c 0 = v ∧ ∀ (i : Fin m), c i.succ = ↑(b i)

If a linear functional f takes the value one on v, then v followed by any basis b of the kernel of f is a basis: M is the direct sum of R v and the kernel of f.