English
A specialization of the isLocallySurjective lemma for a coherent topology over coherentYoneda scenarios.
Русский
Специальная лемма для epi-обобщения в контексте когерентнойTopology.
LaTeX
$$epi_π_app_zero_of_epi$$
Lean4
theorem isLocallySurjective_π_app_zero_of_isLocallySurjective_map : Sheaf.IsLocallySurjective (c.π.app ⟨0⟩) :=
by
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]
intro X y
have hh : EffectiveEpi (limit.π (preimageDiagram hF X y) ⟨0⟩) :=
h _ fun n ↦ by simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n
refine
⟨limit (preimageDiagram hF X y), limit.π (preimageDiagram hF X y) ⟨0⟩, hh,
(coherentTopology C).yonedaEquiv (hc.lift (cone hF X y)), (?_ : (c.π.app (op 0)).val.app _ _ = _)⟩
simp only [← (coherentTopology C).yonedaEquiv_comp, Functor.const_obj_obj, cone, IsLimit.fac,
NatTrans.ofOpSequence_app, (coherentTopology C).yonedaEquiv_comp, (coherentTopology C).yonedaEquiv_yoneda_map]
rfl
