English
The t' compositions satisfy a compatibility relation with pullback symmetry: D.t' j k i ≫ D.t' k i j equals pullbackSymmetry.hom ≫ D.t' j i k ≫ pullbackSymmetry.hom.
Русский
Сумма композиций t' удовлетворяет совместимости с симметрией pullback: тождество для D.t' j k i и D.t' k i j через pullbackSymmetry.
LaTeX
$$$D.t' j k i \\;\\; D.t' k i j = (\\mathrm{pullbackSymmetry}\\; (D.f j k) (D.f j i)).\\mathrm{hom} \\;\\circ D.t' j i k \\circ (\\mathrm{pullbackSymmetry}\\; (D.f i k) (D.f i j)).\\mathrm{hom}$$$
Lean4
@[reassoc]
theorem t'_comp_eq_pullbackSymmetry (i j k : D.J) :
D.t' j k i ≫ D.t' k i j = (pullbackSymmetry _ _).hom ≫ D.t' j i k ≫ (pullbackSymmetry _ _).hom :=
by
trans inv (D.t' i j k)
· exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)
· rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]
simp [t_fac, t_fac_assoc]
