English
We construct the maps ιInvAppπApp for each i and V in the gluing diagram, providing a morphism from Γ(𝒪_{U_i}, U) to Γ(𝒪_V, U_V) for each V. These maps are assembled to lift to ιInvApp.
Русский
Для каждого i и V в диаграмме сшивки строятся отображения ιInvAppπApp, задающие переходы от глобальных секций к секциям на V; эти отображения собираются в ιInvApp.
LaTeX
$$$ιInvAppπApp : \{i : D.J\} \to \left( (D.U_i).presheaf.obj (op U) \to (D.diagramOverOpen U).obj (op V) \right)$$$
Lean4
/-- (Implementation) We construct the map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V)` for each `V` in the gluing
diagram. We will lift these maps into `ιInvApp`. -/
def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) :
(𝖣.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op j) :=
by
rcases j with (⟨j, k⟩ | j)
· refine D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom ?_)
rw [Functor.op_obj]
congr 1; ext1
dsimp only [Functor.op_obj, Opens.map_coe, unop_op, IsOpenMap.coe_functor_obj]
rw [Set.preimage_preimage]
change (D.f j k ≫ 𝖣.ι j).base ⁻¹' _ = _
congr 4
exact colimit.w 𝖣.diagram.multispan (WalkingMultispan.Hom.fst (j, k))
· exact D.opensImagePreimageMap i j U
