English
The composition of germToPullbackStalk with stalkPullbackHom equals the germ on the pullback: germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x = ((pullback C f).obj F).germ _ x hx.
Русский
Сочетание germToPullbackStalk с stalkPullbackHom даёт зародок на обратном канале.
LaTeX
$$germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x = ((pullback C f).obj F).germ _ x hx$$
Lean4
@[ext]
theorem pullback_obj_obj_ext {Z : C} {f : X ⟶ Y} {F : Y.Presheaf C} (U : (Opens X)ᵒᵖ)
{φ ψ : ((pullback C f).obj F).obj U ⟶ Z}
(h :
∀ (V : Opens Y) (hV : U.unop ≤ (Opens.map f).obj V),
((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
((pullback C f).obj F).map (homOfLE hV).op ≫ ψ) :
φ = ψ := by
obtain ⟨U⟩ := U
apply ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F _).hom_ext
rintro ⟨⟨V⟩, ⟨⟩, ⟨b⟩⟩
simpa [pushforwardPullbackAdjunction, Functor.lanAdjunction_unit] using h V (leOfHom b)
