comp_mk₀ — Mathlib

English

Composition with two successive mk₀ constructions is associative with respect to the underlying composition of maps.

Русский

Сочетание двух последовательно построенных mk₀ ассоциативно по отношению к вложенной композиции отображений.

LaTeX

$$theorem comp_mk₀ {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) : f.comp (mk₀ m₀ hm₀ g) = f ≫ g⟦a⟧'$$

Lean4

theorem comp_mk₀ {a : M} (f : ShiftedHom X Y a) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) :
    f.comp (mk₀ m₀ hm₀ g) (by rw [hm₀, zero_add]) = f ≫ g⟦a⟧' :=
  by
  subst hm₀
  simp only [comp, shiftFunctorAdd'_zero_add_inv_app, mk₀, shiftFunctorZero', eqToIso_refl, Iso.refl_trans,
    ← Functor.map_comp, assoc, Iso.inv_hom_id_app, Functor.id_obj, comp_id]

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