transport — Mathlib

English

There is a transportation construction that, given a square sq and compatible mono-factorisations, yields a HasImageMap.

Русский

Существет конструкция переноса, которая дан квадрат sq и совместимые монофакторизации, образует HasImageMap.

LaTeX

$$$ \\text{transport}(sq, F, F', map, map\\_ι) : HasImageMap\\sq $$$

Lean4

theorem transport {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) (F : MonoFactorisation f.hom)
    {F' : MonoFactorisation g.hom} (hF' : IsImage F') (map : F.I ⟶ F'.I) (map_ι : map ≫ F'.m = F.m ≫ sq.right) :
    HasImageMap sq :=
  HasImageMap.mk <| ImageMap.transport sq F hF' map_ι

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