shiftFunctorAdd'_assoc — Mathlib

English

A coherence condition expresses that shifting by a1+a2 then a3 equals shifting by a1 and then a2+a3 up to the natural isomorphisms and associator.

Русский

Согласование сдвига на a1+a2 затем a3 эквивалентно сдвигу на a1, затем a2+a3, с учётом естественных изоморфизмов и ассоциатора.

LaTeX

$$$\\text{ShiftAdd}(a_1+a_2,a_3) = \\text{ShiftAdd}'(a_1,a_2+a_3)$$$

Lean4

theorem shiftFunctorAdd'_assoc (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
    (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) :
    shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (by rw [← h₁₂, h₁₂₃]) ≪≫
        isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) _ ≪≫ associator _ _ _ =
      shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (by rw [← h₂₃, ← add_assoc, h₁₂₃]) ≪≫
        isoWhiskerLeft _ (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃) :=
  by
  subst h₁₂ h₂₃ h₁₂₃
  ext X
  dsimp
  simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.comp_id]
  dsimp [shiftFunctorAdd']
  simp only [eqToHom_app]
  dsimp [shiftFunctorAdd, shiftFunctor]
  simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map, eqToHom_app]
  erw [δ_μ_app_assoc, Category.assoc]
  rfl

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