t'_jii — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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