diagramCompIso_hom_ι — Mathlib

English

Same as the previous item: the inverse of the plusCompIso is the plusLift under the appropriate IsSheaf hypothesis.

Русский

То же самое, что и предыдущий пункт: обратный образ plusCompIso равен plusLift при условиях IsSheaf.

LaTeX

$$(J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus _) F) hP$$

Lean4

@[reassoc (attr := simp)]
theorem diagramCompIso_hom_ι (X : C) (W : (J.Cover X)ᵒᵖ) (i : W.unop.Arrow) :
    (J.diagramCompIso F P X).hom.app W ≫ Multiequalizer.ι ((unop W).index (P ⋙ F)) i = F.map (Multiequalizer.ι _ _) :=
  by
  delta diagramCompIso
  simp

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