map_iff — Mathlib

English

Let F be a functor with preserves and reflects for span f g. Then IsPullback (F.map f) ... ↔ IsPullback f g h i, provided the equation f h = g i holds.

Русский

Пусть F сохраняет и отражает для span f g. Тогда IsPullback (F.map f) ... ↔ IsPullback f g h i при условии равенства f h = g i.

LaTeX

$$$ \\operatorname{IsPullback}(F.map f,F.map g,F.map h,F.map i) \\iff \\operatorname{IsPullback}(f,g,h,i) $$$

Lean4

theorem map_iff {D : Type*} [Category D] (F : C ⥤ D) [PreservesLimit (cospan h i) F] [ReflectsLimit (cospan h i) F]
    (e : f ≫ h = g ≫ i) : IsPullback (F.map f) (F.map g) (F.map h) (F.map i) ↔ IsPullback f g h i :=
  ⟨fun h => h.of_map F e, fun h => h.map F⟩

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