English
The sieve1' in the cylinder is the pullback of a map constructed from pullback.map and the previous sieves.
Русский
sieve1' цилиндра является вытягиванием через отображение pullback.map и ранее образующих sieve.
LaTeX
$$$ (cylinder\\ f\\ g).sieve_1'\\ i\\ j = \\mathrm{Sieve}.pullback(\\mathrm{pullback}.map\\ _\\ _\\ _\\ _ (\\mathrm{pullback}.fst\\ _\\ _) (\\mathrm{pullback}.fst\\ _\\ _) (\\mathbb{1} S) (\\cdots))\\ (E.sieve_1'\\ i.1\\ j.1)$$$
Lean4
theorem sieve₁'_cylinder (i j : Σ (i : E.I₀), F.I₁ (f.s₀ i) (g.s₀ i)) :
(cylinder f g).sieve₁' i j =
Sieve.pullback (pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝟙 S) (by simp) (by simp))
(E.sieve₁' i.1 j.1) :=
by
refine le_antisymm ?_ ?_
· rw [sieve₁', Sieve.ofArrows, Sieve.generate_le_iff]
rintro - - ⟨k⟩
refine ⟨E.Y k.down, pullback.snd _ _, E.toPullback k.down, Presieve.ofArrows.mk k.down, ?_⟩
simp only [cylinder_Y, cylinder_f, toPullback_cylinder, pullback.condition]
· rw [sieve₁', Sieve.ofArrows, ← Sieve.pullbackArrows_comm, Sieve.generate_le_iff]
rintro Z u ⟨W, v, ⟨k⟩⟩
simp_rw [← pullbackSymmetry_inv_comp_fst]
apply (((cylinder f g).sieve₁' i j)).downward_closed
rw [sieve₁']
convert Sieve.ofArrows_mk _ _ (ULift.up k)
simp [toPullback_cylinder f g ⟨k⟩]
