English
There is a global inverse map ιInvApp which provides a morphism Γ(𝒪_{U_i}, U) → lim (D.diagramOverOpen U) compatible with all gluing data.
Русский
Существует глобальное отображение-обратное ιInvApp: Γ(𝒪_{U_i}, U) → lim (D.diagramOverOpen U), совместимое со всей сшивкой.
LaTeX
$$$ιInvApp : (D.U_i).presheaf.obj (op U) → \lim (D.diagramOverOpen U)$$$
Lean4
/-- `ιInvApp` is the right inverse of `D.ι i` on `U`. -/
theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j = D.diagramOverOpenπ U j :=
by
rw [←
@cancel_mono (f :=
(componentwiseDiagram 𝖣.diagram.multispan _).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 _) ..]
· simp_rw [Category.assoc]
rw [limit.w_assoc]
erw [limit.lift_π_assoc]
rw [Category.comp_id, Category.comp_id]
change _ ≫ _ ≫ (_ ≫ _) ≫ _ = _
rw [congr_app (D.t_id _), id_c_app]
simp_rw [Category.assoc]
rw [← Functor.map_comp_assoc]
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`
erw [IsOpenImmersion.inv_naturality_assoc]
erw [IsOpenImmersion.app_invApp_assoc]
iterate 3 rw [← Functor.map_comp_assoc]
rw [NatTrans.naturality_assoc]
erw [← (D.V (i, j)).presheaf.map_comp]
convert limit.w (componentwiseDiagram 𝖣.diagram.multispan _) (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j)))
· rw [Category.comp_id]
apply (config := { allowSynthFailures := true }) mono_comp
change Mono ((_ ≫ D.f j i).c.app _)
rw [comp_c_app]
apply (config := { allowSynthFailures := true }) mono_comp
· erw [D.ι_image_preimage_eq i j U]
infer_instance
· have : IsIso (D.t i j).c := by apply c_isIso_of_iso
infer_instance
