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 Module.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.

@[simp]

theorem Module.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) : b.flag 0 = ⊥

@[simp]

theorem Module.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) : b.flag (Fin.last n) = ⊤

theorem Module.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} : b.flag k ≤ p ↔ ∀ (i : Fin n), i.castSucc < k → b i ∈ p

theorem Module.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) : b.flag k.succ = R ∙ b k ⊔ b.flag k.castSucc

theorem Module.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 : i.castSucc < k) : b i ∈ b.flag k

@[simp]

theorem Module.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 ∈ b.flag k ↔ i.castSucc < k

theorem Module.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 b.flag

theorem Module.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 (x1 x2 : Submodule R M) => x1 ≤ x2) (Set.range b.flag)

theorem Module.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 b.flag

@[deprecated Module.Basis.flag_mono (since := "2025-10-20")]

theorem Module.Basis.flag_le_flag {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {b : Basis (Fin n) R M} {i j : Fin (n + 1)} (hij : i ≤ j) : b.flag i ≤ b.flag j

@[deprecated Module.Basis.flag_strictMono (since := "2025-10-20")]

theorem Module.Basis.flag_lt_flag {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {b : Basis (Fin n) R M} {i j : Fin (n + 1)} [Nontrivial R] (hij : i < j) : b.flag i < b.flag j

@[simp]

theorem Module.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} : b.flag k ≤ (b.coord l).ker ↔ k ≤ l.castSucc

theorem Module.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 ≤ l.castSucc) : b.flag k ≤ (b.coord l).ker

theorem Module.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) : b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)

theorem Module.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) : b.flag i.castSucc ⋖ b.flag i.succ

theorem Module.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) : b.flag i.castSucc ⩿ b.flag i.succ

def Module.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.

@[simp]

theorem Module.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) : ↑b.toFlag = Set.range b.flag

@[simp]

theorem Module.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 ∈ b.toFlag ↔ ∃ (k : Fin (n + 1)), b.flag k = p

theorem Module.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 (x1 x2 : Submodule K V) => x1 ≤ x2) (Set.range b.flag)