refactor(linear_algebra/bilinear_form): Change namespace of is_refl, …

…is_symm, and is_alt (#10338)

The propositions `is_refl`, `is_symm`, and `is_alt` are now in the
namespace `bilin_form`. Moreover, `is_sym` is now renamed to `is_symm`.

docs/overview.yaml

@@ -172,8 +172,8 @@ Linear algebra:
     existence of an eigenvalue: 'module.End.exists_eigenvalue'
   Bilinear and quadratic forms:
     bilinear form: 'bilin_form'
-    alternating bilinear form: 'alt_bilin_form.is_alt'
-    symmetric bilinear form: 'sym_bilin_form.is_sym'
+    alternating bilinear form: 'bilin_form.is_alt'
+    symmetric bilinear form: 'bilin_form.is_symm'
     matrix representation: 'bilin_form.to_matrix'
     quadratic form: 'quadratic_form'
     polar form of a quadratic: 'quadratic_form.polar'

docs/undergrad.yaml

@@ -194,8 +194,8 @@ Ring Theory:
 Bilinear and Quadratic Forms Over a Vector Space:
   Bilinear forms:
     bilinear forms: 'bilin_form'
-    alternating bilinear forms: 'alt_bilin_form.is_alt'
-    symmetric bilinear forms: 'sym_bilin_form.is_sym'
+    alternating bilinear forms: 'bilin_form.is_alt'
+    symmetric bilinear forms: 'bilin_form.is_symm'
     nondegenerate forms: 'bilin_form.nondegenerate'
     matrix representation: 'bilin_form.to_matrix'
     change of coordinates: 'bilin_form.to_matrix_comp'

src/linear_algebra/bilinear_form.lean

@@ -948,39 +948,39 @@ end to_matrix
 
 end matrix
 
-namespace refl_bilin_form
-
-open refl_bilin_form bilin_form
+namespace bilin_form
 
 /-- The proposition that a bilinear form is reflexive -/
 def is_refl (B : bilin_form R M) : Prop := ∀ (x y : M), B x y = 0 → B y x = 0
 
-variable (H : is_refl B)
+namespace is_refl
+
+variable (H : B.is_refl)
 
 lemma eq_zero : ∀ {x y : M}, B x y = 0 → B y x = 0 := λ x y, H x y
 
-lemma ortho_sym {x y : M} :
+lemma ortho_comm {x y : M} :
   is_ortho B x y ↔ is_ortho B y x := ⟨eq_zero H, eq_zero H⟩
 
-end refl_bilin_form
+end is_refl
 
-namespace sym_bilin_form
+/-- The proposition that a bilinear form is symmetric -/
+def is_symm (B : bilin_form R M) : Prop := ∀ (x y : M), B x y = B y x
 
-open sym_bilin_form bilin_form
+namespace is_symm
 
-/-- The proposition that a bilinear form is symmetric -/
-def is_sym (B : bilin_form R M) : Prop := ∀ (x y : M), B x y = B y x
+variable (H : B.is_symm)
 
-variable (H : is_sym B)
+protected lemma eq (x y : M) : B x y = B y x := H x y
 
-lemma sym (x y : M) : B x y = B y x := H x y
+lemma is_refl : B.is_refl := λ x y H1, H x y ▸ H1
 
-lemma is_refl : refl_bilin_form.is_refl B := λ x y H1, H x y ▸ H1
+lemma ortho_comm {x y : M} :
+  is_ortho B x y ↔ is_ortho B y x := H.is_refl.ortho_comm
 
-lemma ortho_sym {x y : M} :
-  is_ortho B x y ↔ is_ortho B y x := refl_bilin_form.ortho_sym (is_refl H)
+end is_symm
 
-lemma is_sym_iff_flip' [algebra R₂ R] : is_sym B ↔ flip_hom R₂ B = B :=
+lemma is_symm_iff_flip' [algebra R₂ R] : B.is_symm ↔ flip_hom R₂ B = B :=
 begin
   split,
   { intros h,
@@ -991,21 +991,14 @@ begin
     simp }
 end
 
-end sym_bilin_form
-
-namespace alt_bilin_form
-
-open alt_bilin_form bilin_form
-
 /-- The proposition that a bilinear form is alternating -/
 def is_alt (B : bilin_form R M) : Prop := ∀ (x : M), B x x = 0
 
-variable (H : is_alt B)
-include H
+namespace is_alt
 
-lemma self_eq_zero (x : M) : B x x = 0 := H x
+lemma self_eq_zero (H : B.is_alt) (x : M) : B x x = 0 := H x
 
-lemma neg (H : is_alt B₁) (x y : M₁) :
+lemma neg (H : B₁.is_alt) (x y : M₁) :
   - B₁ x y = B₁ y x :=
 begin
   have H1 : B₁ (x + y) (x + y) = 0,
@@ -1016,18 +1009,16 @@ begin
   exact H1,
 end
 
-lemma is_refl (H : is_alt B₁) : refl_bilin_form.is_refl B₁ :=
+lemma is_refl (H : B₁.is_alt) : B₁.is_refl :=
 begin
   intros x y h,
   rw [←neg H, h, neg_zero],
 end
 
-lemma ortho_sym (H : is_alt B₁) {x y : M₁} :
-  is_ortho B₁ x y ↔ is_ortho B₁ y x := refl_bilin_form.ortho_sym (is_refl H)
+lemma ortho_comm (H : B₁.is_alt) {x y : M₁} :
+  is_ortho B₁ x y ↔ is_ortho B₁ y x := H.is_refl.ortho_comm
 
-end alt_bilin_form
-
-namespace bilin_form
+end is_alt
 
 section linear_adjoints
 
@@ -1304,7 +1295,7 @@ variables {N L : submodule R M}
 lemma orthogonal_le (h : N ≤ L) : B.orthogonal L ≤ B.orthogonal N :=
 λ _ hn l hl, hn l (h hl)
 
-lemma le_orthogonal_orthogonal (b : refl_bilin_form.is_refl B) :
+lemma le_orthogonal_orthogonal (b : B.is_refl) :
   N ≤ B.orthogonal (B.orthogonal N) :=
 λ n hn m hm, b _ _ (hm n hn)
 
@@ -1366,8 +1357,8 @@ def restrict (B : bilin_form R M) (W : submodule R M) : bilin_form R W :=
   bilin_smul_right := λ _ _ _, smul_right _ _ _}
 
 /-- The restriction of a symmetric bilinear form on a submodule is also symmetric. -/
