det_traceForm_ne_zero — Mathlib

English

Let b be a basis of L over K with Algebra.IsSeparable K L. The determinant of the trace form matrix in this basis is nonzero.

Русский

Пусть b — базис L над K и K⊆L отделимо. Детерминант матрицы формы следа в этом базисе не нулевой.

LaTeX

$$$\\det\\big( \\mathrm{BilinForm.toMatrix}(b,\\mathrm{traceForm}(K,L)) \\big) \\neq 0$$$

Lean4

theorem det_traceForm_ne_zero [Algebra.IsSeparable K L] [DecidableEq ι] (b : Basis ι K L) :
    det (BilinForm.toMatrix b (traceForm K L)) ≠ 0 :=
  by
  haveI : FiniteDimensional K L := FiniteDimensional.of_fintype_basis b
  let pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable _ _
  rw [← BilinForm.toMatrix_mul_basis_toMatrix pb.basis b, ← det_comm' (pb.basis.toMatrix_mul_toMatrix_flip b) _, ←
    Matrix.mul_assoc, det_mul]
  swap; · apply Basis.toMatrix_mul_toMatrix_flip
  refine mul_ne_zero (isUnit_of_mul_eq_one _ ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det ?_).ne_zero ?_
  ·
    calc
      (pb.basis.toMatrix b * (pb.basis.toMatrix b)ᵀ).det * ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det =
          (pb.basis.toMatrix b * (b.toMatrix pb.basis * pb.basis.toMatrix b)ᵀ * b.toMatrix pb.basis).det :=
        by simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]
      _ = 1 := by simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one, Matrix.det_one]
  simpa only [traceMatrix_of_basis] using det_traceMatrix_ne_zero' pb

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