faithful_sheafPushforwardContinuous

English

There is a canonical isomorphism on each X between the fibers of ℱ and ℱ' determined by i.hom and i.inv; explicitly, appHom i.hom X and appHom i.inv X provide the two inverse maps.

Русский

Существует канонический изоморфизм на каждом X между волокнами ℱ и ℱ' определяемый i.hom и i.inv; явления: appHom i.hom X и appHom i.inv X — образы и обратные образы.

LaTeX

$$$\mathrm{appIso}\ (i,X):\; \mathcal{F}.\mathrm{val}(\mathrm{op} X) \cong \mathcal{F}'.\mathrm{val}(\mathrm{op} X) \text{ with }(\mathrm{hom},\mathrm{inv}) = (\mathrm{appHom}(i.hom,X), \mathrm{appHom}(i.inv,X)).$$$

Lean4

instance faithful_sheafPushforwardContinuous [G.IsContinuous J K] : Faithful (G.sheafPushforwardContinuous A J K) where
  map_injective := by
    intro ℱ ℱ' α β e
    ext1
    apply_fun fun e => e.val at e
    dsimp [sheafPushforwardContinuous] at e
    rw [← sheafHom_eq G α.val, ← sheafHom_eq G β.val, e]

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