full_sheafPushforwardContinuous — Mathlib

English

There is an equivalence between morphisms G.op ∘ ℱ ⟶ G.op ∘ ℱ'.val and morphisms ℱ ⟶ ℱ'.val; i.e., restriction along G induces a bijection of Hom-sets.

Русский

Существует эквивалентность между морфизмами $G^{op} \circ \mathcal{F} \to G^{op} \circ \mathcal{F}'.val$ и морфизмами $\mathcal{F} \to \mathcal{F}'.val$; ограничение по G задаёт биекцию множеств гомоморфизмов.

LaTeX

$$$(G^{op}\circ \mathcal{F} \to G^{op}\circ \mathcal{F}'.val) \cong (\mathcal{F} \to \mathcal{F}'.val).$$$

Lean4

instance full_sheafPushforwardContinuous [G.IsContinuous J K] : Full (G.sheafPushforwardContinuous A J K) where
  map_surjective α := ⟨⟨sheafHom α.val⟩, Sheaf.Hom.ext <| sheafHom_restrict_eq α.val⟩

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