instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan

English

If F creates limits of shape WalkingCospan and J has pullbacks, then J.comap F has pullbacks.

Русский

Если F создаёт пределы формы WalkingCospan и J имеет pullbacks, тогда J.comap F имеет pullbacks.

LaTeX

$$$ (J.comap F) \\text{ HasPullbacks}$$$

Lean4

instance [CreatesLimitsOfShape WalkingCospan F] [HasPullbacks J] : HasPullbacks (J.comap F) where
  hasPullbacks_of_mem {X Y} R f
    hR := by
    refine ⟨fun {Z g} hg ↦ ?_⟩
    have : (Presieve.map F R).HasPullbacks (F.map f) := J.hasPullbacks_of_mem (F.map f) hR
    have : HasPullback (F.map g) (F.map f) := (R.map F).hasPullback _ (R.map_map hg)
    exact .of_createsLimit F g f

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