rootSpan_dualAnnihilator_map_eq_iInf_ker_root'

English

The dual annihilator of the root span, transported along the flip map, is equal to the infimum of the kernels of the root maps.

Русский

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

LaTeX

$$$(P.rootSpan R).dualAnnihilator.map P.flip.toPerfPair.symm = \bigwedge_i \ker (P.root' i)$$$

Lean4

theorem rootSpan_dualAnnihilator_map_eq_iInf_ker_root' :
    (P.rootSpan R).dualAnnihilator.map P.flip.toPerfPair.symm = ⨅ i, LinearMap.ker (P.root' i) :=
  SetLike.coe_injective <| by ext; simp [LinearEquiv.symm_apply_eq, subset_def]

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