interUnionPullbackConeLift_left — Mathlib

English

The lift of a cone through the apex P = F(U ⊔ V) factors through the left leg of the diagram, matching the component s.fst.

Русский

Поднятие (lift) конуса через вершину F(U ⊔ V) факторизуется слева и совпадает с координатой s.fst.

LaTeX

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

Lean4

theorem interUnionPullbackConeLift_left :
    interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_left).op = s.fst :=
  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.left

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