next_eq — Mathlib

English

For a morphism f: C1 ⟶ C2 and a relation w between i and j, the forward (next) component satisfies: f.next i = (C1.xNextIso w).hom ≫ f.f j ≫ (C2.xNextIso w).inv.

Русский

Для морфизма f: C1 ⟶ C2 и отношения w между i и j выполняется равенство: f.next i = (C1.xNextIso w).hom ≫ f.f j ≫ (C2.xNextIso w).inv.

LaTeX

$$$f.next i = (C_1.xNextIso w).hom \\circ f.f(j) \\circ (C_2.xNextIso w)^{-1}$$$

Lean4

theorem next_eq (f : Hom C₁ C₂) {i j : ι} (w : c.Rel i j) :
    f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv :=
  by
  obtain rfl := c.next_eq' w
  simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

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