English
The inverse of the overEquiv maps the top sieve to the top sieve.
Русский
Обратное отображение overEquiv отображает верхний севей в верхний севей.
LaTeX
$$(overEquiv Y).symm ⊤ = ⊤$$
Lean4
/-- The equivalence `Sieve Y ≃ Sieve Y.left` for all `Y : Over X`. -/
def overEquiv {X : C} (Y : Over X) : Sieve Y ≃ Sieve Y.left
where
toFun S := Sieve.functorPushforward (Over.forget X) S
invFun S' := Sieve.functorPullback (Over.forget X) S'
left_inv
S := by
ext Z g
dsimp [Presieve.functorPullback, Presieve.functorPushforward]
constructor
· rintro ⟨W, a, b, h, w⟩
let c : Z ⟶ W := Over.homMk b (by rw [← Over.w g, w, assoc, Over.w a])
rw [show g = c ≫ a by ext; exact w]
exact S.downward_closed h _
· intro h
exact ⟨Z, g, 𝟙 _, h, by simp⟩
right_inv
S := by
ext Z g
dsimp [Presieve.functorPullback, Presieve.functorPushforward]
constructor
· rintro ⟨W, a, b, h, rfl⟩
exact S.downward_closed h _
· intro h
exact ⟨Over.mk ((g ≫ Y.hom)), Over.homMk g, 𝟙 _, h, by simp⟩
