opEquiv'_zero_add_symm — Mathlib

English

If a = a, the symmetric inverse of opEquiv' evaluated at zero addition reduces to shiftFunctorZero's inverse, i.e., the symmetric inverse of opEquiv' with a = 0 yields a canonical unop shift.

Русский

При нулевом сложении симметричное отображение opEquiv' сводится к обратному к shiftFunctorZero.

LaTeX

$$$$ (opEquiv'_zero_add_symm)\\ \text{(a)}\\ (f) = (shiftFunctorZero C^op Z).hom.app _ .unop \\circ f.unop $$$$

Lean4

theorem opEquiv'_zero_add_symm (a : ℤ) (f : Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦(0 : ℤ)⟧) :
    (opEquiv' 0 a a (zero_add a)).symm f = ((shiftFunctorZero Cᵒᵖ ℤ).hom.app _).unop ≫ f.unop := by
  simp [opEquiv'_symm_apply, opEquiv_symm_apply, shiftFunctorAdd'_add_zero,
    opShiftFunctorEquivalence_zero_unitIso_inv_app]

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