exists_dual_map_eq_bot_of_notMem — Mathlib

English

If x ∉ p, there exists a dual map f with f(x) ≠ 0 and p.map f = ⊥, under Freeness.

Русский

Если x не лежит в p, найдётся дуальный отображатель f такой, что f(x) ≠ 0 и p.map f = ⊥, при условии свободы.

LaTeX

$$∃ f: Dual R M, f x ≠ 0 ∧ p.map f = ⊥$$

Lean4

theorem exists_dual_map_eq_bot_of_notMem {x : M} (hx : x ∉ p) (hp' : Free R (M ⧸ p)) :
    ∃ f : Dual R M, f x ≠ 0 ∧ p.map f = ⊥ :=
  by
  suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by obtain ⟨f, hf⟩ := this;
    exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩
  rwa [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply, ← forall_dual_apply_eq_zero_iff (K := R),
    not_forall] at hx

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