corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'

English

The dual annihilator of the coroot span, transported along toPerfPair, equals the infimum of the kernels of the coroot maps.

Русский

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

LaTeX

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

Lean4

theorem corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot' :
    (P.corootSpan R).dualAnnihilator.map P.toPerfPair.symm = ⨅ i, LinearMap.ker (P.coroot' i) :=
  P.flip.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'

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