germ_stalkPullbackInv — Mathlib

English

Specialization maps compose in the stalk along a chain of specializations: F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h').

Русский

Специализация-марки в стэле композиционно складываются вдоль цепочки специализаций.

LaTeX

$$F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h')$$

Lean4

@[reassoc (attr := simp)]
theorem germ_stalkPullbackInv (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) (V : Opens X) (hV : x ∈ V) :
    ((pullback C f).obj F).germ _ x hV ≫ stalkPullbackInv C f F x = F.germToPullbackStalk _ f V x hV := by
  apply colimit.ι_desc

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