commShift_natTrans_op_int — Mathlib

English

Equality expressing that the inverse of the unit at X is obtained by composing the op-shift inverse components with the unit components for the appropriate indices.

Русский

Равенство, показывающее, что обратная единица в X получается через композицию обратной части сдвига и единицы для соответствующих индексов.

LaTeX

$$$ (opShiftFunctorEquivalence C p).unitIso.inv.app X = ((shiftFunctorAdd' Cᵒᵖ n m p (by cutsat)).hom.app X).unop⟦p⟧').op ≫ ((shiftFunctorAdd' C m n p h).inv.app _).op ≫ ((opShiftFunctorEquivalence C m).unitIso.inv.app (X⟦n⟧)).unop⟦n⟧').op ≫ (opShiftFunctorEquivalence C n).unitIso.inv.app X $$$

Lean4

noncomputable scoped instance commShift_natTrans_op_int {G : C ⥤ D} [G.CommShift ℤ] (τ : F ⟶ G)
    [NatTrans.CommShift τ ℤ] : NatTrans.CommShift (NatTrans.op τ) ℤ :=
  inferInstanceAs
    (NatTrans.CommShift
      (PullbackShift.natTrans (AddMonoidHom.mk' (fun (n : ℤ) => -n) (by intros; dsimp; cutsat))
        (OppositeShift.natTrans ℤ τ))
      ℤ)

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