dualAnnihilator_ker_eq_range_flip

English

For a bilinear map B, the dual annihilator of its kernel equals the range of its flip.

Русский

Для билинейного отображения B дуальный аннигилятор ядра равен образу его разворота (flip).

LaTeX

$$$(\\ker B)^{\\perp} = \\operatorname{range}(B^{\\mathrm{flip}})$$$

Lean4

@[simp]
theorem dualAnnihilator_ker_eq_range_flip [IsReflexive K V₂] : (ker B).dualAnnihilator = range B.flip :=
  by
  change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap)
  rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]

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