w — Mathlib · SciLib

English

Let A and B be objects of the structured-arrow category over T with fixed S. For every morphism f : A ⟶ B in StructuredArrow S T, the underlying right component and the left data commute, i.e. A.hom followed by T.map f.right equals B.hom.

Русский

Пусть A и B — объекты в категории структурированной стрелки над T с фиксированным S. Для любого морфизма f : A ⟶ B в StructuredArrow S T выполнено равенство: A.hom затем T.map f.right равно B.hom, то есть диаграмма слева направо коммутирует.

LaTeX

$$$\forall f:\, A \to B,\ A.hom \;\circ \ T.map\, f.right = B.hom$$$

Lean4

@[reassoc (attr := simp)]
theorem w {A B : StructuredArrow S T} (f : A ⟶ B) : A.hom ≫ T.map f.right = B.hom := by have := f.w; cat_disch

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