mapMultiforkOfIsLimit_ι — Mathlib

English

simp version of the ι-map equation for multifork is valid.

Русский

Упрощенная версия равенства для ι-части отображения multifork.

LaTeX

$$@[simp] theorem mapMultiforkOfIsLimit_ι {E F : PreOneHypercover S} (f : E.Hom F) (P : Cᵒᵖ ⥤ A) {c : Multifork (E.multicospanIndex P)} (hc : IsLimit c) (d : Multifork (F.multicospanIndex P)) (a : E.I₀) : f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op$$

Lean4

@[reassoc (attr := simp)]
theorem mapMultiforkOfIsLimit_ι {E F : PreOneHypercover.{w} S} (f : E.Hom F) (P : Cᵒᵖ ⥤ A)
    {c : Multifork (E.multicospanIndex P)} (hc : IsLimit c) (d : Multifork (F.multicospanIndex P)) (a : E.I₀) :
    f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op := by simp [mapMultiforkOfIsLimit]

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