submodule_pow_eq_zero_of_pow_eq_zero

English

If G is an endomorphism of M and N is a submodule with a certain commuting relation between G and the inclusion, then G^k = 0 implies g^k = 0 for the restricted endomorphism g on N.

Русский

Пусть G — концевое отображение M, N — подпространство, удовлетворяющее коммутирующему отношению, тогда G^k = 0 влечёт за собой g^k = 0 для ограниченного отображения g на N.

LaTeX

$$$G \\circ N.\\text{subtype} = N.\\text{subtype} \\circ g \\;\\land\\; G^k = 0 \\Rightarrow g^k = 0.$$$

Lean4

theorem _root_.Module.End.submodule_pow_eq_zero_of_pow_eq_zero {N : Submodule R M} {g : Module.End R N}
    {G : Module.End R M} (h : G.comp N.subtype = N.subtype.comp g) {k : ℕ} (hG : G ^ k = 0) : g ^ k = 0 :=
  by
  ext m
  have hg : N.subtype.comp (g ^ k) m = 0 := by
    rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
  simpa using hg

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