English
The fst projection of the pullback cone is given by the restriction map from F(U ⊔ V) to F(U).
Русский
Первая проекция конуса-пулбека равна отображению ограничения F(U ⊔ V) → F(U).
LaTeX
$$$(\\text{interUnionPullbackCone } F U V).fst = F.1.map( (\\mathrm{homOfLE}\\ inf\\_le\\_left) ).op$$$
Lean4
/-- (Implementation).
Every cone over `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)` factors through `F(U ⊔ V)`.
-/
def interUnionPullbackConeLift : s.pt ⟶ F.1.obj (op (U ⊔ V)) :=
by
let ι : ULift.{w} WalkingPair → Opens X := fun j => WalkingPair.casesOn j.down U V
have hι : U ⊔ V = iSup ι := by
ext
rw [Opens.coe_iSup, Set.mem_iUnion]
constructor
· rintro (h | h)
exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
· rintro ⟨⟨_ | _⟩, h⟩
exacts [Or.inl h, Or.inr h]
refine
(F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.lift
⟨s.pt,
{ app := ?_
naturality := ?_ }⟩ ≫
F.1.map (eqToHom hι).op
· rintro ((_ | _) | (_ | _))
exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op, s.snd ≫ F.1.map (homOfLE inf_le_left).op]
rintro ⟨i⟩ ⟨j⟩ f
let g : j ⟶ i := f.unop
have : f = g.op := rfl
clear_value g
subst this
rcases i with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩) <;> rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩) <;> rcases g with ⟨⟩ <;>
dsimp [Pairwise.diagram] <;>
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
rw [← cancel_mono (F.1.map (eqToHom <| inf_comm U V : U ⊓ V ⟶ _).op), Category.assoc, Category.assoc, ← F.1.map_comp,
← F.1.map_comp]
exact s.condition.symm
