interUnionPullbackConeLift_right — Mathlib

English

The lift of a cone through the apex factors through the right leg, matching s.snd.

Русский

Поднятие конуса через вершину делится на правую ветвь диаграммы и совпадает с координатой s.snd.

LaTeX

$$$\\text{interUnionPullbackConeLift } F U V s \\\\ ≫ F.1.map( (\\mathrm{homOfLE}\\ le\\_sup\\_right).op) = s.snd$$$

Lean4

theorem interUnionPullbackConeLift_right :
    interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_right).op = s.snd :=
  by
  erw [Category.assoc]
  simp_rw [← F.1.map_comp]
  exact
    (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <|
      op <| Pairwise.single <| ULift.up WalkingPair.right

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