naturality_apply — Mathlib

English

There exists a unique section that lifts a compatible family across a cover and is compatible with IsSheaf conditions.

Русский

Существует уникальный раздел, который восстанавливает совместимую семью над покрытием и согласуется с условиями IsSheaf.

LaTeX

$$$\\exists!\\, s \\in F.\\text{sections}, \\forall i, s(Y_i) = x_i$$$

Lean4

theorem naturality_apply [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y) (x) :
    ℱ'.1.map i.op (α.app _ x) = α.app _ (ℱ.map i.op x) :=
  by
  have {X Y} (i : X ⟶ Y) (x) : ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
    exact congr_fun (α.naturality i.op).symm x
  refine IsLocallyFull.ext G _ i fun V iVX iVY e ↦ ?_
  simp only [← FunctorToTypes.map_comp_apply, ← op_comp, ← e, this]

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