English
The dual annihilator and dual coannihilator form a Galois coinsertion between the posets of subspaces, up to the relevant duality.
Русский
Дуальный аннигилятор и дуальный коаннигилятор образуют Galois-coinsertion между соответствующими частично упорядоченными множествами подпространств (с учётом двойной дуальности).
LaTeX
$$$\text{dualAnnihilator},\ \text{dualCoannihilator}\ ext{form a Galois coinsertion between the appropriate ordered structures.}$$$
Lean4
/-- `Submodule.dualAnnihilator` and `Submodule.dualCoannihilator` form a Galois coinsertion. -/
def dualAnnihilatorGci (K V : Type*) [Field K] [AddCommGroup V] [Module K V] :
GaloisCoinsertion (OrderDual.toDual ∘ (dualAnnihilator : Subspace K V → Subspace K (Module.Dual K V)))
(dualCoannihilator ∘ OrderDual.ofDual)
where
choice W _ := dualCoannihilator W
gc := dualAnnihilator_gc K V
u_l_le _ := dualAnnihilator_dualCoannihilator_eq.le
choice_eq _ _ := rfl
