map_comp — Mathlib

English

The induced map on adic completions respects composition: map I g ∘ map I f = map I (g ∘ f).

Русский

Полученное отображение на адических завершениях сохраняет композицию: map I g ∘ map I f = map I (g ∘ f).

LaTeX

$$$\mathrm{map}\ I\ g \circ_\mathrm{L} \mathrm{map}\ I\ f = \mathrm{map}\ I\ (g \circ_\mathrm{L} f)$$$

Lean4

theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] P) : map I g ∘ₗ map I f = map I (g ∘ₗ f) :=
  by
  ext
  simp

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