functorMap_commSq_aux — Mathlib

English

Auxiliary lemma establishing a base-case and inductive step for the commutativity relations across the levels of the sequential product.

Русский

Вспомоганная лемма устанавливает базовый случай и индуктивный шаг для соотношений коммутации между уровнями последовательного произведения.

LaTeX

$$$\\forall n,m,k\\; (h:\\, n\\le m)\\; (hh:\\, \\neg(k

Lean4

theorem functorMap_commSq_aux {n m k : ℕ} (h : n ≤ m) (hh : ¬(k < m)) :
    (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
        Pi.π _ k ≫ eqToHom (functorObj_eq_neg (by cutsat : ¬(k < n))) =
      (Pi.π (fun i ↦ if _ : i < m then M i else N i) k) ≫ eqToHom (functorObj_eq_neg hh) :=
  by
  induction h using Nat.leRec with
  | refl => simp
  | @le_succ_of_le m h ih =>
    specialize ih (by cutsat)
    have : homOfLE (by cutsat : n ≤ m + 1) = homOfLE (by cutsat : n ≤ m) ≫ homOfLE (by cutsat : m ≤ m + 1) := by simp
    rw [this, op_comp, Functor.map_comp]
    slice_lhs 2 4 => rw [ih]
    simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ, functorMap,
      dite_eq_ite, limMap_π_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app]
    split_ifs
    simp [dif_neg (by cutsat : ¬(k < m))]

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