map_iff — Mathlib

English

If F preserves and reflects the span, then (sq.map F) is a pushout iff sq is a pushout.

Русский

Если F сохраняет и отражает span, то (sq.map F) является pushout тогда и только тогда, когда sq является pushout.

LaTeX

$$$[\\text{PreservesColimit}(\\operatorname{span} f g, F)] \\land [\\text{ReflectsColimit}(\\operatorname{span} f g, F)] \\Rightarrow ( \\text{IsPushout}((sq.map F)) \\iff \\text{IsPushout}(sq) ).$$$

Lean4

theorem map_iff (F : C ⥤ D) [PreservesColimit (span sq.f₁₂ sq.f₁₃) F] [ReflectsColimit (span sq.f₁₂ sq.f₁₃) F] :
    (sq.map F).IsPushout ↔ sq.IsPushout :=
  ⟨fun h ↦ of_map F h, fun h ↦ h.map F⟩

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