map_functorPullback_overForget — Mathlib

English

The equivalence between sieves preserves the top sieve when passing to forgetful functor from Over X.

Русский

Эквивалентность между сдвоями сохраняет верхний севей при переходе к забывающей функторе из Over X.

LaTeX

$$overEquiv Y ⊤ = ⊤$$

Lean4

@[simp]
theorem map_functorPullback_overForget {X : C} {Y : Over X} (R : Presieve Y.left) :
    Presieve.map (Over.forget X) (.functorPullback (Over.forget X) R) = R :=
  by
  refine le_antisymm (map_functorPullback _) fun Z g hg ↦ ?_
  let g' : Over.mk (g ≫ Y.hom) ⟶ Y := Over.homMk g
  exact Presieve.map.of (u := g') hg

Похожие утверждения