-lemma restrict_sym (B : bilin_form R M) (b : sym_bilin_form.is_sym B)
-  (W : submodule R M) : sym_bilin_form.is_sym $ B.restrict W :=
+lemma restrict_symm (B : bilin_form R M) (b : B.is_symm)
+  (W : submodule R M) : (B.restrict W).is_symm :=
 λ x y, b x y
 
 /-- A nondegenerate bilinear form is a bilinear form such that the only element that is orthogonal
@@ -1409,7 +1400,7 @@ lemma nondegenerate.ker_eq_bot {B : bilin_form R₂ M₂} (h : B.nondegenerate)
 /-- 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₁) (b : sym_bilin_form.is_sym B)
+  (B : bilin_form R₁ M₁) (b : B.is_symm)
   {W : submodule R₁ M₁} (hW : disjoint W (B.orthogonal W)) :
   (B.restrict W).nondegenerate :=
 begin
@@ -1462,7 +1453,7 @@ end
 section
 
 lemma to_lin_restrict_ker_eq_inf_orthogonal
-  (B : bilin_form K V) (W : subspace K V) (b : sym_bilin_form.is_sym B) :
+  (B : bilin_form K V) (W : subspace K V) (b : B.is_symm) :
   (B.to_lin.dom_restrict W).ker.map W.subtype = (W ⊓ B.orthogonal ⊤ : subspace K V) :=
 begin
   ext x, split; intro hx,
@@ -1499,7 +1490,7 @@ variable [finite_dimensional K V]
 open finite_dimensional
 
 lemma finrank_add_finrank_orthogonal
-  {B : bilin_form K V} {W : subspace K V} (b₁ : sym_bilin_form.is_sym B) :
+  {B : bilin_form K V} {W : subspace K V} (b₁ : B.is_symm) :
   finrank K W + finrank K (B.orthogonal W) =
   finrank K V + finrank K (W ⊓ B.orthogonal ⊤ : subspace K V) :=
 begin
