corootSpan_dualAnnihilator_map_eq

English

The dual annihilator map of the coroot span equals the infimum of the kernels of coroot maps.

Русский

Дуальный аннигилятор корорта спана равен пересечению ядер отображений корорт'

LaTeX

$$$(P.corootSpan R).dualAnnihilator.map P.toPerfPair.symm = \bigwedge_i \ker (P.coroot' i)$$$

Lean4

theorem corootSpan_dualAnnihilator_map_eq :
    (P.corootSpan R).dualAnnihilator.map P.toPerfPair.symm = (span R (range P.coroot')).dualCoannihilator :=
  P.flip.rootSpan_dualAnnihilator_map_eq

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