English
The composition D.t i j with its reverse D.t j i gives the identity on the gluing object, i.e., t i j then t j i is the identity.
Русский
Состав morfizma t i j и обратного t j i равен тождественному морфизму на склейке.
LaTeX
$$$D.t i j \\circ D.t j i = \\mathrm{Id}$$$
Lean4
@[reassoc, elementwise (attr := simp)]
theorem t_inv (i j : D.J) : D.t i j ≫ D.t j i = 𝟙 _ :=
by
have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd _ _ ≫ inv (pullback.fst _ _) := by simp
have := D.cocycle i j i
rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this
simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this
rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this
simpa using this
