English
Let 𝒰 be an open cover of a scheme X, with morphisms f: X → Z and g: Y → Z, and assume pullbacks exist for every index in 𝒰. Then, for all i, j, k ∈ 𝒰.I₀, the coherence morphism t'(𝒰) composed with three successive fst maps equals the snd-projected fst map, i.e. t'(𝒰)_{i j k} ⋅ fst ⋅ fst ⋅ fst = fst ⋅ snd.
Русский
Пусть 𝒰 — открытое покрытие X, есть морфизмы f: X → Z и g: Y → Z, и существуют взятия обратных диаграмм для всех индексов i в 𝒰.I₀. Тогда для любых i, j, k ∈ 𝒰.I₀ кокосовое тождество даёт: t'(𝒰)_{i j k} ⋅ fst ⋅ fst ⋅ fst = fst ⋅ snd.
LaTeX
$$$ t'_{\\mathcal{U}} f g i j k \\;\\gg\\; \\mathrm{pullback.fst} \\_ \\_ \\;\\gg\\; \\mathrm{pullback.fst} \\_ \\_ \\;\\gg\\; \\mathrm{pullback.fst} \\_ \\_ = \\mathrm{pullback.fst} \\_ \\_ \\;\\gg\\; \\mathrm{pullback.snd} \\_ \\_.$$
Lean4
@[simp, reassoc]
theorem t'_fst_fst_fst (i j k : 𝒰.I₀) :
t' 𝒰 f g i j k ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.snd _ _ := by
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackRightPullbackFstIso_inv_snd_fst_assoc,
pullback.lift_fst_assoc, t_fst_fst, pullbackRightPullbackFstIso_hom_fst_assoc]
