XOpIso_hom_d_op — Mathlib

English

Explicit proof of XOpIso_hom_d_op: compatibility of XOpIso with d_op in each case of i and j.

Русский

Доказательство совместимости XOpIso и d_op в каждом случае i, j.

LaTeX

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

Lean4

@[reassoc]
theorem XOpIso_hom_d_op (i j : Option ι) : (XOpIso K i).hom ≫ (d K j i).op = d K.op i j ≫ (XOpIso K j).hom :=
  match i, j with
  | none, _ => by simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]
  | some i, some j => by
    dsimp [XOpIso]
    simp only [d_eq _ rfl rfl, op_comp, assoc, id_comp, comp_id]
    rfl
  | some _, none => by simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]

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