restrictHomEquivHom — Mathlib

English

If G is cover-dense and full, then the whiskering map sends morphisms (P → Q) to morphisms (G.op ∘ P → G.op ∘ Q) bijectively when Q is a sheaf.

Русский

При G, являющемся плотным по подслоям и полноте, отображение через обнесение (whiskeringLeft) между морфизмами дает биекцию, если Q — шейф.

LaTeX

$$$\text{Bij}(((\mathrm{whiskeringLeft}\ C^{op} D^{op} A).op\ G^{{op}}).map : (P \to Q) \to (G^{op} \circ P \to G^{op} \circ Q)).$$$

Lean4

/-- A locally-full and cover-dense functor `G` induces an equivalence between morphisms into a sheaf and
morphisms over the restrictions via `G`.
-/
noncomputable def restrictHomEquivHom : (G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) ≃ (ℱ ⟶ ℱ'.val)
    where
  toFun := sheafHom
  invFun := whiskerLeft G.op
  left_inv := sheafHom_restrict_eq
  right_inv := sheafHom_eq _

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