congr_symm_apply — Mathlib

English

Let I be an ideal in a commutative ring R, and let f: M ≃ N be a linear isomorphism between R-modules. For every x in the I-adic completion of N, the inverse of the induced congruence map is given by applying the I-adic completion map to the inverse of f; that is, (congr I f).symm x = map I f⁻¹ x.

Русский

Пусть I — идеал кольца R и пусть f: M ≃ N — линейное изоморфизм между R-модулями. Для любого x в I-адической инициализации N, обратное преобразование конгруэнции даёт тот же результат, что и отображение через f⁻¹: (congr I f).symm x = map I f⁻¹ x.

LaTeX

$$$ (congr I f).symm\, x = map I\, f^{-1}\, x $$$

Lean4

@[simp]
theorem congr_symm_apply (f : M ≃ₗ[R] N) (x : AdicCompletion I N) : (congr I f).symm x = map I f.symm x :=
  rfl

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