functorPushforward_over_map — Mathlib

English

The pushforward of the symmetric overEquiv of a sieve along an arrow f corresponds to the overEquiv of the pushforward along f.

Русский

Пушфорвард симметричного overEquiv с севеем вдоль стрелки f соответствует overEquiv от пушфорварда вдоль f.

LaTeX

$$Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv Z).symm S) = (Sieve.overEquiv ((Over.map f).obj Z)).symm S$$

Lean4

@[simp]
theorem functorPushforward_over_map {X Y : C} (f : X ⟶ Y) (Z : Over X) (S : Sieve Z.left) :
    Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv Z).symm S) =
      (Sieve.overEquiv ((Over.map f).obj Z)).symm S :=
  by
  ext W g
  constructor
  · rintro ⟨T, a, b, ha, rfl⟩
    exact S.downward_closed ha _
  · intro hg
    exact ⟨Over.mk (g.left ≫ Z.hom), Over.homMk g.left, Over.homMk (𝟙 _) (by simpa using Over.w g), hg, by cat_disch⟩

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