English
If a presheaf is locally surjective in the extensive topology, then it remains locally surjective when restricted to Type-level targets.
Русский
Если презашифр локально сюръективен внутри экстензивной топологии, он сохраняет это свойство при ограничении к типам.
LaTeX
$$$\mathrm{surjective}_{\mathrm{loc}}(f) \Rightarrow \mathrm{locallySurjective}(f)$. $$
Lean4
theorem surjective_of_isLocallySurjective_sheaf_of_types [FinitaryPreExtensive C] {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G)
[PreservesFiniteProducts F] [PreservesFiniteProducts G] (h : Presheaf.IsLocallySurjective (extensiveTopology C) f)
{X : C} : Function.Surjective (f.app (op X)) := by
intro x
replace h := h.1 x
rw [mem_sieves_iff_contains_colimit_cofan] at h
obtain ⟨α, _, Y, π, h, h'⟩ := h
let y : (a : α) → (F.obj ⟨Y a⟩) := fun a ↦ (h' a).choose
let _ : Fintype α := Fintype.ofFinite _
let ht := (Types.productLimitCone (fun a ↦ F.obj ⟨Y a⟩)).isLimit
let ht' :=
(Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
let i : ((a : α) → (F.obj ⟨Y a⟩)) ≅ (F.obj ⟨X⟩) :=
ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso (fun _ ↦ (Iso.refl (F.obj ⟨_⟩))))
refine ⟨i.hom y, ?_⟩
apply Concrete.isLimit_ext _ (isLimitOfPreserves G ht')
intro ⟨a⟩
simp only [Functor.comp_obj, Discrete.opposite_inverse_obj, Functor.op_obj, Discrete.functor_obj, Functor.mapCone_pt,
Cone.whisker_pt, Cocone.op_pt, Cofan.mk_pt, Functor.const_obj_obj, Functor.mapCone_π_app, Cone.whisker_π,
Cocone.op_π, Functor.whiskerLeft_app, NatTrans.op_app, Cofan.mk_ι_app]
rw [← (h' a).choose_spec]
erw [← NatTrans.naturality_apply (φ := f)]
change f.app _ ((i.hom ≫ F.map (π a).op) y) = _
erw [IsLimit.map_π]
rfl
