functorMap_commSq_succ — Mathlib

English

Two compatibility statements express how functorMap interacts with projections when shifting from n to n+1, ensuring the square commutes for successive levels.

Русский

Два условия совместимости показывают, как functorMap взаимодействует с проекциями при переходе от n к n+1, обеспечивая коммутативность квадрата для последовательных уровней.

LaTeX

$$$\\forall n,\\;\\text{CommSq}_{n}:\\; (\\mathrm{functorMap}\\ M\\ N\\ (n+1))\\; \\text{coincides with the composition of projections and } f_n$$$

Lean4

theorem functorMap_commSq_succ (n : ℕ) :
    (Functor.ofOpSequence (functorMap f)).map (homOfLE (by cutsat : n ≤ n + 1)).op ≫
        Pi.π _ n ≫ eqToHom (functorObj_eq_neg (by cutsat : ¬(n < n))) =
      (Pi.π (fun i ↦ if _ : i < (n + 1) then M i else N i) n) ≫ eqToHom (functorObj_eq_pos (by cutsat)) ≫ f n :=
  by simp [functorMap]

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