ofIsoComp

Mathlib.CategoryTheory.Limits.Shapes.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.MonoFactorisation.ofIsoComp

Lean4

/-- A mono factorisation of `g ≫ f`, where `g` is an isomorphism,
gives a mono factorisation of `f`. -/
@[simps]
def ofIsoComp {X' : C} (g : X' ⟶ X) [IsIso g] (F : MonoFactorisation (g ≫ f)) : MonoFactorisation f
    where
  I := F.I
  m := F.m
  e := inv g ≫ F.e

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

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

Разделы

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

Аффилиация

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