English
There is an explicit R-linear equivalence between the quotient of I^n by I^(n+1) and the image under the quotient map of I^n inside I^n, implemented compatibly with the quotient maps and scalar actions.
Русский
Существует явное R-линейное эквивалентное отображение между фактор-модулем I^n / I^(n+1) и образом под фактором I^n внутри I^n, совместимое с отображениями факторизации и скалярными действиями.
LaTeX
$${$((I^n) / (I^{n+1})) \cong \mathrm{Ideal.map}(\mathrm{Quotient.mk}(I^{n+1}))(I^n)$}$$
Lean4
/-- The linear map from `M ⧸ I ^ m • ⊤` to `M ⧸ I ^ n • ⊤` induced by
the natural inclusion `I ^ n • ⊤ → I ^ m • ⊤`.
To future contributors: Before adding lemmas related to `Submodule.factorPow`, please
check whether it can be generalized to `Submodule.factor` and whether the
corresponding (more general) lemma for `Submodule.factor` already exists.
-/
abbrev factorPow {m n : ℕ} (le : m ≤ n) : M ⧸ (I ^ n • ⊤ : Submodule R M) →ₗ[R] M ⧸ (I ^ m • ⊤ : Submodule R M) :=
factor (smul_mono_left (Ideal.pow_le_pow_right le))
