feat(linear_algebra/dual): more about dual_annihilator (#17313)

Also gives `dual_annihilator_sup_eq_inf_dual_annihilator` a shorter name.

src/linear_algebra/bilinear_form.lean

@@ -1097,9 +1097,9 @@ lemma to_lin_restrict_range_dual_annihilator_comap_eq_orthogonal
 begin
   ext x, split; rw [mem_orthogonal_iff]; intro hx,
   { intros y hy,
-    rw submodule.mem_dual_annihilator_comap_iff at hx,
+    rw submodule.mem_dual_annihilator_comap at hx,
     refine hx (B.to_lin.dom_restrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩ },
-  { rw submodule.mem_dual_annihilator_comap_iff,
+  { rw submodule.mem_dual_annihilator_comap,
     rintro _ ⟨⟨w, hw⟩, rfl⟩,
     exact hx w hw }
 end

src/linear_algebra/dual.lean

@@ -317,6 +317,20 @@ open module module.dual submodule linear_map cardinal basis finite_dimensional
 theorem eval_ker : (eval K V).ker = ⊥ :=
 by { classical, exact (basis.of_vector_space K V).eval_ker }
 
+section
+variable (K)
+
+theorem eval_apply_eq_zero_iff (v : V) : (eval K V) v = 0 ↔ v = 0 :=
+by simpa only using set_like.ext_iff.mp (eval_ker : (eval K V).ker = _) v
+
+theorem eval_apply_injective : function.injective (eval K V) :=
+(injective_iff_map_eq_zero' (eval K V)).mpr (eval_apply_eq_zero_iff K)
+
+theorem forall_dual_apply_eq_zero_iff (v : V) : (∀ (φ : module.dual K V), φ v = 0) ↔ v = 0 :=
+by { rw [← eval_apply_eq_zero_iff K v, linear_map.ext_iff], refl }
+
+end
+
 -- TODO(jmc): generalize to rings, once `module.rank` is generalized
 theorem dual_dim_eq [finite_dimensional K V] :
   cardinal.lift (module.rank K V) = module.rank K (dual K V) :=
@@ -478,7 +492,73 @@ lemma dual_restrict_ker_eq_dual_annihilator (W : submodule R M) :
   W.dual_restrict.ker = W.dual_annihilator :=
 rfl
 
-lemma dual_annihilator_sup_eq_inf_dual_annihilator (U V : submodule R M) :
+/-- The `dual_annihilator` of a submodule of the dual space pulled back along the evaluation map
+`module.dual.eval`. -/
+def dual_annihilator_comap (Φ : submodule R (module.dual R M)) : submodule R M :=
+Φ.dual_annihilator.comap (module.dual.eval R M)
+
+lemma mem_dual_annihilator_comap {Φ : submodule R (module.dual R M)} (x : M) :
+  x ∈ Φ.dual_annihilator_comap ↔ ∀ φ ∈ Φ, (φ x : R) = 0 :=
+by simp_rw [dual_annihilator_comap, mem_comap, mem_dual_annihilator, module.dual.eval_apply]
+
+@[simp] lemma dual_annihilator_top : (⊤ : submodule R M).dual_annihilator = ⊥ :=
+begin
+  rw eq_bot_iff,
+  intro v,
+  simp_rw [mem_dual_annihilator, mem_bot, mem_top, forall_true_left],
+  exact λ h, linear_map.ext h,
+end
+
+@[simp] lemma dual_annihilator_bot : (⊥ : submodule R M).dual_annihilator = ⊤ :=
+begin
+  rw eq_top_iff,
+  intro v,
+  simp_rw [mem_dual_annihilator, mem_bot, mem_top, forall_true_left],
+  rintro _ rfl,
+  exact _root_.map_zero v,
+end
+
+@[simp] lemma dual_annihilator_comap_bot :
+  (⊥ : submodule R (module.dual R M)).dual_annihilator_comap = ⊤ :=
+by rw [dual_annihilator_comap, dual_annihilator_bot, comap_top]
+
+@[mono] lemma dual_annihilator_anti {U V : submodule R M} (hUV : U ≤ V) :
+  V.dual_annihilator ≤ U.dual_annihilator :=
+begin
+  intro φ,
+  simp_rw [mem_dual_annihilator],
+  intros h w hw,
+  exact h w (hUV hw),
+end
+
+@[mono] lemma dual_annihilator_comap_anti {U V : submodule R (module.dual R M)} (hUV : U ≤ V) :
+  V.dual_annihilator_comap ≤ U.dual_annihilator_comap :=
+begin
+  intro φ,
+  simp_rw [mem_dual_annihilator_comap],
+  intros h w hw,
+  exact h w (hUV hw),
+end
+
+lemma le_dual_annihilator_dual_annihilator_comap {U : submodule R M} :
+  U ≤ U.dual_annihilator.dual_annihilator_comap :=
+begin
+  intro v,
+  simp_rw [mem_dual_annihilator_comap, mem_dual_annihilator],
+  intros hv φ h,
+  exact h _ hv,
+end
+
+lemma le_dual_annihilator_comap_dual_annihilator {U : submodule R (module.dual R M)} :
+  U ≤ U.dual_annihilator_comap.dual_annihilator :=
+begin
+  intro v,
+  simp_rw [mem_dual_annihilator, mem_dual_annihilator_comap],
+  intros hv φ h,
+  exact h _ hv,
+end
+
+lemma dual_annihilator_sup_eq (U V : submodule R M) :
   (U ⊔ V).dual_annihilator = U.dual_annihilator ⊓ V.dual_annihilator :=
 begin
   ext φ,
@@ -493,13 +573,52 @@ begin
     rw [linear_map.map_add, h.1 _ hx, h.2 _ hy, add_zero] }
 end
 
-/-- The pullback of a submodule in the dual space along the evaluation map. -/
-def dual_annihilator_comap (Φ : submodule R (module.dual R M)) : submodule R M :=
-Φ.dual_annihilator.comap (module.dual.eval R M)
+lemma dual_annihilator_supr_eq {ι : Type*} (U : ι → submodule R M) :
+  (⨆ (i : ι), U i).dual_annihilator = ⨅ (i : ι), (U i).dual_annihilator :=
+begin
+  classical,
+  ext φ,
+  simp_rw [mem_infi, mem_dual_annihilator],
+  split,
+  { simp_rw [mem_supr],
+    intros h i w hw,
+    exact h _ (λ _ hi, hi i hw), },
+  { simp_rw [submodule.mem_supr_iff_exists_dfinsupp'],
+    rintros h w ⟨f, rfl⟩,
+    simp only [linear_map.map_dfinsupp_sum],
+    transitivity f.sum (λ (i : ι) (d : U i), (0 : R)),
+    { congr,
+      ext i d,
+      exact h i d d.property, },
+    { exact @dfinsupp.sum_zero ι _ (λ i, U i) _ _ _ _ f, } }
+end
 
-lemma mem_dual_annihilator_comap_iff {Φ : submodule R (module.dual R M)} (x : M) :
-  x ∈ Φ.dual_annihilator_comap ↔ ∀ φ ∈ Φ, (φ x : R) = 0 :=
-by simp_rw [dual_annihilator_comap, mem_comap, mem_dual_annihilator, module.dual.eval_apply]
+-- TODO: when `M` is finite-dimensional this is an equality
+lemma sup_dual_annihilator_le_inf (U V : submodule R M) :
+  U.dual_annihilator ⊔ V.dual_annihilator ≤ (U ⊓ V).dual_annihilator :=
+begin
+  intro φ,
+  simp_rw [mem_sup, mem_dual_annihilator, mem_inf],
+  rintro ⟨ψ, hψ, ψ', hψ', rfl⟩ v ⟨hU, hV⟩,
+  rw [linear_map.add_apply, hψ _ hU, hψ' _ hV, zero_add],
+end
+
+-- TODO: when `M` is finite-dimensional this is an equality
+lemma supr_dual_annihilator_le_infi {ι : Type*} (U : ι → submodule R M) :
+  (⨆ (i : ι), (U i).dual_annihilator) ≤ (⨅ (i : ι), U i).dual_annihilator :=
+begin
+  classical,
+  intro φ,
+  simp_rw [mem_dual_annihilator, submodule.mem_supr_iff_exists_dfinsupp', mem_infi],
+  rintros ⟨f, rfl⟩ x hx,
+  rw [linear_map.dfinsupp_sum_apply],
+  transitivity f.sum (λ (i : ι) (d : (U i).dual_annihilator), (0 : R)),
+  { congr,
+    ext i ⟨d, hd⟩,
+    rw [mem_dual_annihilator] at hd,
+    exact hd x (hx _), },
+  { exact @dfinsupp.sum_zero ι _ (λ i, (U i).dual_annihilator) _ _ _ _ f }
+end
 
 end submodule
 
@@ -512,6 +631,33 @@ universes u v w
 -- We work in vector spaces because `exists_is_compl` only hold for vector spaces
 variables {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V]
 
+@[simp] lemma dual_annihilator_comap_top (W : subspace K V) :
+  (⊤ : submodule K (module.dual K W)).dual_annihilator_comap = ⊥ :=
+by rw [dual_annihilator_comap, dual_annihilator_top, comap_bot, module.eval_ker]
+
+lemma dual_annihilator_dual_annihilator_comap_eq {W : subspace K V} :
+  W.dual_annihilator.dual_annihilator_comap = W :=
+begin
+  refine le_antisymm _ le_dual_annihilator_dual_annihilator_comap,
+  intro v,
+  simp only [mem_dual_annihilator, mem_dual_annihilator_comap],
+  contrapose!,
+  intro hv,
+  obtain ⟨W', hW⟩ := submodule.exists_is_compl W,
+  obtain ⟨⟨w, w'⟩, rfl, -⟩ := exists_unique_add_of_is_compl_prod hW v,
+  have hw'n : (w' : V) ∉ W := by { contrapose! hv, exact submodule.add_mem W w.2 hv },
+  have hw'nz : w' ≠ 0 := by { rintro rfl, exact hw'n (submodule.zero_mem W) },
+  rw [ne.def, ← module.forall_dual_apply_eq_zero_iff K w'] at hw'nz,
+  push_neg at hw'nz,
+  obtain ⟨φ, hφ⟩ := hw'nz,
+  existsi ((linear_map.of_is_compl_prod hW).comp (linear_map.inr _ _ _)) φ,
+  simp only [coe_comp, coe_inr, function.comp_app, of_is_compl_prod_apply, map_add,
+    of_is_compl_left_apply, zero_apply, of_is_compl_right_apply, zero_add, ne.def],
+  refine ⟨_, hφ⟩,
+  intros v hv,
+  convert linear_map.of_is_compl_left_apply hW ⟨v, hv⟩,
+end
+
 /-- Given a subspace `W` of `V` and an element of its dual `φ`, `dual_lift W φ` is
 the natural extension of `φ` to an element of the dual of `V`.
 That is, `dual_lift W φ` sends `w ∈ W` to `φ x` and `x` in the complement of `W` to `0`. -/