mk₀_comp_mk₀_assoc — Mathlib

English

Associativity of nested mk₀ compositions reduces to a single mk₀ of the composite morphism.

Русский

Ассоциативность вложенной композиции mk₀ сводится к одному mk₀ для составного морфизма.

LaTeX

$$theorem mk₀_comp_mk₀_assoc (f : X ⟶ Y) (g : Y ⟶ Z) {a : M} (ha : a = 0) {d : M} (h : ShiftedHom Z T d) : (mk₀ a ha f).comp (mk₀ a ha g) h = (mk₀ a ha (f ≫ g)).comp h$$

Lean4

@[simp]
theorem mk₀_comp_mk₀_assoc (f : X ⟶ Y) (g : Y ⟶ Z) {a : M} (ha : a = 0) {d : M} (h : ShiftedHom Z T d) :
    (mk₀ a ha f).comp ((mk₀ a ha g).comp h (show _ = d by rw [ha, add_zero])) (show _ = d by rw [ha, add_zero]) =
      (mk₀ a ha (f ≫ g)).comp h (by rw [ha, add_zero]) :=
  by
  subst ha
  rw [← comp_assoc, mk₀_comp_mk₀]
  all_goals simp

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