range_dualMap_mkQ_eq — Mathlib

English

The image of the dual map of W.mkQ is exactly the dual annihilator W.dualAnnihilator.

Русский

Образ двойственного отображения W.mkQ равен точному двойственному аннигилятору W.dualAnnihilator.

LaTeX

$$Range(W.mkQ.dualMap) = W.dualAnnihilator$$

Lean4

/-- That $\operatorname{im}(q^* : (V/W)^* \to V^*) = \operatorname{ann}(W)$. -/
theorem range_dualMap_mkQ_eq (W : Submodule R M) : LinearMap.range W.mkQ.dualMap = W.dualAnnihilator :=
  by
  ext φ
  rw [LinearMap.mem_range]
  constructor
  · rintro ⟨ψ, rfl⟩
    have := LinearMap.mem_range_self W.mkQ.dualMap ψ
    simpa only [ker_mkQ] using W.mkQ.range_dualMap_le_dualAnnihilator_ker this
  · intro hφ
    exists W.dualCopairing ⟨φ, hφ⟩

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