unop — Mathlib

Lean4
/-- The homotopy between morphisms in `ShortComplex C` that is induced by a homotopy
between morphisms in `ShortComplex Cᵒᵖ`. -/
@[simps]
def unop {S₁ S₂ : ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) : Homotopy (unopMap φ₁) (unopMap φ₂)
    where
  h₀ := h.h₃.unop
  h₁ := h.h₂.unop
  h₂ := h.h₁.unop
  h₃ := h.h₀.unop
  h₀_f := Quiver.Hom.op_inj h.g_h₃
  g_h₃ := Quiver.Hom.op_inj h.h₀_f
  comm₁ := Quiver.Hom.op_inj (by dsimp; rw [h.comm₃]; abel)
  comm₂ := Quiver.Hom.op_inj (by dsimp; rw [h.comm₂]; abel)
  comm₃ := Quiver.Hom.op_inj (by dsimp; rw [h.comm₁]; abel)
Похожие утверждения