English
A variant: monotone stabilization principle for Artinian modules.
Русский
Вариант принципа стабилизации для артинановых модулей.
LaTeX
$$$(\\forall f: \\mathbb{N} \\to o(\\Submodule\\ R\\ M))\\, \\exists n, \\forall m \\ge n, f(n) = f(m)$$$
Lean4
theorem isArtinian_of_range_eq_ker [IsArtinian R M] [IsArtinian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
(h : LinearMap.range f = LinearMap.ker g) : IsArtinian R N :=
wellFounded_lt_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])
