glue_condition — Mathlib

English

For indices i and j, t i j composed with f j i and ι j equals f i j composed with ι i.

Русский

Для индексов i и j композиция t i j с f j i и ι j равна композиции f i j с ι i.

LaTeX

$$$D.t i j \\circ D.f j i \\circ D.\\u03bbi j = D.f i j \\circ D\\u03bbi i$$$

Lean4

@[elementwise (attr := simp)]
theorem glue_condition (i j : D.J) : D.t i j ≫ D.f j i ≫ D.ι j = D.f i j ≫ D.ι i :=
  (Category.assoc _ _ _).symm.trans (Multicoequalizer.condition D.diagram ⟨i, j⟩).symm

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