functorPushforward_comp — Mathlib

English

Pushing forward along a composed functor is the same as pushing forward step by step: (F ⋙ G)-pushforward equals G-pushforward of F-pushforward.

Русский

Перенос по композиции функторов равен переносу по частям: pushforward по F⋙G эквивалентен pushforward по G после F.

LaTeX

$$$R\\!\\!\\!\\text{functorPushforward}(F \\cdot G) = \\big( R\\!\\!\\text{functorPushforward } F \\big)\\!\\text{ functorPushforward } G$$$

Lean4

theorem functorPushforward_comp (R : Presieve X) :
    R.functorPushforward (F ⋙ G) = (R.functorPushforward F).functorPushforward G :=
  by
  funext x
  ext f
  constructor
  · rintro ⟨X, f₁, g₁, h₁, rfl⟩
    exact ⟨F.obj X, F.map f₁, g₁, ⟨X, f₁, 𝟙 _, h₁, by simp⟩, rfl⟩
  · rintro ⟨X, f₁, g₁, ⟨X', f₂, g₂, h₁, rfl⟩, rfl⟩
    exact ⟨X', f₂, g₁ ≫ G.map g₂, h₁, by simp⟩

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