@@ -1516,7 +1507,7 @@ end
 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}
-  (b₁ : sym_bilin_form.is_sym B) (b₂ : (B.restrict W).nondegenerate) :
+  (b₁ : B.is_symm) (b₂ : (B.restrict W).nondegenerate) :
   is_compl W (B.orthogonal W) :=
 begin
   have : W ⊓ B.orthogonal W = ⊥,
@@ -1540,7 +1531,7 @@ 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} (b₁ : sym_bilin_form.is_sym B) :
+  {B : bilin_form K V} {W : subspace K V} (b₁ : B.is_symm) :
   (B.restrict W).nondegenerate ↔ is_compl W (B.orthogonal W) :=
 ⟨λ b₂, restrict_nondegenerate_of_is_compl_orthogonal b₁ b₂,
  λ h, B.nondegenerate_restrict_of_disjoint_orthogonal b₁ h.1⟩
@@ -1579,7 +1570,7 @@ by rw [dual_basis, basis.map_apply, basis.coe_dual_basis, ← to_dual_def hB,
        finsupp.single_apply]
 
 lemma apply_dual_basis_right (B : bilin_form K V) (hB : B.nondegenerate)
-  (sym : sym_bilin_form.is_sym B) (b : basis ι K V)
+  (sym : B.is_symm) (b : basis ι K V)
   (i j) : B (b i) (B.dual_basis hB b j) = if i = j then 1 else 0 :=
 by rw [sym, apply_dual_basis_left]
 
@@ -1595,7 +1586,7 @@ 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)
-  (b₁ : nondegenerate B) (b₂ : sym_bilin_form.is_sym B) {x : V} (hx : ¬ B.is_ortho x x) :
+  (b₁ : B.nondegenerate) (b₂ : B.is_symm) {x : V} (hx : ¬ B.is_ortho x x) :
   nondegenerate $ B.restrict $ B.orthogonal (K ∙ x) :=
 begin
   refine λ m hm, submodule.coe_eq_zero.1 (b₁ m.1 (λ n, _)),

src/linear_algebra/quadratic_form/basic.lean

@@ -462,7 +462,7 @@ end
 end bilin_form
 
 namespace quadratic_form
-open bilin_form sym_bilin_form
+open bilin_form
 
 section associated_hom
 variables (S) [comm_semiring S] [algebra S R]
@@ -498,7 +498,7 @@ variables (Q : quadratic_form R M) (S)
 @[simp] lemma associated_apply (x y : M) :
   associated_hom S Q x y = ⅟2 * (Q (x + y) - Q x - Q y) := rfl
 
-lemma associated_is_sym : is_sym (associated_hom S Q) :=
+lemma associated_is_symm : (associated_hom S Q).is_symm :=
 λ x y, by simp only [associated_apply, add_comm, add_left_comm, sub_eq_add_neg]
 
 @[simp] lemma associated_comp {N : Type v} [add_comm_group N] [module R N] (f : N →ₗ[R] M) :
@@ -510,10 +510,11 @@ lemma associated_to_quadratic_form (B : bilin_form R M) (x y : M) :
   associated_hom S B.to_quadratic_form x y = ⅟2 * (B x y + B y x) :=
 by simp only [associated_apply, ← polar_to_quadratic_form, polar, to_quadratic_form_apply]
 
-lemma associated_left_inverse (h : is_sym B₁) :
+lemma associated_left_inverse (h : B₁.is_symm) :
   associated_hom S (B₁.to_quadratic_form) = B₁ :=
 bilin_form.ext $ λ x y,
-by rw [associated_to_quadratic_form, sym h x y, ←two_mul, ←mul_assoc, inv_of_mul_self, one_mul]
+by rw [associated_to_quadratic_form, is_symm.eq h x y, ←two_mul, ←mul_assoc, inv_of_mul_self,
+  one_mul]
 
 lemma to_quadratic_form_associated : (associated_hom S Q).to_quadratic_form = Q :=
 quadratic_form.ext $ λ x,
@@ -547,7 +548,7 @@ associated_hom ℤ
 /-- Symmetric bilinear forms can be lifted to quadratic forms -/
 instance : can_lift (bilin_form R M) (quadratic_form R M) :=
 { coe := associated_hom ℕ,
-  cond := is_sym,
+  cond := bilin_form.is_symm,
   prf := λ B hB, ⟨B.to_quadratic_form, associated_left_inverse _ hB⟩ }
 
 /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated
@@ -769,7 +770,7 @@ lemma nondegenerate_of_anisotropic
 on a module `M` over a ring `R` with invertible `2`, i.e. there exists some
 `x : M` such that `B x x ≠ 0`. -/
 lemma exists_bilin_form_self_ne_zero [htwo : invertible (2 : R)]
-  {B : bilin_form R M} (hB₁ : B ≠ 0) (hB₂ : sym_bilin_form.is_sym B) :
+  {B : bilin_form R M} (hB₁ : B ≠ 0) (hB₂ : B.is_symm) :
   ∃ x, ¬ B.is_ortho x x :=
 begin
   lift B to quadratic_form R M using hB₂ with Q,
@@ -785,7 +786,7 @@ variable [finite_dimensional K V]
 /-- Given a symmetric bilinear form `B` on some vector space `V` over a field `K`
 in which `2` is invertible, there exists an orthogonal basis with respect to `B`. -/
 lemma exists_orthogonal_basis [hK : invertible (2 : K)]
-  {B : bilin_form K V} (hB₂ : sym_bilin_form.is_sym B) :
+  {B : bilin_form K V} (hB₂ : B.is_symm) :
   ∃ (v : basis (fin (finrank K V)) K V), B.is_Ortho v :=
 begin
   tactic.unfreeze_local_instances,
@@ -801,7 +802,7 @@ begin
   rw [← submodule.finrank_add_eq_of_is_compl (is_compl_span_singleton_orthogonal hx).symm,
       finrank_span_singleton (ne_zero_of_not_is_ortho_self x hx)] at hd,
   let B' := B.restrict (B.orthogonal $ K ∙ x),
-  obtain ⟨v', hv₁⟩ := ih (B.restrict_sym hB₂ _ : sym_bilin_form.is_sym B') (nat.succ.inj hd),
+  obtain ⟨v', hv₁⟩ := ih (B.restrict_symm hB₂ _ : B'.is_symm) (nat.succ.inj hd),
   -- concatenate `x` with the basis obtained by induction
   let b := basis.mk_fin_cons x v'
     (begin
@@ -923,15 +924,15 @@ variables [finite_dimensional K V]
 
 lemma equivalent_weighted_sum_squares (Q : quadratic_form K V) :
   ∃ w : fin (finite_dimensional.finrank K V) → K, equivalent Q (weighted_sum_squares K w) :=
-let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_is_sym _ Q) in
+let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_is_symm _ Q) in
   ⟨_, ⟨Q.isometry_weighted_sum_squares v hv₁⟩⟩
 
 lemma equivalent_weighted_sum_squares_units_of_nondegenerate'
   (Q : quadratic_form K V) (hQ : (associated Q).nondegenerate) :
   ∃ w : fin (finite_dimensional.finrank K V) → units K,
     equivalent Q (weighted_sum_squares K w) :=
 begin
-  obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_is_sym _ Q),
+  obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_is_symm _ Q),
   have hv₂ := hv₁.not_is_ortho_basis_self_of_nondegenerate hQ,
   simp_rw [is_ortho, associated_eq_self_apply] at hv₂,
   exact ⟨λ i, units.mk0 _ (hv₂ i), ⟨Q.isometry_weighted_sum_squares v hv₁⟩⟩,

src/ring_theory/trace.lean

@@ -152,7 +152,7 @@ variables {S}
 -- This is a nicer lemma than the one produced by `@[simps] def trace_form`.
 @[simp] lemma trace_form_apply (x y : S) : trace_form R S x y = trace R S (x * y) := rfl
 
-lemma trace_form_is_sym : sym_bilin_form.is_sym (trace_form R S) :=
+lemma trace_form_is_symm : (trace_form R S).is_symm :=
 λ x y, congr_arg (trace R S) (mul_comm _ _)
 
 lemma trace_form_to_matrix [decidable_eq ι] (i j) :