English
Intersections sieve propagates through pullbacks with sieve operations.
Русский
Перемещение пересечений sieve через вытягивания и операции sieve.
LaTeX
$$$ (E.inter F).sieve_1 = \\mathrm{bind}(E.sieve_1, (\\lambda... ).pullback) $$$
Lean4
theorem sieve₁_inter [HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C} {p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)}
{p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)} (w : p₁ ≫ pullback.fst _ _ ≫ E.f _ = p₂ ≫ pullback.fst _ _ ≫ E.f _) :
(inter E F).sieve₁ p₁ p₂ =
Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst _ _) (p₂ ≫ pullback.fst _ _))
(fun _ f _ ↦ (F.sieve₁ (p₁ ≫ pullback.snd _ _) (p₂ ≫ pullback.snd _ _)).pullback f) :=
by
ext Y f
let p : W ⟶ pullback ((inter E F).f i) ((inter E F).f j) := pullback.lift p₁ p₂ w
refine ⟨fun ⟨k, a, h₁, h₂⟩ ↦ ?_, fun ⟨Z, a, b, ⟨k, e, h₁, h₂⟩, ⟨l, u, u₁, u₂⟩, hab⟩ ↦ ?_⟩
· refine ⟨pullback p ((E.inter F).toPullback k), pullback.lift f a ?_, pullback.fst _ _, ?_, ?_, ?_⟩
· apply pullback.hom_ext
· apply pullback.hom_ext <;> simp [p, h₁, toPullback]
· apply pullback.hom_ext <;> simp [p, h₂, toPullback]
· refine ⟨k.1, pullback.snd _ _ ≫ pullback.fst _ _, ?_, ?_⟩
· have : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = p ≫ pullback.fst _ _ ≫ pullback.fst _ _ := by simp [p]
simp [this, pullback.condition_assoc, toPullback]
· have : p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = p ≫ pullback.snd _ _ ≫ pullback.fst _ _ := by simp [p]
simp [this, pullback.condition_assoc, toPullback]
· exact ⟨k.2, a ≫ pullback.snd _ _, by simp [reassoc_of% h₁], by simp [reassoc_of% h₂]⟩
· simp
· subst hab
refine ⟨(k, l), pullback.lift (a ≫ e) u ?_, ?_, ?_⟩
· simp only [Category.assoc] at u₁
simp [← reassoc_of% h₁, w, ← reassoc_of% u₁, ← pullback.condition]
· apply pullback.hom_ext
· simp [h₁]
· simpa using u₁
· apply pullback.hom_ext
· simp [h₂]
· simpa using u₂
