feat(LinearAlgebra): basis flag lemmas and genEigenspace map

[or4nge19]

Part 1/3 of #39139.
Introduces basis flag lemmas and intertwining genEigenspace map, using directly available constructors, ie introducing none (so improving on #39139)

Co-authored-by: kuotsanhsu learningstud@gmail.com

---

[github-actions]

PR summary 9d846ddeb4

Import changes exceeding 2%

%	File
+3.85%	Mathlib.LinearAlgebra.Basis.Flag

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Basis.Flag	986	1024	+38 (+3.85%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Basis.Flag	38

---

Declarations diff

+ flag_map
+ map_flag_le_mkFinCons_flag_succ
+ map_genEigenspace_le
+ mapsTo_genEigenspace_of_comp
+ mem_flag_iff_repr_eq_zero
+ span_singleton_le_mkFinCons_flag_succ

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[themathqueen]

golf in one-line, and no need for Nontrivial, you can also move this out of the commring section

Suggested change

	theorem mem_flag_iff_repr_eq_zero [Nontrivial R] (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 := by
	constructor
	· intro hx i hi
	have hmem : x ∈ LinearMap.ker (b.coord i) := b.flag_le_ker_coord hi hx
	simpa [Module.Basis.coord_apply] using (LinearMap.mem_ker.mp hmem)
	· intro h
	rw [← b.sum_repr x]
	exact Submodule.sum_mem _ fun i _ => by
	by_cases hi : i.castSucc < k
	· exact Submodule.smul_mem _ _ (b.self_mem_flag hi)
	· rw [h i (le_of_not_gt hi), zero_smul]
	exact Submodule.zero_mem _
	theorem mem_flag_iff_repr_eq_zero (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 := by
	simp [flag, Basis.mem_span_image, Finsupp.support_subset_iff]

[themathqueen]

Suggested change

	obtain ⟨l, hl, hx⟩ := (mem_genEigenspace (f := f) (μ := μ) (k := k)).mp hx
	apply (mem_genEigenspace (f := g) (μ := μ) (k := k)).mpr
	refine ⟨l, hl, ?_⟩
	rw [LinearMap.mem_ker] at hx ⊢
	have hsub (x : M) : (g - μ • 1) (φ x) = φ ((f - μ • 1) x) := by
	have hfg : g (φ x) = φ (f x) := LinearMap.congr_fun hφ x
	simp [LinearMap.sub_apply, hfg]
	have hpow (l : ℕ) (x : M) :
	((g - μ • 1) ^ l) (φ x) = φ (((f - μ • 1) ^ l) x) := by
	induction l with
	| zero => simp
	| succ l ih =>
	rw [pow_succ', pow_succ', Module.End.mul_apply, Module.End.mul_apply, ih, hsub]
	rw [hpow, hx, map_zero]
	obtain ⟨l, hl, hx⟩ := mem_genEigenspace.mp hx
	refine mem_genEigenspace.mpr ⟨l, hl, ?_⟩
	simp only [LinearMap.mem_ker, Module.End.pow_apply] at hx ⊢
	suffices (⇑φ).Semiconj ⇑(f - μ • 1) ⇑(g - μ • 1) by rw [← this.iterate_right, hx, map_zero]
	intro; simpa using congr($hφ _).symm