smul_top_inf_eq_smul_of_isSMulRegular_on_quot

English

If a module M is regular by r, and its quotient M/N is regular by r, then M′ is regular by r (in a short exact sequence).

Русский

Если модуль M регулярен по r, а фактор-модуль M/N регулярен по r, то точная последовательность даёт, что M′ регулярен по r.

LaTeX

$$$IsSMulRegular M r \wedge IsSMulRegular (M/N) r \Rightarrow IsSMulRegular M' r$$$

Lean4

theorem smul_top_inf_eq_smul_of_isSMulRegular_on_quot : IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N :=
  by
  convert map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp using 2
  exact Eq.trans (congrArg (· ⊓ N) (map_top _)) (map_comap_eq _ _).symm

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