truncGE'Map_f_eq_opcyclesMap — Mathlib

English

The f-component of truncGE'Map is given by an iso-composed opcycles map.

Русский

F-компонента truncGE'Map задаётся через изоморфизм и отображение opcyclesMap.

LaTeX

$$$(truncGE'Map \phi e).f i = (K.truncGE'XIsoOpcycles e h hi).hom \circ opcyclesMap \phi i' \circ (L.truncGE'XIsoOpcycles e h hi).inv$$$

Lean4

theorem truncGE'Map_f_eq_opcyclesMap {i : ι} (hi : e.BoundaryGE i) {i' : ι'} (h : e.f i = i') :
    (truncGE'Map φ e).f i =
      (K.truncGE'XIsoOpcycles e h hi).hom ≫ opcyclesMap φ i' ≫ (L.truncGE'XIsoOpcycles e h hi).inv :=
  by
  subst h
  exact dif_pos hi

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