# Flag of submodules defined by a basis #

In this file we define Basis.flag b k, where b : Basis (Fin n) R M, k : Fin (n + 1), to be the subspace spanned by the first k vectors of the basis b.

def Basis.flag {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) (k : Fin (n + 1)) :

The subspace spanned by the first k vectors of the basis b.

Equations
Instances For
@[simp]
theorem Basis.flag_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) :
b.flag 0 =
@[simp]
theorem Basis.flag_last {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) :
b.flag () =
theorem Basis.flag_le_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) {k : Fin (n + 1)} {p : } :
b.flag k p ∀ (i : Fin n), i.castSucc < kb i p
theorem Basis.flag_succ {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) (k : Fin n) :
b.flag k.succ = Submodule.span R {b k} b.flag k.castSucc
theorem Basis.self_mem_flag {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} (h : i.castSucc < k) :
b i b.flag k
@[simp]
theorem Basis.self_mem_flag_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } [] (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} :
b i b.flag k i.castSucc < k
theorem Basis.flag_mono {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) :
Monotone b.flag
theorem Basis.isChain_range_flag {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) :
IsChain (fun (x x_1 : ) => x x_1) (Set.range b.flag)
theorem Basis.flag_strictMono {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } [] (b : Basis (Fin n) R M) :
StrictMono b.flag
@[simp]
theorem Basis.flag_le_ker_coord_iff {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } [] (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} :
b.flag k LinearMap.ker (b.coord l) k l.castSucc
theorem Basis.flag_le_ker_coord {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} (h : k l.castSucc) :
b.flag k LinearMap.ker (b.coord l)
theorem Basis.flag_le_ker_dual {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (b : Basis (Fin n) R M) (k : Fin n) :
b.flag k.castSucc LinearMap.ker (b.dualBasis k)
theorem Basis.flag_covBy {K : Type u_1} {V : Type u_2} [] [] [Module K V] {n : } (b : Basis (Fin n) K V) (i : Fin n) :
b.flag i.castSucc b.flag i.succ
theorem Basis.flag_wcovBy {K : Type u_1} {V : Type u_2} [] [] [Module K V] {n : } (b : Basis (Fin n) K V) (i : Fin n) :
b.flag i.castSucc ⩿ b.flag i.succ
@[simp]
theorem Basis.toFlag_carrier {K : Type u_1} {V : Type u_2} [] [] [Module K V] {n : } (b : Basis (Fin n) K V) :
b.toFlag = Set.range b.flag
def Basis.toFlag {K : Type u_1} {V : Type u_2} [] [] [Module K V] {n : } (b : Basis (Fin n) K V) :
Flag ()

Range of Basis.flag as a Flag.

Equations
Instances For
@[simp]
theorem Basis.mem_toFlag {K : Type u_1} {V : Type u_2} [] [] [Module K V] {n : } (b : Basis (Fin n) K V) {p : } :
p b.toFlag ∃ (k : Fin (n + 1)), b.flag k = p
theorem Basis.isMaxChain_range_flag {K : Type u_1} {V : Type u_2} [] [] [Module K V] {n : } (b : Basis (Fin n) K V) :
IsMaxChain (fun (x x_1 : ) => x x_1) (Set.range b.flag)