English
There is a natural map ιInvApp from Γ(𝒪_{U_i}, U) to the limit of the gluing diagram, which serves as the inverse to the gluing morphism (ι_i).c.app (op U).
Русский
Существование естественного отображения ιInvApp: Γ(𝒪_{U_i}, U) → lim(diagramOverOpen U), являющегося обратным к глу-образному морфингу (ι_i).c.app (op U).
LaTeX
$$$ιInvApp : (D.U_i).presheaf.obj (op U) \to \lim (D.diagramOverOpen U)$$$
Lean4
/-- (Implementation) The natural map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, 𝖣.ι i '' U)`.
This forms the inverse of `(𝖣.ι i).c.app (op U)`. -/
def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) : (D.U i).presheaf.obj (op U) ⟶ limit (D.diagramOverOpen U) :=
limit.lift (D.diagramOverOpen U)
{ pt := (D.U i).presheaf.obj (op U)
π :=
{ app := fun j => D.ιInvAppπApp U (unop j)
naturality := fun {X Y} f' =>
by
induction X with
| op X => ?_
induction Y with
| op Y => ?_
let f : Y ⟶ X := f'.unop; have : f' = f.op := rfl; clear_value f; subst this
rcases f with (_ | ⟨j, k⟩ | ⟨j, k⟩)
· simp
· simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
congr 1
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
-- It remains to show that the blue is equal to red + green in the original diagram.
-- The proof strategy is illustrated in 
-- where we prove red = pink = light-blue = green = blue.
change
D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom _) =
D.opensImagePreimageMap _ _ _ ≫
((D.f k j).c.app _ ≫ (D.t j k).c.app _) ≫ (D.V (j, k)).presheaf.map (eqToHom _)
rw [opensImagePreimageMap_app_assoc]
simp_rw [Category.assoc]
rw [opensImagePreimageMap_app_assoc, (D.t j k).c.naturality_assoc, snd_invApp_t_app_assoc, ←
PresheafedSpace.comp_c_app_assoc]
-- light-blue = green is relatively easy since the part that differs does not involve
-- partial inverses.
have :
D.t' j k i ≫ (π₁ k, i, j) ≫ D.t k i ≫ 𝖣.f i k =
(pullbackSymmetry _ _).hom ≫ (π₁ j, i, k) ≫ D.t j i ≫ D.f i j :=
by
rw [← 𝖣.t_fac_assoc, 𝖣.t'_comp_eq_pullbackSymmetry_assoc, pullbackSymmetry_hom_comp_snd_assoc,
pullback.condition, 𝖣.t_fac_assoc]
rw [congr_app this, PresheafedSpace.comp_c_app_assoc (pullbackSymmetry _ _).hom]
simp_rw [Category.assoc]
congr 1
rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc, NatTrans.naturality_assoc]
simp_rw [Functor.op_obj]
rw [← PresheafedSpace.comp_c_app_assoc, congr_app (pullbackSymmetry_hom_comp_snd _ _)]
simp_rw [Category.assoc, Functor.op_obj, comp_base, Opens.map_comp_obj, TopCat.Presheaf.pushforward_obj_map]
rw [IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.inv_naturality_assoc,
IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc]
repeat rw [← (D.V (j, k)).presheaf.map_comp]
rfl } }
