English
There is an induction principle on the rank of a submodule: given a property P on submodules and an inductive step ih describing how to extend P from smaller submodules to larger ones by adjoining a new independent vector, P holds for all submodules when the standard rank-parameter conditions are met.
Русский
Существует принцип индукции по рангa подпространств: для свойства P на подпространства вводится переход ih, описывающий переход from меньших подпространств к большим путем присоединения нового линейно независимого вектора; тогда P выполняется для всех подпространств при выполнении соответствующих условий ранга.
LaTeX
$$$\\text{InductionOnRankAux}(b,P,ih,n,N,rank\\_le) = P N$$$
Lean4
/-- If `N` is a submodule with finite rank, do induction on adjoining a linear independent
element to a submodule. -/
def inductionOnRankAux (b : Basis ι R M) (P : Submodule R M → Sort*)
(ih : ∀ N : Submodule R M, (∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = (0 : M) → c = 0) → P N') → P N)
(n : ℕ) (N : Submodule R M)
(rank_le : ∀ {m : ℕ} (v : Fin m → N), LinearIndependent R ((↑) ∘ v : Fin m → M) → m ≤ n) : P N :=
by
haveI : DecidableEq M := Classical.decEq M
have Pbot : P ⊥ := by
apply ih
intro N _ x x_mem x_ortho
exfalso
rw [mem_bot] at x_mem
simpa [x_mem] using x_ortho 1 0 N.zero_mem
induction n generalizing N with
| zero =>
suffices N = ⊥ by rwa [this]
apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)
| succ n rank_ih =>
apply ih
intro N' N'_le x x_mem x_ortho
apply rank_ih
intro m v hli
refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
convert hli.fin_cons' x _ ?_
· ext i
refine Fin.cases ?_ ?_ i <;> simp
· intro c y hcy
refine x_ortho c y (Submodule.span_le.mpr ?_ y.2) hcy
rintro _ ⟨z, rfl⟩
exact (v z).2
