yonedaGluedToSheaf — Mathlib

Lean4
/-- The map from the glued scheme `(glueData hf).glued`, treated as a sheaf, to `F`. -/
noncomputable def yonedaGluedToSheaf : zariskiTopology.yoneda.obj (glueData hf).glued ⟶ F where
  -- The map is obtained by finding an object of `F((glueData hf).glued)`.
  val :=
    yonedaEquiv.symm
      ((glueData hf).sheafValGluedMk (fun i ↦ yonedaEquiv (f i))
        (by
          intro i j
          apply yonedaEquiv.symm.injective
          dsimp only [glueData_V, glueData_J, glueData_U, glueData_f, glueData_t]
          rw [yonedaEquiv_naturality, Equiv.symm_apply_apply, FunctorToTypes.map_comp_apply, yonedaEquiv_naturality,
            yonedaEquiv_naturality, Equiv.symm_apply_apply, ← Functor.map_comp_assoc,
            Functor.relativelyRepresentable.symmetry_fst, ((hf i).rep.isPullback' (f j)).w]))
Похожие утверждения