op_δ — Mathlib

English

The opposite of δ equals δ in the opposite category.

Русский

Противоположность δ равна δ в противоположной категории.

LaTeX

$$$S^{op}.\\delta = \\delta^{op}$$$

Lean4

theorem op_δ : S.op.δ = S.δ.op :=
  Quiver.Hom.unop_inj
    (by
      rw [Quiver.Hom.unop_op, ← cancel_mono (pushout.inr _ _ : _ ⟶ S.P'), ← cancel_epi (pullback.snd _ _ : S.P ⟶ _),
        S.snd_δ_inr, ← cancel_mono S.P'IsoUnopOpP.hom, ← cancel_epi S.PIsoUnopOpP'.inv, P'IsoUnopOpP, PIsoUnopOpP',
        assoc, assoc, assoc, assoc, pushoutIsoUnopPullback_inr_hom, pullbackIsoUnopPushout_inv_snd_assoc,
        pushoutIsoUnopPullback_inl_hom, pullbackIsoUnopPushout_inv_fst_assoc]
      apply Quiver.Hom.op_inj
      simpa only [op_comp, Quiver.Hom.op_unop, assoc] using S.op.snd_δ_inr)

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