English
If an orthogonal basis with respect to a bilinear map has no self-orthogonal elements, then the map is left-separating.
Русский
Если базис, ортогональный по биллинейной карте, не имеет элементов, самоперекрещённых, то отображение леворазделяющее.
LaTeX
$$B.SeparatingLeft, not IsOrtho basis ->$$
Lean4
/-- Given an orthogonal basis with respect to a bilinear map, the bilinear map is left-separating if
the basis has no elements which are self-orthogonal. -/
theorem separatingLeft_of_not_isOrtho_basis_self [NoZeroSMulDivisors R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (v : Basis n R M)
(hO : B.IsOrthoᵢ v) (h : ∀ i, ¬B.IsOrtho (v i) (v i)) : B.SeparatingLeft :=
by
intro m hB
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
rw [LinearEquiv.map_eq_zero_iff]
ext i
rw [Finsupp.zero_apply]
specialize hB (v i)
simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_smulₛₗ₂] at hB
rw [Finset.sum_eq_single i] at hB
· exact (smul_eq_zero.mp hB).elim _root_.id (h i).elim
· intro j _hj hij
replace hij : B (v j) (v i) = 0 := hO hij
rw [hij, RingHom.id_apply, smul_zero]
· intro hi
replace hi : vi i = 0 := Finsupp.notMem_support_iff.mp hi
rw [hi, RingHom.id_apply, zero_smul]
