pushforwardFamily — Mathlib

English

Naturality of pushforward along pullback respects composition of arrows in the base category.

Русский

Натуральность перемещения по обратному отображению сохраняет композицию стрелок в базе.

LaTeX

$$$\\text{naturality of pushforward}$$$

Lean4

/-- (Implementation). Given a section of `ℱ` on `X`, we can obtain a family of elements valued in `ℱ'`
that is defined on a cover generated by the images of `G`. -/
noncomputable def pushforwardFamily {X} (x : ℱ.obj (op X)) : FamilyOfElements ℱ'.val (coverByImage G X) := fun _ _ hf =>
  ℱ'.val.map hf.some.lift.op <| α.app (op _) (ℱ.map hf.some.map.op x)

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