t'_inv — Mathlib

English

The morphism t' i j i is the inverse-like component in a cocycle relation for glue data, expressed using pullback symmetry and t' i j k.

Русский

Морфизм t' i j i является частью кокцик-отношения для данных сцепления, выраженным через симметрию pullback и t' i j k.

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'_inv (i j k : D.J) :
    D.t' i j k ≫ (pullbackSymmetry _ _).hom ≫ D.t' j i k ≫ (pullbackSymmetry _ _).hom = 𝟙 _ :=
  by
  rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]
  simp [t_fac, t_fac_assoc]

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