underlying_arrow — Mathlib

English

Given a morphism f: Y → Z between subobjects Y,Z of X, the map underlying.map f composed with arrow Z equals arrow Y.

Русский

Для отображения f: Y → Z между подпредметами X стрелка подмножества Z, затем подмножество Y удовлетворяют равенству.

LaTeX

$$$\\text{underlying.map } f \\; \\circ \\arrow Z = \\arrow Y$$$

Lean4

@[reassoc (attr := simp)]
theorem underlying_arrow {X : C} {Y Z : Subobject X} (f : Y ⟶ Z) : underlying.map f ≫ arrow Z = arrow Y :=
  Over.w (representative.map f)

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