feat(linear_algebra/basis): if (p : submodule K V) < ⊤, then there …

…exists `f : V →ₗ[K] K`, `p ≤ ker f` (#6074)

src/analysis/convex/cone.lean

@@ -421,20 +421,17 @@ begin
     replace := nonneg _ this,
     rwa [f.map_sub, sub_nonneg] at this },
   have hy' : y ≠ 0, from λ hy₀, hy (hy₀.symm ▸ zero_mem _),
-  refine ⟨f.sup (linear_pmap.mk_span_singleton y (-c) hy') _, _, _⟩,
-  { refine linear_pmap.sup_h_of_disjoint _ _ (submodule.disjoint_span_singleton.2 _),
-    exact (λ h, (hy h).elim) },
+  refine ⟨f.sup_span_singleton y (-c) hy, _, _⟩,
   { refine lt_iff_le_not_le.2 ⟨f.left_le_sup _ _, λ H, _⟩,
     replace H := linear_pmap.domain_mono.monotone H,
-    rw [linear_pmap.domain_sup, linear_pmap.domain_mk_span_singleton, sup_le_iff,
-      span_le, singleton_subset_iff] at H,
+    rw [linear_pmap.domain_sup_span_singleton, sup_le_iff, span_le, singleton_subset_iff] at H,
     exact hy H.2 },
   { rintros ⟨z, hz⟩ hzs,
     rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩,
     rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩,
     simp only [subtype.coe_mk] at hzs,
-    rw [linear_pmap.sup_apply _ ⟨x, hx⟩ ⟨_, hy'⟩ ⟨_, hz⟩ rfl, linear_pmap.mk_span_singleton_apply,
-      smul_neg, ← sub_eq_add_neg, sub_nonneg],
+    erw [linear_pmap.sup_span_singleton_apply_mk _ _ _ _ _ hx, smul_neg,
+      ← sub_eq_add_neg, sub_nonneg],
     rcases lt_trichotomy r 0 with hr|hr|hr,
     { have : -(r⁻¹ • x) - y ∈ s,
         by rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,

src/linear_algebra/basis.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 -/
 import linear_algebra.linear_independent
 import linear_algebra.projection
+import linear_algebra.linear_pmap
 import data.fintype.card
 
 /-!
@@ -494,8 +495,31 @@ begin
   simp [constr_basis hC, right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) c]
 end
 
+/-- Any linear map `f : p →ₗ[K] V'` defined on a subspace `p` can be extended to the whole
+space. -/
+lemma linear_map.exists_extend {p : submodule K V} (f : p →ₗ[K] V') :
+  ∃ g : V →ₗ[K] V', g.comp p.subtype = f :=
+let ⟨g, hg⟩ := p.subtype.exists_left_inverse_of_injective p.ker_subtype in
+⟨f.comp g, by rw [linear_map.comp_assoc, hg, f.comp_id]⟩
+
 open submodule linear_map
 
+/-- If `p < ⊤` is a subspace of a vector space `V`, then there exists a nonzero linear map
+`f : V →ₗ[K] K` such that `p ≤ ker f`. -/
+lemma submodule.exists_le_ker_of_lt_top (p : submodule K V) (hp : p < ⊤) :
+  ∃ f ≠ (0 : V →ₗ[K] K), p ≤ ker f :=
+begin
+  rcases submodule.exists_of_lt hp with ⟨v, -, hpv⟩, clear hp,
+  rcases (linear_pmap.sup_span_singleton ⟨p, 0⟩ v (1 : K) hpv).to_fun.exists_extend with ⟨f, hf⟩,
+  refine ⟨f, _, _⟩,
+  { rintro rfl, rw [linear_map.zero_comp] at hf,
+    have := linear_pmap.sup_span_singleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv 0 p.zero_mem 1,
+    simpa using (linear_map.congr_fun hf _).trans this },
+  { refine λ x hx, mem_ker.2 _,
+    have := linear_pmap.sup_span_singleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv x hx 0,
+    simpa using (linear_map.congr_fun hf _).trans this }
+end
+
 theorem quotient_prod_linear_equiv (p : submodule K V) :
   nonempty ((p.quotient × p) ≃ₗ[K] V) :=
 let ⟨q, hq⟩ := p.exists_is_compl in nonempty.intro $

src/linear_algebra/linear_pmap.lean

@@ -282,6 +282,32 @@ begin
   simp [*]
 end
 
+section
+
+variables {K : Type*} [division_ring K] [module K E] [module K F]
+
+/-- Extend a `linear_pmap` to `f.domain ⊔ K ∙ x`. -/
+noncomputable def sup_span_singleton (f : linear_pmap K E F) (x : E) (y : F) (hx : x ∉ f.domain) :
+  linear_pmap K E F :=
+f.sup (mk_span_singleton x y (λ h₀, hx $ h₀.symm ▸ f.domain.zero_mem)) $
+  sup_h_of_disjoint _ _ $ by simpa [disjoint_span_singleton]
+
+@[simp] lemma domain_sup_span_singleton (f : linear_pmap K E F) (x : E) (y : F)
+  (hx : x ∉ f.domain) :
+  (f.sup_span_singleton x y hx).domain = f.domain ⊔ K ∙ x := rfl
+
+@[simp] lemma sup_span_singleton_apply_mk (f : linear_pmap K E F) (x : E) (y : F)
+  (hx : x ∉ f.domain) (x' : E) (hx' : x' ∈ f.domain) (c : K) :
+  f.sup_span_singleton x y hx ⟨x' + c • x,
+    mem_sup.2 ⟨x', hx', _, mem_span_singleton.2 ⟨c, rfl⟩, rfl⟩⟩ = f ⟨x', hx'⟩ + c • y :=
+begin
+  erw [sup_apply _ ⟨x', hx'⟩ ⟨c • x, _⟩, mk_span_singleton_apply],
+  refl,
+  exact mem_span_singleton.2 ⟨c, rfl⟩
+end
+
+end
+
 private lemma Sup_aux (c : set (linear_pmap R E F)) (hc : directed_on (≤) c) :
   ∃ f : ↥(Sup (domain '' c)) →ₗ[R] F, (⟨_, f⟩ : linear_pmap R E F) ∈ upper_bounds c :=
 begin