English
For each i and open U, the componentwise projection π is an isomorphism with explicit inverse given by ιInvAppπApp and ιInvApp.
Русский
Для каждого i и открытого U проекция по компонентам является изоморфизмом с явным обратным отображением через ιInvAppπApp и ιInvApp.
LaTeX
$$$(D.\mathrm{diagramOverOpen}\,U)_i \cong (D.diagramOverOpen U).obj(\mathrm{op}\,i)$$$
Lean4
/-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
Vᵢⱼ ⟶ Uᵢ
| |
↓ ↓
Uⱼ ⟶ X
-/
def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
PullbackCone.isLimitAux' _ fun s => by
refine ⟨?_, ?_, ?_, ?_⟩
· refine PresheafedSpace.IsOpenImmersion.lift (D.f i j) s.fst ?_
erw [← D.toTopGlueData.preimage_range j i]
have : s.fst.base ≫ D.toTopGlueData.ι i = s.snd.base ≫ D.toTopGlueData.ι j :=
by
rw [← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _, ← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _]
have := congr_arg PresheafedSpace.Hom.base s.condition
rw [comp_base, comp_base] at this
replace this := reassoc_of% this
exact this _
simp only [mapGlueData_U, forget_obj]
rw [← Set.image_subset_iff, ← Set.image_univ, ← Set.image_comp, Set.image_univ, ← TopCat.coe_comp, this,
TopCat.coe_comp, ← Set.image_univ, Set.image_comp]
exact Set.image_subset_range _ _
· apply IsOpenImmersion.lift_fac
· rw [← cancel_mono (𝖣.ι j), Category.assoc, ← (𝖣.vPullbackCone i j).condition]
conv_rhs => rw [← s.condition]
erw [IsOpenImmersion.lift_fac_assoc]
· intro m e₁ _
rw [← cancel_mono (D.f i j)]
simp only [lift_fac]
tauto
