diagramPullback — Mathlib

English

A technical lemma about multiequalizers in the pullback diagram ensuring compatibility of maps.

Русский

Техническая лемма о мультик-равносмножителях в диаграмме вытягивания, обеспечивающая совместимость отображений.

LaTeX

$$Eq (… lift …) (… lift …)$$

Lean4

/-- A helper definition used to define the morphisms for `plus`. -/
@[simps]
def diagramPullback {X Y : C} (f : X ⟶ Y) : J.diagram P Y ⟶ (J.pullback f).op ⋙ J.diagram P X
    where
  app
    S :=
    Multiequalizer.lift _ _ (fun I => Multiequalizer.ι (S.unop.index P) I.base) fun I =>
      Multiequalizer.condition (S.unop.index P) (Cover.Relation.mk' I.r.base)
  naturality S T f := Multiequalizer.hom_ext _ _ _ (fun I => by simp; rfl)

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