Bases indexed by `Fin` #

source

noncomputable def Basis.mkFinCons {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R ↥N) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) :

Basis (Fin (n + 1)) R M

Let b be a basis for a submodule N of M. If y : M is linear independent of N and y and N together span the whole of M, then there is a basis for M whose basis vectors are given by Fin.cons y b.

Equations

Basis.mkFinCons y b hli hsp = Basis.mk ⋯ ⋯

source

@[simp]

theorem Basis.coe_mkFinCons {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R ↥N) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N) :

⇑(mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)

source

noncomputable def Basis.mkFinConsOfLE {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N) :

Basis (Fin (n + 1)) R ↥O

Let b be a basis for a submodule N ≤ O. If y ∈ O is linear independent of N and y and N together span the whole of O, then there is a basis for O whose basis vectors are given by Fin.cons y b.

Equations

Basis.mkFinConsOfLE y yO b hNO hli hsp = Basis.mkFinCons ⟨y, yO⟩ (b.map (Submodule.comapSubtypeEquivOfLe hNO).symm) ⋯ ⋯

source

@[simp]

theorem Basis.coe_mkFinConsOfLE {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O) (b : Basis (Fin n) R ↥N) (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N) :