English
For a sheaf F, the object F(U ⊔ V) is the pullback of the two restriction maps from F(U) and F(V) to F(U ∩ V). This gives the canonical pullback cone expressing the sheaf condition for unions of opens.
Русский
Для сло́я F объект F(U ∪ V) является вытянутым пределом двух отображений ограничений F(U) → F(U ∩ V) и F(V) → F(U ∩ V). Это каноническая связка предела, выражающая условие sheaf для объединения открытых множеств.
LaTeX
$$$\\text{interUnionPullbackCone} : \\mathrm{PullbackCone}(F.1.map(\\mathrm{homOfLE}\\ inf\\_le\\_left).op, F.1.map(\\mathrm{homOfLE}\\ inf\\_le\\_right).op)$$$
Lean4
/-- For a sheaf `F`, `F(U ⊔ V)` is the pullback of `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)`.
This is the pullback cone. -/
def interUnionPullbackCone :
PullbackCone (F.1.map (homOfLE inf_le_left : U ⊓ V ⟶ _).op) (F.1.map (homOfLE inf_le_right).op) :=
PullbackCone.mk (F.1.map (homOfLE le_sup_left).op) (F.1.map (homOfLE le_sup_right).op) <|
by
rw [← F.1.map_comp, ← F.1.map_comp]
congr 1
