opEquiv'_symm_comp — Mathlib

English

For f:Y→X and g: Opp, the symmetric equivalence intertwines with composition: (opEquiv' n a a' h).symm (x ≫ f) = f ≫ (opEquiv' n a a' h).symm x.

Русский

Симметрическая эквивалентность сохраняет композицию: (opEquiv' n a a' h).symm (x ≫ f^{op}) = f ≫ (opEquiv' n a a' h).symm x.

LaTeX

$$$$ (opEquiv' n a a' h)^{-1} (x \\;≫\\; f^{op}) = f^{op} \\;≫\\; (opEquiv' n a a' h)^{-1} x $$$$

Lean4

theorem opEquiv'_symm_comp (f : Y ⟶ X) {n a : ℤ} (x : Opposite.op (Z⟦a⟧) ⟶ (Opposite.op X⟦n⟧)) (a' : ℤ)
    (h : n + a = a') : (opEquiv' n a a' h).symm (x ≫ f.op⟦n⟧') = f ≫ (opEquiv' n a a' h).symm x :=
  Quiver.Hom.op_inj (by simp [opEquiv'_symm_apply, opEquiv_symm_apply])

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