English
An auxiliary form of the commutativity lemma parameterized by n, m and k, providing the inductive mechanism for the sequence of projections.
Русский
Вспомогательная форма леммы коммутации, параметризованная n, m, k, обеспечивающая индуктивный механизм для последовательности проекций.
LaTeX
$$$\\forall n,m,k:\\; \\text{auxiliary commutativity condition}$$$
Lean4
theorem functorMap_commSq {n m : ℕ} (h : ¬(m < n)) :
(Functor.ofOpSequence (functorMap f)).map (homOfLE (by cutsat : n ≤ m + 1)).op ≫
Pi.π _ m ≫ eqToHom (functorObj_eq_neg (by cutsat : ¬(m < n))) =
(Pi.π (fun i ↦ if _ : i < m + 1 then M i else N i) m) ≫ eqToHom (functorObj_eq_pos (by cutsat)) ≫ f m :=
by
cases m with
| zero =>
have : n = 0 := by omega
subst this
simp [functorMap]
| succ m =>
rw [← functorMap_commSq_succ f (m + 1)]
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite, Functor.ofOpSequence_map_homOfLE_succ]
have :
homOfLE (by cutsat : n ≤ m + 1 + 1) = homOfLE (by cutsat : n ≤ m + 1) ≫ homOfLE (by cutsat : m + 1 ≤ m + 1 + 1) :=
by simp
rw [this, op_comp, Functor.map_comp]
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ, Category.assoc]
congr 1
exact functorMap_commSq_aux f (by cutsat) (by cutsat)
