transport

Mathlib.CategoryTheory.Limits.Shapes.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.ImageMap.transport

Lean4

/-- To give an image map for a commutative square with `f` at the top and `g` at the bottom, it
suffices to give a map between any mono factorisation of `f` and any image factorisation of `g`. -/
def 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) :
    ImageMap sq where
  map := image.lift F ≫ map ≫ hF'.lift (Image.monoFactorisation g.hom)
  map_ι := by simp [map_ι]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru