feat(linear_algebra/bilinear_form): Bilinear form restricted on a sub…

…space is nondegenerate under some condition (#6855)

The main result is `restrict_nondegenerate_iff_is_compl_orthogonal` which states that: a subspace is complement to its orthogonal complement with respect to some bilinear form if and only if that bilinear form restricted on to the subspace is nondegenerate.

To prove this, I also introduced `dual_annihilator_comap`. This is a definition that allows us to treat the dual annihilator of a dual annihilator as a subspace in the original space.

src/linear_algebra/basic.lean

@@ -1772,7 +1772,9 @@ lemma map_eq_comap {p : submodule R M} : (p.map e : submodule R M₂) = p.comap
 set_like.coe_injective $ by simp [e.image_eq_preimage]
 
 /-- A linear equivalence of two modules restricts to a linear equivalence from any submodule
-of the domain onto the image of the submodule. -/
+`p` of the domain onto the image of that submodule.
+
+This is `linear_equiv.of_submodule'` but with `map` on the right instead of `comap` on the left. -/
 def of_submodule (p : submodule R M) : p ≃ₗ[R] ↥(p.map ↑e : submodule R M₂) :=
 { inv_fun   := λ y, ⟨e.symm y, by {
     rcases y with ⟨y', hy⟩, rw submodule.mem_map at hy, rcases hy with ⟨x, hx, hxy⟩, subst hxy,
@@ -1836,6 +1838,30 @@ def of_submodules (p : submodule R M) (q : submodule R M₂) (h : p.map ↑e = q
 @[simp] lemma of_submodules_symm_apply {p : submodule R M} {q : submodule R M₂}
   (h : p.map ↑e = q) (x : q) : ↑((e.of_submodules p q h).symm x) = e.symm x := rfl
 
+/-- A linear equivalence of two modules restricts to a linear equivalence from the preimage of any
+submodule to that submodule.
+
+This is `linear_equiv.of_submodule` but with `comap` on the left instead of `map` on the right. -/
+def of_submodule' [semimodule R M] [semimodule R M₂] (f : M ≃ₗ[R] M₂) (U : submodule R M₂) :
+  U.comap (f : M →ₗ[R] M₂) ≃ₗ[R] U :=
+(f.symm.of_submodules _ _ f.symm.map_eq_comap).symm
+
+lemma of_submodule'_to_linear_map [semimodule R M] [semimodule R M₂]
+  (f : M ≃ₗ[R] M₂) (U : submodule R M₂) :
+  (f.of_submodule' U).to_linear_map =
+  (f.to_linear_map.dom_restrict _).cod_restrict _ subtype.prop :=
+by { ext, refl }
+
+@[simp]
+lemma of_submodule'_apply [semimodule R M] [semimodule R M₂]
+  (f : M ≃ₗ[R] M₂) (U : submodule R M₂) (x : U.comap (f : M →ₗ[R] M₂)) :
+(f.of_submodule' U x : M₂) = f (x : M) := rfl
+
+@[simp]
+lemma of_submodule'_symm_apply [semimodule R M] [semimodule R M₂]
+  (f : M ≃ₗ[R] M₂) (U : submodule R M₂) (x : U) :
+((f.of_submodule' U).symm x : M) = f.symm (x : M₂) := rfl
+
 variable (p)
 
 /-- The top submodule of `M` is linearly equivalent to `M`. -/
@@ -2111,6 +2137,35 @@ section semimodule
 
 variables [semiring R] [add_comm_monoid M] [semimodule R M]
 
+/-- Given `p` a submodule of the module `M` and `q` a submodule of `p`, `p.equiv_subtype_map q`
+is the natural `linear_equiv` between `q` and `q.map p.subtype`. -/
+def equiv_subtype_map (p : submodule R M) (q : submodule R p) :
+  q ≃ₗ[R] q.map p.subtype :=
+{ inv_fun :=
+    begin
+      rintro ⟨x, hx⟩,
+      refine ⟨⟨x, _⟩, _⟩;
+      rcases hx with ⟨⟨_, h⟩, _, rfl⟩;
+      assumption
+    end,
+  left_inv := λ ⟨⟨_, _⟩, _⟩, rfl,
+  right_inv := λ ⟨x, ⟨_, h⟩, _, rfl⟩, rfl,
+  .. (p.subtype.dom_restrict q).cod_restrict _
+    begin
+      rintro ⟨x, hx⟩,
+      refine ⟨x, hx, rfl⟩,
+    end }
+
+@[simp]
+lemma equiv_subtype_map_apply {p : submodule R M} {q : submodule R p} (x : q) :
+  (p.equiv_subtype_map q x : M) = p.subtype.dom_restrict q x :=
+rfl
+
+@[simp]
+lemma equiv_subtype_map_symm_apply {p : submodule R M} {q : submodule R p} (x : q.map p.subtype) :
+  ((p.equiv_subtype_map q).symm x : M) = x :=
+by { cases x, refl }
+
 /-- If `s ≤ t`, then we can view `s` as a submodule of `t` by taking the comap
 of `t.subtype`. -/
 def comap_subtype_equiv_of_le {p q : submodule R M} (hpq : p ≤ q) :

src/linear_algebra/bilinear_form.lean

@@ -1319,10 +1319,107 @@ begin
     ext, exact hm x }
 end
 
+/-- The restriction of a nondegenerate bilinear form `B` onto a submodule `W` is
+nondegenerate if `disjoint W (B.orthogonal W)`. -/
+lemma nondegenerate_restrict_of_disjoint_orthogonal
+  (B : bilin_form R₁ M₁) (hB : sym_bilin_form.is_sym B)
+  {W : submodule R₁ M₁} (hW : disjoint W (B.orthogonal W)) :
+  (B.restrict W).nondegenerate :=
+begin
+  rintro ⟨x, hx⟩ hB₁,
+  rw [submodule.mk_eq_zero, ← submodule.mem_bot R₁],
+  refine hW ⟨hx, λ y hy, _⟩,
+  specialize hB₁ ⟨y, hy⟩,
+  rwa [restrict_apply, submodule.coe_mk, submodule.coe_mk, hB] at hB₁
+end
+
 section
 
+lemma to_lin_restrict_ker_eq_inf_orthogonal
+  (B : bilin_form K V) (W : subspace K V) (hB : sym_bilin_form.is_sym B) :
+  (B.to_lin.dom_restrict W).ker.map W.subtype = (W ⊓ B.orthogonal ⊤ : subspace K V) :=
+begin
+  ext x, split; intro hx,
+  { rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩,
+    erw linear_map.mem_ker at hker,
+    split,
+    { simp [hx] },
+    { intros y _,
+      rw [is_ortho, hB],
+      change (B.to_lin.dom_restrict W) ⟨x, hx⟩ y = 0,
+      rw hker, refl } },
+  { simp_rw [submodule.mem_map, linear_map.mem_ker],
+    refine ⟨⟨x, hx.1⟩, _, rfl⟩,
+    ext y, change B x y = 0,
+    rw hB,
+    exact hx.2 _ submodule.mem_top }
+end
+
+lemma to_lin_restrict_range_dual_annihilator_comap_eq_orthogonal
+  (B : bilin_form K V) (W : subspace K V) :
+  (B.to_lin.dom_restrict W).range.dual_annihilator_comap = B.orthogonal W :=
+begin
+  ext x, split; rw [mem_orthogonal_iff]; intro hx,
+  { intros y hy,
+    rw submodule.mem_dual_annihilator_comap_iff at hx,
+    refine hx (B.to_lin.dom_restrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, _, rfl⟩,
+    simp only [submodule.top_coe] },
+  { rw submodule.mem_dual_annihilator_comap_iff,
+    rintro _ ⟨⟨w, hw⟩, _, rfl⟩,
+    exact hx w hw }
+end
+
 variable [finite_dimensional K V]
 
+open finite_dimensional
+
+lemma findim_add_findim_orthogonal
+  {B : bilin_form K V} {W : subspace K V} (hB₁ : sym_bilin_form.is_sym B) :
+  findim K W + findim K (B.orthogonal W) =
+  findim K V + findim K (W ⊓ B.orthogonal ⊤ : subspace K V) :=
+begin
+  rw [← to_lin_restrict_ker_eq_inf_orthogonal _ _ hB₁,
+      ← to_lin_restrict_range_dual_annihilator_comap_eq_orthogonal _ _,
+      findim_map_subtype_eq],
+  conv_rhs { rw [← @subspace.findim_add_findim_dual_annihilator_comap_eq K V _ _ _ _
+                  (B.to_lin.dom_restrict W).range,
+                 add_comm, ← add_assoc, add_comm (findim K ↥((B.to_lin.dom_restrict W).ker)),
+                 linear_map.findim_range_add_findim_ker] },
+end
+
+/-- A subspace is complement to its orthogonal complement with respect to some
+bilinear form if that bilinear form restricted on to the subspace is nondegenerate. -/
+lemma restrict_nondegenerate_of_is_compl_orthogonal
+  {B : bilin_form K V} {W : subspace K V}
+  (hB₁ : sym_bilin_form.is_sym B) (hB₂ : (B.restrict W).nondegenerate) :
+  is_compl W (B.orthogonal W) :=
+begin
+  have : W ⊓ B.orthogonal W = ⊥,
+  { rw eq_bot_iff,
+    intros x hx,
+    obtain ⟨hx₁, hx₂⟩ := submodule.mem_inf.1 hx,
+    refine subtype.mk_eq_mk.1 (hB₂ ⟨x, hx₁⟩ _),
+    rintro ⟨n, hn⟩,
+    rw [restrict_apply, submodule.coe_mk, submodule.coe_mk, hB₁],
+    exact hx₂ n hn },
+  refine ⟨this ▸ le_refl _, _⟩,
+  { rw top_le_iff,
+    refine eq_top_of_findim_eq _,
+    refine le_antisymm (submodule.findim_le _) _,
+    conv_rhs { rw ← add_zero (findim K _) },
+    rw [← findim_bot K V, ← this, submodule.dim_sup_add_dim_inf_eq,
+        findim_add_findim_orthogonal hB₁],
+    exact nat.le.intro rfl }
+end
+
+/-- A subspace is complement to its orthogonal complement with respect to some bilinear form
+if and only if that bilinear form restricted on to the subspace is nondegenerate. -/
+theorem restrict_nondegenerate_iff_is_compl_orthogonal
+  {B : bilin_form K V} {W : subspace K V} (hB₁ : sym_bilin_form.is_sym B) :
+  (B.restrict W).nondegenerate ↔ is_compl W (B.orthogonal W) :=
+⟨λ hB₂, restrict_nondegenerate_of_is_compl_orthogonal hB₁ hB₂,
+ λ h, B.nondegenerate_restrict_of_disjoint_orthogonal hB₁ h.1⟩
+
 /-- Given a nondegenerate bilinear form `B` on a finite-dimensional vector space, `B.to_dual` is
 the linear equivalence between a vector space and its dual with the underlying linear map
 `B.to_lin`. -/
@@ -1336,6 +1433,11 @@ lemma to_dual_def {B : bilin_form K V} (hB : B.nondegenerate) {m n : V} :
 
 end
 
+/-! We note that we cannot use `bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal` for the
+lemma below since the below lemma does not require `V` to be finite dimensional. However,
+`bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal` does not require `B` to be nondegenerate
+on the whole space. -/
+
 /-- The restriction of a symmetric, non-degenerate bilinear form on the orthogonal complement of
 the span of a singleton is also non-degenerate. -/
 lemma restrict_orthogonal_span_singleton_nondegenerate (B : bilin_form K V)

src/linear_algebra/dual.lean

@@ -296,6 +296,9 @@ end
 def eval_equiv [finite_dimensional K V] : V ≃ₗ[K] dual K (dual K V) :=
 linear_equiv.of_bijective (eval K V) eval_ker (erange_coe)
 
+lemma eval_equiv_to_linear_map [finite_dimensional K V] :
+  eval_equiv.to_linear_map = dual.eval K V := rfl
+
 end vector_space
 
 section dual_pair
@@ -458,6 +461,14 @@ 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 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]
+
 end submodule
 
 namespace subspace
@@ -573,6 +584,24 @@ begin
     exact is_basis.to_dual_equiv _ hB.1 },
 end
 
+open finite_dimensional
+
+@[simp]
+lemma findim_dual_annihilator_comap_eq {Φ : subspace K (module.dual K V)} :
+  findim K Φ.dual_annihilator_comap = findim K Φ.dual_annihilator :=
+begin
+  rw [submodule.dual_annihilator_comap, ← vector_space.eval_equiv_to_linear_map],
+  exact linear_equiv.findim_eq (linear_equiv.of_submodule' _ _),
+end
+
+lemma findim_add_findim_dual_annihilator_comap_eq
+  (W : subspace K (module.dual K V)) :
+  findim K W + findim K W.dual_annihilator_comap = findim K V :=
+begin
+  rw [findim_dual_annihilator_comap_eq, W.quot_equiv_annihilator.findim_eq.symm, add_comm,
+      submodule.findim_quotient_add_findim, subspace.dual_findim_eq],
+end
+
 end
 
 end subspace

src/linear_algebra/finite_dimensional.lean

@@ -752,6 +752,11 @@ begin
       ← linear_equiv.findim_eq f, add_comm, submodule.findim_quotient_add_findim]
 end
 
+@[simp]
+lemma findim_map_subtype_eq (p : subspace K V) (q : subspace K p) :
+  finite_dimensional.findim K (q.map p.subtype) = finite_dimensional.findim K q :=
+(submodule.equiv_subtype_map p q).symm.findim_eq
+
 end finite_dimensional
 
 namespace linear_map