t'_iji — Mathlib

English

For i,j, the morphism t' i j i equals the pullback fst followed by D.t i j and the inverse of pullback.snd.

Русский

Для i, j морфизм t' i j i равен pullback.fst после D.t i j и обратного pullback.snd.

LaTeX

$$$D.t' i j i = \\text{pullback.fst} (D.f\\,i\\,j) (D.f\\,i\\,i) \\;\\circ\\; D.t i j \\;\\circ\\; (\\text{pullback.snd} (D.f\\,j\\,i) (D.f\\,j\\,i))^{-1}$$$

Lean4

theorem t'_iji (i j : D.J) : D.t' i j i = pullback.fst _ _ ≫ D.t i j ≫ inv (pullback.snd _ _) :=
  by
  rw [← Category.assoc, ← D.t_fac]
  simp

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