English
There exists an equality witnessing the commutativity of a square formed by invApp and t_app in the gluing data; i.e., a witness eq such that a composed path equals another path in the diagram.
Русский
Существет свидетельство равенства, фиксирующее равносильность квадратов в данных склейки; существует eq, чтобы композиции путей совпадали.
LaTeX
$$$\\exists eq:\\; (π_2^{-1} i,j,k)U \\;\\text{and related arrows commute with } D.t_k i \\text{ and } D.t'\\,k i j$$$
Lean4
/-- The red and the blue arrows in  commute. -/
@[simp, reassoc]
theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
(D.f_open i j).invApp _ U ≫ (D.f i k).c.app _ =
(π₁ i, j, k).c.app (op U) ≫
(π₂⁻¹ i, j, k) (unop _) ≫
(D.V _).presheaf.map
(eqToHom
(by
delta IsOpenImmersion.opensFunctor
dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]
congr
apply pullback_base)) :=
by
have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)
dsimp only [comp_c_app] at this
rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc, IsOpenImmersion.inv_invApp]
simp_rw [Category.assoc]
erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ← (D.V (i, k)).presheaf.map_comp, ←
(D.V (i, k)).presheaf.map_comp]
convert (Category.comp_id _).symm
erw [(D.V (i, k)).presheaf.map_id]
rfl