English
The overEquiv is compatible with pullbacks: pushing forward and pulling back yields the same sieve under the appropriate pullback operation.
Русский
overEquiv совместим с вытянутыми: продвижение вперед и возвращение дают один и тот же севей при соответствующем pullback.
LaTeX
$$overEquiv _ (S.pullback f) = (overEquiv _ S).pullback f.left$$
Lean4
theorem overEquiv_pullback {X : C} {Y₁ Y₂ : Over X} (f : Y₁ ⟶ Y₂) (S : Sieve Y₂) :
overEquiv _ (S.pullback f) = (overEquiv _ S).pullback f.left :=
by
ext Z g
dsimp [overEquiv, Presieve.functorPushforward]
constructor
· rintro ⟨W, a, b, h, rfl⟩
exact ⟨W, a ≫ f, b, h, by simp⟩
· rintro ⟨W, a, b, h, w⟩
let T := Over.mk (b ≫ W.hom)
let c : T ⟶ Y₁ := Over.homMk g (by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f])
let d : T ⟶ W := Over.homMk b
refine ⟨T, c, 𝟙 Z, ?_, by simp [T, c]⟩
rw [show c ≫ f = d ≫ a by ext; exact w]
exact S.downward_closed h _
