English
There is a compatibility between opens-map images and pullbacks along t and f in the gluing data; i.e., an equality between two ways of transporting sections across pullbacks and opens.
Русский
Согласованность образа открытого отображения и вытаскивания через t и f в данных склейки; равенство между двумя путями переноса секций через вытаскивания и открытые множества.
LaTeX
$$$\\exists eq:\\; D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ = ((π_1 j,i,k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫ (π_2^{-1} j,i,k) (unop _) ≫ (D.V (j,k)).presheaf.map (eqToHom eq)$$$
Lean4
/-- We can prove the `eq` along with the lemma. Thus this is bundled together here, and the
lemma itself is separated below.
-/
theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)).carrier) :
∃ eq,
(π₂⁻¹ i, j, k) U ≫ (D.t k i).c.app _ ≫ (D.V (k, i)).presheaf.map (eqToHom eq) =
(D.t' k i j).c.app _ ≫ (π₁⁻¹ k, j, i) (unop _) :=
by
fconstructor
-- Porting note: I don't know what the magic was in Lean3 proof, it just skipped the proof of `eq`
· delta IsOpenImmersion.opensFunctor
dsimp only [Functor.op, Opens.map, IsOpenMap.functor, unop_op, Opens.coe_mk]
congr 2
have := (𝖣.t_fac k i j).symm
rw [← IsIso.inv_comp_eq] at this
replace this := (congr_arg ((PresheafedSpace.Hom.base ·)) this).symm
replace this := congr_arg (TopCat.Hom.hom ·) this
replace this := congr_arg (ContinuousMap.toFun ·) this
dsimp at this
rw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
swap
· refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
refine congr_arg (_ '' ·) ?_
refine congr_fun ?_ _
refine Set.image_eq_preimage_of_inverse ?_ ?_
· intro x
rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base, ConcreteCategory.id_apply]
· intro x
rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.hom_inv_id, id_base, ConcreteCategory.id_apply]
· rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc, (D.t' k i j).c.naturality_assoc]
simp_rw [← Category.assoc]
dsimp
rw [← comp_c_app, congr_app (D.t_fac k i j), comp_c_app]
dsimp
simp_rw [Category.assoc]
rw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_inv_app'_assoc]
· simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]; rfl
rintro x ⟨y, -, eq⟩
replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq
rw [𝖣.t_inv, id_base, TopCat.id_app] at eq
subst eq
use (inv (D.t' k i j)).base y
change (inv (D.t' k i j) ≫ π₁ k, i, j).base y = _
congr 3
rw [IsIso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, Category.comp_id]
