shiftFunctorCompIsoId_add'_inv_app

English

The add'-inverse expansion expresses the inv.app X for a complex composite of multiple shift inverses in terms of nested inv apps and additive inverses.

Русский

Разложение add'-inverse выражает inv.app X для сложного из композиции обратных сдвигов через вложенные inv.app и обратные суммы.

LaTeX

$$$ (\\mathrm{shiftFunctorCompIsoId} \\ C p' p hp).inv.app X = (\\mathrm{shiftFunctorCompIsoId} \\ C n' n hn).inv.app X \\\\gg (\\mathrm{shiftFunctorCompIsoId} \\ C m' m hm).inv.app (X⟦n'⟧)⟦n⟧' \\\\gg (\\mathrm{shiftFunctorAdd'} \\ C m n p h).inv.app (X⟦n'⟧⟦m'⟧) \\\\gg (\\mathrm{shiftFunctorAdd' } \\ C n' m' p' \\dots).inv.app X $$$

Lean4

theorem shiftFunctorCompIsoId_add'_inv_app :
    (shiftFunctorCompIsoId C p' p hp).inv.app X =
      (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
        (shiftFunctorCompIsoId C m' m hm).inv.app (X⟦n'⟧)⟦n⟧' ≫
          (shiftFunctorAdd' C m n p h).inv.app (X⟦n'⟧⟦m'⟧) ≫
            ((shiftFunctorAdd' C n' m' p'
                    (by rw [← add_left_inj p, hp, ← h, add_assoc, ← add_assoc m', hm, zero_add, hn])).inv.app
                X)⟦p⟧' :=
  by
  dsimp [shiftFunctorCompIsoId]
  simp only [Functor.map_comp, Category.assoc]
  congr 1
  rw [← NatTrans.naturality]
  dsimp
  rw [← cancel_mono ((shiftFunctorAdd' C p' p 0 hp).inv.app X), Iso.hom_inv_id_app, Category.assoc, Category.assoc,
    Category.assoc, Category.assoc, ←
    shiftFunctorAdd'_assoc_inv_app p' m n n' p 0 (by rw [← add_left_inj n, hn, add_assoc, h, hp]) h
      (by rw [add_assoc, h, hp]),
    ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, Category.assoc, Category.assoc,
    shiftFunctorAdd'_assoc_inv_app n' m' m p' 0 n' _ hm (by rw [add_assoc, hm, add_zero]), Iso.hom_inv_id_app_assoc, ←
    shiftFunctorAdd'_add_zero_hom_app, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp, Iso.hom_inv_id_app]

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