map_comp — Mathlib

English

Localization commutes with composition: map S f0 f2 (h ∘ g) equals map S f1 f2 h ∘ map S f0 f1 g.

Русский

Локализация сохраняет композицию: map S f0 f2 (h ∘ g) = map S f1 f2 h ∘ map S f0 f1 g.

LaTeX

$$$$ \\text{map } S f_0 f_2 (h \\circ g) = \\text{map } S f_1 f_2 h \\circ \\text{map } S f_0 f_1 g $$$$

Lean4

theorem map_comp (h : M →ₗ[R] N) : (map S f g h) ∘ₗ f = g ∘ₗ h :=
  lift_comp S f (g ∘ₗ h) (IsLocalizedModule.map_units g)

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