English
If A' has a forgetful functor to Type and preserves limits, then IsSheaf J P' is equivalent to IsSheaf J (P' ⋙ s).
Русский
Если A' имеет забывающий функтор к Type и сохраняет пределы, тогда IsSheaf J P' эквивалентно IsSheaf J (P' ⋙ s).
LaTeX
$$$IsSheaf(J, P') \iff IsSheaf(J, P'\circ s)$$$
Lean4
theorem exists_app (hx : x.Compatible) (g : Y ⟶ X) :
∃ (φ : F.obj (op Y) ⟶ G.obj (op Y)),
∀ {Z : C} (p : Z ⟶ Y) (hp : S (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app ⟨Over.mk (𝟙 Z)⟩ :=
by
let c : Cone ((Presieve.diagram (Sieve.pullback g S).arrows).op ⋙ G) :=
{ pt := F.obj (op Y)
π :=
{ app := fun ⟨Z, hZ⟩ => F.map Z.hom.op ≫ (x _ hZ).app (op (Over.mk (𝟙 _)))
naturality := by
rintro ⟨Z₁, hZ₁⟩ ⟨Z₂, hZ₂⟩ ⟨f : Z₂ ⟶ Z₁⟩
dsimp
rw [id_comp, assoc]
have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by simp)
simp only [presheafHom_obj, unop_op, Functor.id_obj, op_id, FunctorToTypes.map_id_apply] at H
let φ : Over.mk f.left ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk f.left
have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op
dsimp at H H' ⊢
erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc, ← op_comp, Over.w f] } }
use (hG g).lift c
intro Z p hp
exact ((hG g).fac c ⟨Over.mk p, hp⟩)
