comm_to — Mathlib

English

For a morphism f: C1 ⟶ C2 and any j, we have a commutativity relation at the To side: f.prev j ≫ C2.dTo j = C1.dTo j ≫ f.f j.

Русский

Для морфизма f: C1 ⟶ C2 и любого j выполняется сопряженная условие на стороне To: f.prev j ≫ C2.dTo j = C1.dTo j ≫ f.f j.

LaTeX

$$$f.prev j \\circ C_2.dTo j = C_1.dTo j \\circ f.f j$$$

Lean4

@[reassoc, elementwise]
theorem comm_to (f : Hom C₁ C₂) (j : ι) : f.prev j ≫ C₂.dTo j = C₁.dTo j ≫ f.f j :=
  f.comm _ _

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