English
Assuming pullbacks exist, the uncurry of pullbackArrows b s equals the image of s.uncurry under the map f ↦ ⟨pullback f.2 b, pullback.snd f.snd b⟩.
Русский
При условии существования пульебратов, распакованный пресейв pullbackArrows b s равен образу s.uncurry под отображением, отправляющим f на ⟨pullback f.2 b, pullback.snd f.snd b⟩.
LaTeX
$$$(pullbackArrows\\ b\\ s).uncurry = \\mathrm{image}\\Big(\\lambda f, \\langle \\mathrm{pullback}(f.2,b), \\mathrm{pullback.snd}(f.snd,b) \\rangle \\Big)\\ s.uncurry$$$
Lean4
@[simp]
theorem uncurry_pullbackArrows [HasPullbacks C] {B : C} (b : B ⟶ X) :
(pullbackArrows b s).uncurry = (fun f ↦ ⟨pullback f.2 b, pullback.snd _ _⟩) '' s.uncurry :=
by
ext ⟨Z, v⟩; constructor
· rintro ⟨Y, u, hu⟩; exact ⟨⟨Y, u⟩, hu, rfl⟩
· rintro ⟨⟨Y, u⟩, hu, h⟩
rw [Sigma.ext_iff] at h
obtain ⟨rfl, h⟩ := h
rw [heq_iff_eq] at h; subst h
exact ⟨Y, u, hu⟩
