stalkFunctor_map_germ_apply' — Mathlib

English

Variant of Germ Apply: the equality holds in a variant form that is convenient for simplification rules.

Русский

Вариант применения зародка, равенство в форме, удобной для упрощения.

LaTeX

$$A variant of Germ Apply with a specialized form for simplifications.$$

Lean4

@[simp]
theorem stalkFunctor_map_germ_apply' [ConcreteCategory C FC] {F G : X.Presheaf C} (U : Opens X) (x : X) (hx : x ∈ U)
    (f : F ⟶ G) (s) :
    DFunLike.coe (F := ToHom (F.stalk x) (G.stalk x)) (ConcreteCategory.hom ((stalkFunctor C x).map f))
        (F.germ U x hx s) =
      G.germ U x hx (f.app (op U) s) :=
  stalkFunctor_map_germ_apply U x hx f s

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