sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson

English

A standard Nakayama-type equality: the supremum of N with I•N' equals the supremum with J•N'.

Русский

Стандартное равенство типа Найямы: верхняя граница N ⊔ I•N' равна N ⊔ J•N'.

LaTeX

$$$$ N \\oplus I\\cdot N' = N \\oplus J\\cdot N'. $$$$

Lean4

/-- **Nakayama's Lemma** - A slightly more general version of (4) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `smul_le_of_le_smul_of_le_jacobson_bot` for the special case when `J = ⊥`. -/
@[stacks 00DV "(4)"]
theorem sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson {I J : Ideal R} {N N' : Submodule R M} (hN' : N'.FG)
    (hIJ : I ≤ jacobson J) (hNN : N' ≤ N ⊔ I • N') : N ⊔ I • N' = N ⊔ J • N' :=
  ((sup_le_sup_left smul_le_right _).antisymm (sup_le le_sup_left hNN)).trans
    (sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN)

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