English
For U ⊆ (Module.Dual R M) and V ⊆ M, U ≤ V.dualAnnihilator iff V ≤ U.dualCoannihilator.
Русский
Для U ⊆ M^* и V ⊆ M имеет U ≤ V.dualAnnihilator тогда и только тогда, когда V ≤ U.dualCoannihilator.
LaTeX
$$U ≤ V.dualAnnihilator \\iff V ≤ U.dualCoannihilator$$
Lean4
theorem dualAnnihilator_gc :
GaloisConnection (OrderDual.toDual ∘ (dualAnnihilator : Submodule R M → Submodule R (Module.Dual R M)))
(dualCoannihilator ∘ OrderDual.ofDual) :=
by
intro a b
induction b using OrderDual.rec
simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual]
constructor <;>
· intro h x hx
simp only [mem_dualAnnihilator, mem_dualCoannihilator]
intro y hy
have := h hy
simp only [mem_dualAnnihilator, mem_dualCoannihilator] at this
exact this x hx
