not_isOrtho_basis_self_of_separatingLeft

English

For a symmetric bilinear form, a restriction to W with a complementary ker is nondegenerate.

Русский

Для симметричной билинейной формы ограничение на W с комплементарным ядром невырождено.

LaTeX

$$IsSymm.restrict_nondegenerate_with_ker_complement$$

Lean4

/-- An orthogonal basis with respect to a left-separating bilinear map has no self-orthogonal
elements. -/
theorem not_isOrtho_basis_self_of_separatingLeft [Nontrivial R] {B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Basis n R M}
    (h : B.IsOrthoᵢ v) (hB : B.SeparatingLeft) (i : n) : ¬B.IsOrtho (v i) (v i) :=
  by
  intro ho
  refine v.ne_zero i (hB (v i) fun m ↦ ?_)
  obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
  rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum]
  apply Finset.sum_eq_zero
  rintro j -
  rw [map_smulₛₗ]
  suffices B (v i) (v j) = 0 by rw [this, smul_zero]
  obtain rfl | hij := eq_or_ne i j
  · exact ho
  · exact h hij

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