functorPushforward_inverse — Mathlib

English

For an equivalence e: C ≃ D, and sieve S on X, pushing forward along e.inverse equals the pullback along e.functor of the pullback by e.counit.

Русский

Для эквивалентности e: C ≃ D и щели S на X, перенос вперед через e.inverse равен вытягиванию через e.functor и последующему вытягиванию через e.counit.

LaTeX

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

Lean4

theorem functorPushforward_inverse {X : D} (S : Sieve X) (e : C ≌ D) :
    S.functorPushforward e.inverse = (S.pullback (e.counit.app X)).functorPullback e.functor :=
  Sieve.functorPushforward_functor S e.symm

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