English
If M and P are Noetherian and we have f: M → N and g: N → P with range f = ker g, then N is Noetherian.
Русский
Пусть M и P Noetherian и dаны линейные отображения f: M → N и g: N → P такие, что range f = ker g; тогда N Noetherian.
LaTeX
$$$[IsNoetherian R M] \wedge [IsNoetherian R P](f,g,h) \Rightarrow IsNoetherian R N$ где $\operatorname{range} f = \ker g$$$
Lean4
/-- If the first and final modules in an exact sequence are Noetherian,
then the middle module is also Noetherian. -/
theorem isNoetherian_of_range_eq_ker [IsNoetherian R M] [IsNoetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
(h : LinearMap.range f = LinearMap.ker g) : IsNoetherian R N :=
isNoetherian_mk <|
wellFounded_gt_exact_sequence (LinearMap.range f) (Submodule.map ((LinearMap.ker f).liftQ f le_rfl))
(Submodule.comap ((LinearMap.ker f).liftQ f le_rfl)) (Submodule.comap g.rangeRestrict)
(Submodule.map g.rangeRestrict)
(Submodule.gciMapComap <| LinearMap.ker_eq_bot.mp <| Submodule.ker_liftQ_eq_bot _ _ _ le_rfl)
(Submodule.giMapComap g.surjective_rangeRestrict)
(by simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ]) (by simp [Submodule.comap_map_eq, h])
