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.

We also prove some lemmas about this definition.

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

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

Equations

• Basis.flag b k = Submodule.span R (⇑b '' {i : Fin n | Fin.castSucc i < k})

@[simp]

theorem Basis.flag_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) : Basis.flag b 0 = ⊥

@[simp]

theorem Basis.flag_last {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) : Basis.flag b (Fin.last n) = ⊤

theorem Basis.flag_le_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) {k : Fin (n + 1)} {p : Submodule R M} : Basis.flag b k ≤ p ↔ ∀ (i : Fin n), Fin.castSucc i < k → b i ∈ p

theorem Basis.flag_succ {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (k : Fin n) : Basis.flag b (Fin.succ k) = Submodule.span R {b k} ⊔ Basis.flag b (Fin.castSucc k)

theorem Basis.self_mem_flag {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} (h : Fin.castSucc i < k) : b i ∈ Basis.flag b k

@[simp]

theorem Basis.self_mem_flag_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} [Nontrivial R] (b : Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)} : b i ∈ Basis.flag b k ↔ Fin.castSucc i < k

theorem Basis.flag_mono {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) : Monotone (Basis.flag b)

theorem Basis.isChain_range_flag {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) : IsChain (fun (x x_1 : Submodule R M) => x ≤ x_1) (Set.range (Basis.flag b))

theorem Basis.flag_strictMono {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} [Nontrivial R] (b : Basis (Fin n) R M) : StrictMono (Basis.flag b)

@[simp]

theorem Basis.flag_le_ker_coord_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} [Nontrivial R] (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} : Basis.flag b k ≤ LinearMap.ker (Basis.coord b l) ↔ k ≤ Fin.castSucc l

theorem Basis.flag_le_ker_coord {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} (h : k ≤ Fin.castSucc l) : Basis.flag b k ≤ LinearMap.ker (Basis.coord b l)

theorem Basis.flag_le_ker_dual {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {n : ℕ} (b : Basis (Fin n) R M) (k : Fin n) : Basis.flag b (Fin.castSucc k) ≤ LinearMap.ker ((Basis.dualBasis b) k)

theorem Basis.flag_covBy {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Basis (Fin n) K V) (i : Fin n) : Basis.flag b (Fin.castSucc i) ⋖ Basis.flag b (Fin.succ i)

theorem Basis.flag_wcovBy {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Basis (Fin n) K V) (i : Fin n) : Basis.flag b (Fin.castSucc i) ⩿ Basis.flag b (Fin.succ i)

@[simp]

theorem Basis.toFlag_carrier {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Basis (Fin n) K V) : ↑(Basis.toFlag b) = Set.range (Basis.flag b)

def Basis.toFlag {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Basis (Fin n) K V) : Flag (Submodule K V)

Range of Basis.flag as a Flag.

Equations

• Basis.toFlag b = Flag.rangeFin (Basis.flag b) ⋯ ⋯ ⋯

@[simp]

theorem Basis.mem_toFlag {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Basis (Fin n) K V) {p : Submodule K V} : p ∈ Basis.toFlag b ↔ ∃ (k : Fin (n + 1)), Basis.flag b k = p

theorem Basis.isMaxChain_range_flag {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Basis (Fin n) K V) : IsMaxChain (fun (x x_1 : Submodule K V) => x ≤ x_1) (Set.range (Basis.flag b))