map_comp — Mathlib

English

The map on adic completion 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) :=
  rfl

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