English
The glueing compatibility condition appHom_valid_glue asserts that for any X, Y, f, we have the equality of composites: appHom α X ≫ ℱ'.val.map f = ℱ.map f ≫ α.app (op Y).
Русский
Утверждение совместимости склейки: для любых X, Y и f выполняется равенство композитов: $\mathrm{appHom}_X(\alpha) \circ \mathcal{F}'(f) = \mathcal{F}(f) \circ \alpha_Y$.
LaTeX
$$$\mathrm{appHom}_X(\alpha) \; ; \mathcal{F}'.\text{val}.map f = \mathcal{F}.map f \; ; \alpha.\text{app}(\mathrm{op} Y).$$$
Lean4
/-- (Implementation). The maps given in `appIso` is inverse to each other and gives a `ℱ(X) ≅ ℱ'(X)`.
-/
@[simps]
noncomputable def appIso {ℱ ℱ' : Sheaf K (Type v)} (i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val) (X : D) :
ℱ.val.obj (op X) ≅ ℱ'.val.obj (op X) where
hom := appHom i.hom X
inv := appHom i.inv X
hom_inv_id := by
ext x
apply Functor.IsCoverDense.ext G
intro Y f
simp
inv_hom_id := by
ext x
apply Functor.IsCoverDense.ext G
intro Y f
simp
