map_comp_map_s — Mathlib

English

For a left fraction φ and a functor L with left-inverted property hL, the map respects composition with the left fraction's s: φ.map L hL ≫ L.map φ.s = L.map φ.f.

Русский

Для левой дроби φ и функторa L с свойством обратимости hL отображение сохраняет композицию с левым элементом дроби: φ.map L hL ≫ L.map φ.s = L.map φ.f.

LaTeX

$$\left(\phi.map L hL\right) \circ L.map(\phi.s) = L.map(\phi.f)$$

Lean4

@[reassoc (attr := simp)]
theorem map_comp_map_s (φ : W.LeftFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    φ.map L hL ≫ L.map φ.s = L.map φ.f := by
  letI := hL _ φ.hs
  simp [map]

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