fac'

Mathlib.CategoryTheory.Sites.CoverLifting

URI: https://scilib.ai/kg/mathlib#CategoryTheory.RanIsSheafOfIsCocontinuous.fac'

English

Core relation between lift and fac in RanIsSheafIsCocontinuous.

Русский

Основное соотношение между lift и fac в RanIsSheafIsCocontinuous.

LaTeX

$$$\\text{lift} \\;\\text{and} \\; \\text{fac}$$$

Lean4

theorem fac' (j : StructuredArrow (op X) G.op) :
    lift hF hR s ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s j.hom.unop := by apply IsLimit.fac

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

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

Разделы

Аффилиация

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