exists_dual_map_eq_bot_of_lt_top — Mathlib

English

If p < ⊤ and hp' Free, there exists a dual map with p.map f = ⊥ and f ≠ 0.

Русский

Если p < ⊤ и hp' свободность, существует дуальное отображение f с p.map f = 0 и f ≠ 0.

LaTeX

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

Lean4

theorem exists_dual_map_eq_bot_of_lt_top (hp : p < ⊤) (hp' : Free R (M ⧸ p)) : ∃ f : Dual R M, f ≠ 0 ∧ p.map f = ⊥ :=
  by
  obtain ⟨x, hx⟩ : ∃ x : M, x ∉ p := by rw [lt_top_iff_ne_top] at hp; contrapose! hp; ext; simp [hp]
  obtain ⟨f, hf, hf'⟩ := p.exists_dual_map_eq_bot_of_notMem hx hp'
  exact ⟨f, by aesop, hf'⟩

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