t'_isIso — Mathlib

English

The morphism t' i j k is an isomorphism, with inverse constructed from t' j k i and t' k i j via cocycle data.

Русский

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

LaTeX

$$$\\text{IsIso}(D.t' i j k)$$$

Lean4

instance t'_isIso (i j k : D.J) : IsIso (D.t' i j k) :=
  ⟨⟨D.t' j k i ≫ D.t' k i j, D.cocycle _ _ _, by simpa using D.cocycle _ _ _⟩⟩

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