Flags of triangular bases

Let e and b be bases of a vector space indexed by Fin n, with b triangular with respect to e: each b l is a combination of e 0, …, e l. Then b and e define the same flag of subspaces in the sense of Module.Basis.flag. Combined with Module.Basis.mem_flag_iff_repr_eq_zero, a vector in the span of e 0, …, e (j - 1) has vanishing b-coordinates from the j-th on.

For a linearly ordered index type, a family v is triangular with respect to a basis b with diagonal coefficients c when each v i - c i • b i is a combination of the b j with j < i. Its matrix in b is then upper triangular, so its determinant in b is the product of the c i.

Main results

• Module.Basis.flag_eq_of_triangular: a basis triangular with respect to e has the same flag as e.
• Module.Basis.det_eq_prod_of_sub_smul_mem_span: the determinant of a triangular family is the product of its diagonal coefficients.
• Module.Basis.det_pos_of_sub_smul_mem_span: over an ordered ring, a triangular family with positive diagonal coefficients has positive determinant.
• Module.Basis.det_pos_of_sub_smul_mem_span_image_fst_lt: the same for a family indexed by a product ι × κ, triangular with respect to the order on the first factor only.

theorem Module.Basis.flag_eq_of_triangular {K : Type u_1} {E : Type u_2} [DivisionRing K] [AddCommGroup E] [Module K E] {n : ℕ} (b : Basis (Fin n) K E) {e : Basis (Fin n) K E} (htri : ∀ (l i : Fin n), l < i → (e.repr (b l)) i = 0) (k : Fin (n + 1)) : b.flag k = e.flag k

A basis b that is triangular with respect to a basis e (each b l is a combination of e 0, …, e l) has the same flag as e: b 0, …, b (k - 1) and e 0, …, e (k - 1) span the same subspace.

theorem Module.Basis.det_eq_prod_of_sub_smul_mem_span {ι : Type u_3} {R : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] [DecidableEq ι] [LinearOrder ι] (b : Basis ι R M) {v : ι → M} {c : ι → R} (hv : ∀ (i : ι), v i - c i • b i ∈ Submodule.span R (⇑b '' Set.Iio i)) : b.det v = ∏ i : ι, c i

The determinant of a family v that is triangular with respect to a basis b, in the sense that each v i - c i • b i is a combination of the b j with j < i, is the product of the diagonal coefficients c i.

theorem Module.Basis.det_pos_of_sub_smul_mem_span {ι : Type u_3} {R : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] [DecidableEq ι] [LinearOrder ι] [PartialOrder R] [IsStrictOrderedRing R] (b : Basis ι R M) {v : ι → M} {c : ι → R} (hc : ∀ (i : ι), 0 < c i) (hv : ∀ (i : ι), v i - c i • b i ∈ Submodule.span R (⇑b '' Set.Iio i)) : 0 < b.det v

Over an ordered ring, a family v that is triangular with respect to a basis b with positive diagonal coefficients c i, in the sense of Module.Basis.det_eq_prod_of_sub_smul_mem_span, has positive determinant in b.

theorem Module.Basis.det_pos_of_sub_smul_mem_span_image_fst_lt {ι : Type u_3} {κ : Type u_4} {R : Type u_5} {M : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] [Fintype κ] [LinearOrder ι] [DecidableEq κ] [PartialOrder R] [IsStrictOrderedRing R] (b : Basis (ι × κ) R M) {v : ι × κ → M} {c : ι × κ → R} (hc : ∀ (p : ι × κ), 0 < c p) (hv : ∀ (p : ι × κ), v p - c p • b p ∈ Submodule.span R (⇑b '' {r : ι × κ | r.1 < p.1})) : 0 < b.det v

Over an ordered ring, a family v indexed by ι × κ that is triangular with respect to a basis b with positive diagonal coefficients c p, in the sense that each v p - c p • b p is a combination of the b r with r.1 < p.1, has positive determinant in b. This is Module.Basis.det_pos_of_sub_smul_mem_span for a lexicographic order on the index type; the order on κ plays no role, since the hypothesis only compares first coordinates.