w

Mathlib.CategoryTheory.MorphismProperty.Representable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.relativelyRepresentable.w

English

The identity hf.fst g ≫ f = F.map (hf.snd g) ≫ g holds in the pullback square.

Русский

Соответствующее тождество hf.fst g ≫ f = F.map (hf.snd g) ≫ g в квадрате вытяжки верно.

LaTeX

$$$ hf.fst g \\;\\circ\\; f = F.map (hf.snd g) \\;\\circ\\; g $$$

Lean4

@[reassoc]
theorem w : hf.fst g ≫ f = F.map (hf.snd g) ≫ g :=
  (hf.isPullback g).w

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

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

Разделы

Аффилиация

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