t'_snd_fst_snd — Mathlib

English

Again a cocycle-type identity: t'(𝒰) i j k ≫ fst ≫ snd ≫ snd equals fst ≫ fst ≫ snd.

Русский

Ещё одно кокосовое тождество вида: t'(𝒰) i j k ≫ fst ≫ snd ≫ snd = fst ≫ fst ≫ snd.

LaTeX

$$$ t'_{\\mathcal{U}} f g i j k \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_ = \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_$$

Lean4

@[simp, reassoc]
theorem t'_snd_fst_snd (i j k : 𝒰.I₀) :
    t' 𝒰 f g i j k ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ :=
  by
  simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc, pullbackRightPullbackFstIso_inv_fst_assoc,
    pullback.lift_fst_assoc, t_fst_snd, pullbackRightPullbackFstIso_hom_fst_assoc]

Похожие утверждения