English
If hH is CoverPreserving and H.IsCoverDense, and IsLocallySurjective J (whiskerLeft H.op f), then IsLocallySurjective K f.
Русский
Если hH сохраняет покрытия и плотность, тогда IsLocallySurjective J(whiskerLeft H.op f) во много раз приводит к IsLocallySurjective K f.
LaTeX
$$$[hH: CoverPreserving J K H] \Rightarrow [H.IsCoverDense K] \Rightarrow IsLocallySurjective J (whiskerLeft H.op f) \Rightarrow IsLocallySurjective K f$$$
Lean4
theorem isLocallySurjective_of_whisker (hH : CoverPreserving J K H) [H.IsCoverDense K]
[IsLocallySurjective J (whiskerLeft H.op f)] : IsLocallySurjective K f where
imageSieve_mem {X}
a := by
apply K.transitive (H.is_cover_of_isCoverDense K X)
intro Y g ⟨⟨Z, lift, m, fac⟩⟩
rw [← fac, Sieve.pullback_comp]
apply K.pullback_stable
have hh := hH.cover_preserve <| imageSieve_mem J (whiskerLeft H.op f) (G.map m.op a)
refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_
refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_) hh
intro W q ⟨x, h⟩
simp only [Sieve.functorPullback_apply, Presieve.functorPullback_mem, Sieve.pullback_apply]
exact ⟨x, by simpa using h⟩
