pushforward_comp — Mathlib

English

Pushforward along a composition of functors equals sequential pushforwards: R.pushforward (F ⋙ G) = (R.pushforward F).pushforward G.

Русский

Перемещение вперед вдоль композиции функторов F ⋙ G равно последовательной операции pushforward.

LaTeX

$$$ R.pushforward (F \\circ G) = (R.pushforward F).pushforward G $$$

Lean4

theorem pushforward_comp {f : Y ⟶ X} {g : Z ⟶ Y} (R : Sieve Z) :
    R.pushforward (g ≫ f) = (R.pushforward g).pushforward f :=
  Sieve.ext fun W h =>
    ⟨fun ⟨f₁, hq, hf₁⟩ => ⟨f₁ ≫ g, by simpa, f₁, rfl, hf₁⟩, fun ⟨y, hy, z, hR, hz⟩ =>
      ⟨z, by rw [← Category.assoc, hR]; tauto⟩⟩

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