pushforwardFamily_apply — Mathlib

English

The section_extracts formula demonstrates how the section obtained from hx.section_ matches the original elements on each Y_i.

Русский

Разделение, полученное из hx.section_, совпадает с исходными элементами на каждом Y_i.

LaTeX

$$$\\text{section\_apply}(i) : (hx.section_ hY hF).1 (op (Y_i)) = x_i$$$

Lean4

@[simp]
theorem pushforwardFamily_apply [G.IsLocallyFull K] {X} (x : ℱ.obj (op X)) {Y : C} (f : G.obj Y ⟶ X) :
    pushforwardFamily α x f (Presieve.in_coverByImage G f) = α.app (op Y) (ℱ.map f.op x) :=
  by
  simp only [pushforwardFamily_def, op_obj]
  generalize Nonempty.some (Presieve.in_coverByImage G f) = l
  obtain ⟨W, iYW, iWX, rfl⟩ := l
  simp only [← op_comp, ← FunctorToTypes.map_comp_apply, naturality_apply]

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