appHom_restrict — Mathlib

English

Naturality of appHom with respect to a morphism f: op X ⟶ op(G.obj Y) states that composing appHom_X(α) with ℱ'.val.map f equals composing α.app(op Y) with ℱ.map f.

Русский

Естественность аппХом относительно морфизма f: op X ⟶ op(G.obj Y): композиция \mathcal{F}'(f) ∘ \mathrm{appHom}_X(\alpha) равна композиции \alpha_{\mathrm{op} Y} ∘ \mathcal{F}(f).

LaTeX

$$$\mathcal{F}'.val.map f \circ \mathrm{appHom}_X(\alpha) = \alpha.app (\mathrm{op} Y) \circ \mathcal{F}.map f.$$$

Lean4

@[simp]
theorem appHom_restrict {X : D} {Y : C} (f : op X ⟶ op (G.obj Y)) (x) :
    ℱ'.val.map f (appHom α X x) = α.app (op Y) (ℱ.map f x) :=
  (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ'.cond _ (G.is_cover_of_isCoverDense _ X)).valid_glue
        (pushforwardFamily_compatible α x) f.unop (Presieve.in_coverByImage G f.unop)).trans
    (pushforwardFamily_apply _ _ _)

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