functorPushforward_functor — Mathlib

English

Under a functor e between categories, the pushforward along e.functor relates to the pullback along e.inverse via the pullback along e.unitInv.

Русский

При функторе e между категориями перенос по e.functor связан с объездом по e.inverse через обратное отображение e.unitInv.

LaTeX

$$$S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse$$$

Lean4

theorem functorPushforward_functor (S : Sieve X) (e : C ≌ D) :
    S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse :=
  by
  ext Y iYX
  constructor
  · rintro ⟨Z, iZX, iYZ, hiZX, rfl⟩
    simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)
  · intro H
    exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩

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