map'_comp — Mathlib

English

Let f: R →+* S be a ring hom and M1, M2, M3 be R-modules. For any morphisms l12: M1 → M2 and l23: M2 → M3, the extension-of-scalars map preserves composition: map' f (l12 ≫ l23) = map' f l12 ≫ map' f l23.

Русский

Пусть f: R →+* S — кольцо-гомоморфизм, и M1, M2, M3 — модули над R. Пусть l12: M1 → M2 и l23: M2 → M3 — морфизмы. Тогда отображение расширения скаляров сохраняет композицию: map' f (l12 ≫ l23) = map' f l12 ≫ map' f l23.

LaTeX

$$$map' f (l_{12} \gg l_{23}) = map' f l_{12} \gg map' f l_{23}$$$

Lean4

theorem map'_comp {M₁ M₂ M₃ : ModuleCat.{v} R} (l₁₂ : M₁ ⟶ M₂) (l₂₃ : M₂ ⟶ M₃) :
    map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃ := by
  ext x
  induction x using TensorProduct.induction_on with
  | zero => rfl
  | tmul => rfl
  | add _ _ ihx ihy => rw [map_add, map_add, ihx, ihy]

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