cyclesMk₂_eq — Mathlib

English

A canonical equality for cyclesMk at levels 2 and 1 with the inverse of chainsIso₂.

Русский

Каноническое равенство cyclesMk на уровнях 2 и 1 с обратным от chainsIso₂.

LaTeX

$$$ cyclesMk\ 2 1 (by\ simp) ((chainsIso_2 A).inv x) (by\ simp) = (isoCycles_2 A).inv x$$

Lean4

theorem cyclesMk₂_eq (x : cycles₂ A) : cyclesMk 2 1 (by simp) ((chainsIso₂ A).inv x) (by simp) = (isoCycles₂ A).inv x :=
  (ModuleCat.mono_iff_injective <| iCycles A 2).1 inferInstance <|
    by
    rw [iCycles_mk]
    simp only [ChainComplex.of_x, isoCycles₂_inv_comp_iCycles_apply]
    rfl

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