English
For finite index i, the same span inclusion holds for iInf ker and ker relations of L_i and K.
Русский
Для конечного множества индексов i справедливо то же отношение включения спана и ядер для L_i и K.
LaTeX
$$mem_span_of_iInf_ker_le_ker (I = finite) : K ∈ span range L$$
Lean4
/-- Given some linear forms $L_1, ..., L_n, K$ over a vector space $E$, if
$\bigcap_{i=1}^n \mathrm{ker}(L_i) \subseteq \mathrm{ker}(K)$, then $K$ is in the space generated
by $L_1, ..., L_n$. -/
theorem _root_.mem_span_of_iInf_ker_le_ker [Finite ι] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜} (h : ⨅ i, ker (L i) ≤ ker K) :
K ∈ span 𝕜 (range L) := by
have _ := Fintype.ofFinite ι
let φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
let p := ⨅ i, ker (L i)
have p_eq : p = ker φ := (ker_pi L).symm
let ψ : (E ⧸ p) →ₗ[𝕜] ι → 𝕜 := p.liftQ φ p_eq.le
have _ : FiniteDimensional 𝕜 (E ⧸ p) := of_injective ψ (ker_eq_bot.1 (ker_liftQ_eq_bot' p φ p_eq))
let L' i : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ (L i) (iInf_le _ i)
let K' : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ K h
have : ⨅ i, ker (L' i) ≤ ker K' :=
by
simp_rw +zetaDelta [← ker_pi, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq]
exact bot_le
obtain ⟨c, hK'⟩ := (mem_span_range_iff_exists_fun 𝕜).1 (FiniteDimensional.mem_span_of_iInf_ker_le_ker this)
refine (mem_span_range_iff_exists_fun 𝕜).2 ⟨c, ?_⟩
conv_lhs => enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]
rw [← p.liftQ_mkQ K h]
ext x
convert LinearMap.congr_fun hK' (p.mkQ x)
simp only [L', coeFn_sum, Finset.sum_apply, smul_apply, coe_comp, Function.comp_apply, smul_eq_mul]
