isArtinian_of_quotient_of_artinian

English

If there exist linear maps f: M → N and g: N → P with range f = ker g, then N is Artinian provided M and P are Artinian.

Русский

Если существуют линейные отображения f: M → N и g: N → P с range f = ker g, то N артинанов при условии, что M и P артинановы.

LaTeX

$$$[IsArtinian\\ R\\ M] \\land [IsArtinian\\ R\\ P] \\land (f: M \\to\\_l[R]\\ N) \\land (g: N \\to\\_l[R]\\ P) \\land (LinearMap.range f = LinearMap.ker g) \\Rightarrow IsArtinian\\ R\\ N$$$

Lean4

instance isArtinian_of_quotient_of_artinian (N : Submodule R M) [IsArtinian R M] : IsArtinian R (M ⧸ N) :=
  isArtinian_of_surjective M (Submodule.mkQ N) (Submodule.Quotient.mk_surjective N)

Похожие утверждения