English
For a finite family of linear maps, if the kernels are independent in the sense of SupIndep, then the kernel of the noncommutative product equals the supremum of the kernels.
Русский
Для конечного множества линейных отображений, если ядра линейных отображений тяже SupIndep, то ядро произведения равно объёму суммируемых ядер.
LaTeX
$$$[\operatorname{FiniteDimensional}_K V] {\iota} ~{f}: {\iota \to V \to V} (s: Finset \iota) (comm) (h: s.SupIndep( \lambda i, \ker (f i))) : \ker( s.noncommProd f comm ) = \bigvee_{i \in s} \ker (f i)$$$
Lean4
theorem ker_noncommProd_eq_of_supIndep_ker [FiniteDimensional K V] {ι : Type*} {f : ι → V →ₗ[K] V} (s : Finset ι) (comm)
(h : s.SupIndep fun i ↦ ker (f i)) : ker (s.noncommProd f comm) = ⨆ i ∈ s, ker (f i) := by
classical
induction s using Finset.induction_on with
| empty => simp [Module.End.one_eq_id]
| insert i s hi
ih =>
replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) = ⨆ x ∈ s, ker (f x) :=
ih _ (h.subset (s.subset_insert i))
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp, ker_comp_eq_of_commute_of_disjoint_ker]
· simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
· exact s.noncommProd_commute _ _ _ fun j hj ↦ comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by aesop)
· replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
simpa [ih, hi, Finset.sup_eq_iSup] using h
