English
The presheaf presheafHom is sheaf for the sieve S.arrows, given appropriate hG assumptions about pullbacks and limits.
Русский
presheafHom является sheaf для сетки S.arrows при подходящих предположениях hG относительно отбора и пределов.
LaTeX
$$Presieve.IsSheafFor(presheafHom F G, S.arrows)$$
Lean4
theorem presheafHom_isSheafFor : Presieve.IsSheafFor (presheafHom F G) S.arrows :=
by
intro x hx
apply existsUnique_of_exists_of_unique
· refine
⟨{ app := fun Y => app hG x hx Y.unop.hom
naturality := by
rintro ⟨Y₁ : Over X⟩ ⟨Y₂ : Over X⟩ ⟨φ : Y₂ ⟶ Y₁⟩
apply (hG Y₂.hom).hom_ext
rintro ⟨Z : Over Y₂.left, hZ⟩
dsimp
rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]
rw [app_cond hG x hx Y₁.hom (Z.hom ≫ φ.left) (by simpa using hZ), ← F.map_comp_assoc, op_comp]
congr 3
simp },
?_⟩
rw [PresheafHom.isAmalgamation_iff _ _ hx]
intro Y g hg
dsimp
have H := app_cond hG x hx g (𝟙 _) (by simpa using hg)
rw [op_id, G.map_id, comp_id, F.map_id, id_comp] at H
exact H.trans (by congr; simp)
· intro y₁ y₂ hy₁ hy₂
rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂
apply NatTrans.ext
ext ⟨Y : Over X⟩
apply (hG Y.hom).hom_ext
rintro ⟨Z : Over Y.left, hZ⟩
dsimp
let φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom
refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))
rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]
