English
There exists for each i and U an eq using ιInvApp to relate the projection maps of the gluing diagram with the canonical identification given by 𝒪.
Русский
Для каждого i и U существует равенство, связывающее проекции диаграммы с каноническим тождеством из 𝒪 через ιInvApp.
LaTeX
$$$\exists eq:\, D.ιInvApp U ≫ D.diagramOverOpenπ U i = D.ι i$$$
Lean4
/-- `ιInvApp` is the left inverse of `D.ι i` on `U`. -/
theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) :
∃ eq, D.ιInvApp U ≫ D.diagramOverOpenπ U i = (D.U i).presheaf.map (eqToHom eq) :=
by
fconstructor
-- Porting note: I don't know what the magic was in Lean3 proof, it just skipped the proof of `eq`
· congr; ext1; change _ = _ ⁻¹' (_ '' _); ext1 x
simp only [SetLike.mem_coe, unop_op, Set.mem_preimage, Set.mem_image]
refine ⟨fun h => ⟨_, h, rfl⟩, ?_⟩
rintro ⟨y, h1, h2⟩
convert h1 using 1
delta ι Multicoequalizer.π at h2
apply_fun (D.ι _).base
· exact h2.symm
· have := D.ι_gluedIso_inv (PresheafedSpace.forget _) i
dsimp at this
rw [← this, TopCat.coe_comp]
refine Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)
rw [← TopCat.mono_iff_injective]
infer_instance
delta ιInvApp
rw [limit.lift_π]
change D.opensImagePreimageMap i i U = _
dsimp [opensImagePreimageMap]
rw [congr_app (D.t_id _), id_c_app, ← Functor.map_comp]
erw [IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_inv_app'_assoc]
· simp only [eqToHom_op, ← Functor.map_comp]
rfl
· rw [Set.range_eq_univ.mpr _]
· simp
· rw [← TopCat.epi_iff_surjective]
infer_instance
