English
The sieve zero of the cylinder is generated by a pullback-based construction using E.f, F.sieve1', and a lift from a pullback.
Русский
sieve0 цилиндра образуется генерацией из оснастки по ударам E.f, F.sieve1' и подъема через вытяжку из вытянутого диагоналя.
LaTeX
$$$ (cylinder\\ f\\ g).sieve_0 = \\mathrm{Sieve}.generate(\\mathrm{Presieve}.bindOfArrows\\ _\\ E.f \\vert\\\\|\\| (\\mathrm{Sieve}.pullback(\\mathrm{pullback}.lift\\ (f.h_0\\ _)\\ (g.h_0\\ _) (\\mathrm{by simp}))\\ (F.sieve_1'\\ _\\ _)).arrows )$$$
Lean4
theorem sieve₀_cylinder :
(cylinder f g).sieve₀ =
Sieve.generate
(Presieve.bindOfArrows _ E.f <| fun i ↦
(Sieve.pullback (pullback.lift (f.h₀ _) (g.h₀ _) (by simp)) (F.sieve₁' _ _)).arrows) :=
by
refine le_antisymm ?_ ?_
· rw [PreZeroHypercover.sieve₀, Sieve.generate_le_iff]
rintro - - ⟨i⟩
refine ⟨_, 𝟙 _, (cylinder f g).f _, ⟨_, _, ?_⟩, by simp⟩
simp only [Sieve.pullback_apply, pullback.condition]
exact Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ _) _
· rw [Sieve.generate_le_iff, PreZeroHypercover.sieve₀]
rintro Z u ⟨i, v, ⟨W, o, o', ⟨j⟩, hoo'⟩⟩
exact ⟨_, pullback.lift v o hoo'.symm, (cylinder f g).f ⟨i, j⟩, Presieve.ofArrows.mk _, by simp⟩
