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, including flag_map, Basis.mkFinCons, and mem_flag_iff_repr_eq_zero.

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

Equations

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

@[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.flag_map {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {M₂ : Type u_3} [AddCommMonoid M₂] [Module R M₂] (b : Basis (Fin n) R M) (e : M ≃ₗ[R] M₂) (k : Fin (n + 1)) : (b.map e).flag k = Submodule.map (↑e) (b.flag k)

flag commutes with Basis.map.

theorem Module.Basis.mem_flag_iff_repr_eq_zero {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)} {x : M} : x ∈ b.flag k ↔ ∀ (i : Fin n), k ≤ i.castSucc → (b.repr x) i = 0

x ∈ b.flag k iff b.repr x i = 0 for k ≤ i.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

theorem Module.Basis.span_singleton_le_mkFinCons_flag_succ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {v : M} {W : Submodule R M} {bW : Basis (Fin n) R ↥W} {hli : ∀ (c : R), ∀ x ∈ W, c • v + x = 0 → c = 0} {hsp : ∀ (z : M), ∃ (c : R), z + c • v ∈ W} (k : Fin (n + 1)) : R ∙ v ≤ (mkFinCons v bW hli hsp).flag k.succ

The span of the new head vector lies in the successor flag of Basis.mkFinCons.

theorem Module.Basis.map_flag_le_mkFinCons_flag_succ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {v : M} {W : Submodule R M} {bW : Basis (Fin n) R ↥W} {hli : ∀ (c : R), ∀ x ∈ W, c • v + x = 0 → c = 0} {hsp : ∀ (z : M), ∃ (c : R), z + c • v ∈ W} (k : Fin (n + 1)) : Submodule.map W.subtype (bW.flag k) ≤ (mkFinCons v bW hli hsp).flag k.succ

The image of a flag under Submodule.subtype lies in the successor flag of Basis.mkFinCons.

@[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

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

Equations

• b.toFlag = Flag.rangeFin b.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)