mk₀_comp — Mathlib

English

If F has a shift sequence and preserves zero morphisms, then for every n ∈ M, the shifted functor F.shift n preserves zero morphisms.

Русский

Если F имеет последовательность сдвигов и сохраняет нулевые морфизмы, тогда для каждого n ∈ M сдвигающий функтор F.shift n сохраняет нулевые морфизмы.

LaTeX

$$theorem instPreservesZeroMorphismsShift {n : M} : (F.shift n).PreservesZeroMorphisms$$

Lean4

theorem mk₀_comp (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M} (g : ShiftedHom Y Z a) :
    (mk₀ m₀ hm₀ f).comp g (by rw [hm₀, add_zero]) = f ≫ g :=
  by
  subst hm₀
  simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']

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