XOpIso — Mathlib

English

The diagram composed with XOpIso and d_op commutes with the opposite differential; i.e., the two ways of forming the opposite commute.

Русский

Диаграмма с XOpIso и d_op коммутирует с противоположной дифференциалом.

LaTeX

$$XOpIso_hom_d_op : (XOpIso K i).hom ≫ (d K j i).op = d K.op i j ≫ (XOpIso K j).hom$$

Lean4

/-- The canonical isomorphism `X K.op i ≅ Opposite.op (X K i)`. -/
noncomputable def XOpIso (i : Option ι) : X K.op i ≅ Opposite.op (X K i) :=
  match i with
  | some _ => Iso.refl _
  | none => IsZero.iso (isZero_X _ rfl) (isZero_X K rfl).op

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