English
The forgetful functor from Q.Over to Over of S induces a locally surjective functor in the Grothendieck topology.
Русский
Функтор под забыванием из Q.Over в Over S индуцирует локально сюръективный функтор в топологии Гротендика.
LaTeX
$$$\\text{LocallySurjective} (\\text{forget } Q \\;_{} \\;\\top )$ in $overGrothendieckTopology$$$
Lean4
theorem locallyCoverDense_of_le (hPQ : P ≤ Q) :
(MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S) where
functorPushforward_functorPullback_mem
X := by
intro ⟨T, hT⟩
rw [mem_overGrothendieckTopology] at hT ⊢
obtain ⟨𝒰, h, hle⟩ := hT
use 𝒰, h
rintro - - ⟨i⟩
have p : Q (𝒰.X i ↘ S) := by
rw [← comp_over (𝒰.f i) S]
exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop
use (𝒰.X i).asOverProp S p, MorphismProperty.Over.homMk (𝒰.f i) (comp_over (𝒰.f i) S), 𝟙 _
exact ⟨hle _ ⟨i⟩, rfl⟩
