Documentation

Mathlib.LinearAlgebra.Basis.Flag

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)) :

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} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] {n : } (b : Basis (Fin n) R M) :
    b.flag (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} :
    b.flag k p ∀ (i : Fin n), i.castSucc < kb 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) :
    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} [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 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 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 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 b.flag)
    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 b.flag
    @[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} :
    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} [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 LinearMap.ker (b.coord 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) :
    b.flag k.castSucc LinearMap.ker (b.dualBasis 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) :
    b.flag i.castSucc b.flag i.succ
    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) :
    b.flag i.castSucc ⩿ b.flag i.succ
    @[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) :
    b.toFlag = Set.range b.flag
    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) :

    Range of Basis.flag as a Flag.

    Equations
    Instances For
      @[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 b.toFlag ∃ (k : Fin (n + 1)), b.flag 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 b.flag)