English
If f: M → N and g: N → P have FG kernels and f is surjective, then ker(g ∘ f) is finitely generated.
Русский
Если линейные отображения f: M → N и g: N → P имеют FG ядра, и f сюрьективно, тогда ker(g ∘ f) порождается конечным множеством.
LaTeX
$$Linear maps with FG kernels: ker(g ∘ f) FG if ker f FG and ker g FG and f surjective$$
Lean4
/-- The kernel of the composition of two linear maps is finitely generated if both kernels are and
the first morphism is surjective. -/
theorem fg_ker_comp (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf1 : (LinearMap.ker f).FG) (hf2 : (LinearMap.ker g).FG)
(hsur : Function.Surjective f) : (LinearMap.ker (g.comp f)).FG :=
by
rw [LinearMap.ker_comp]
apply fg_of_fg_map_of_fg_inf_ker f
· rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]
· rwa [inf_of_le_right (show (LinearMap.ker f) ≤ (LinearMap.ker g).comap f from comap_mono bot_le)]
