coe_dualAnnihilator_span — Mathlib

English

For any set s in M, the dual annihilator of the span of s equals the set of linear functionals vanishing on s; i.e., the dual annihilator of span_R s is the set of f with s ⊆ ker f.

Русский

Для множества s ⊆ M дуальный аннигилятор $\\mathrm{span}_R(s)^{\\mathrm{dualAnnihilator}}$ равен множеству функционалов, которые обнуляются на все элементы s.

LaTeX

$$$ (\\mathrm{span}_R s).dualAnnihilator = \\{ f \\in \\mathrm{Module.Dual} \\, R \\, M \\mid s \\subseteq \\ker f \\} $$$

Lean4

@[simp]
theorem coe_dualAnnihilator_span (s : Set M) :
    ((span R s).dualAnnihilator : Set (Module.Dual R M)) = {f | s ⊆ LinearMap.ker f} :=
  by
  ext f
  simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker]
  exact span_le

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