English
For objects i and j in the glue data, the morphism t' i i j equals the homomorphism given by the pullback symmetry on the corresponding f-morphisms.
Русский
Для объектов i и j в данных для сцепления, морфизм t' i i j равен гомоморфизму, задаваемому симметрией тяп-обратно pullback на соответствующих f-морфизмах.
LaTeX
$$$D.t'\\,i\\,i\\,j = (\\text{pullbackSymmetry}\\; (D.f\\;i\\;i)\\; (D.f\\;i\\;j)).\\mathrm{hom}$$$
Lean4
@[simp]
theorem t'_iij (i j : D.J) : D.t' i i j = (pullbackSymmetry _ _).hom :=
by
have eq₁ := D.t_fac i i j
have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
rw [D.t_id, Category.comp_id, eq₂] at eq₁
have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃
exact Mono.right_cancellation _ _ ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)
