Finite generic scalar perturbations

A finite family of affine matrix paths can be made simultaneously nonsingular by choosing an arbitrarily small positive parameter away from the finitely many determinant roots. This is the only genericity input needed by the S6 subdivision argument: the perturbation direction is fixed globally, so face compatibility and prime equivariance are preserved automatically.

noncomputable def NRR.FiniteGenericPerturbation.matrixPath {n : Type u_1} (A B : Matrix n n ℝ) : Matrix n n (Polynomial ℝ)

Polynomial-valued straight-line path from A to B.

Equations

• NRR.FiniteGenericPerturbation.matrixPath A B = Matrix.of fun (i j : n) => Polynomial.C (A i j) + Polynomial.X * Polynomial.C (B i j - A i j)

noncomputable def NRR.FiniteGenericPerturbation.determinantPath {n : Type u_1} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) : Polynomial ℝ

Determinant polynomial of the straight-line matrix path.

Equations

• NRR.FiniteGenericPerturbation.determinantPath A B = (NRR.FiniteGenericPerturbation.matrixPath A B).det

theorem NRR.FiniteGenericPerturbation.eval_matrixPath {n : Type u_1} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) (t : ℝ) : (Polynomial.evalRingHom t).mapMatrix (matrixPath A B) = (1 - t) • A + t • B

Evaluation of the polynomial matrix path.

theorem NRR.FiniteGenericPerturbation.eval_determinantPath {n : Type u_1} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) (t : ℝ) : Polynomial.eval t (determinantPath A B) = ((1 - t) • A + t • B).det

Evaluation of the determinant path is the determinant of the evaluated matrix path.

@[simp]

theorem NRR.FiniteGenericPerturbation.eval_one_determinantPath {n : Type u_1} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) : Polynomial.eval 1 (determinantPath A B) = B.det

At parameter one the determinant polynomial evaluates to the target determinant.

theorem NRR.FiniteGenericPerturbation.determinantPath_ne_zero_of_target {n : Type u_1} [Fintype n] [DecidableEq n] (A B : Matrix n n ℝ) (hB : B.det ≠ 0) : determinantPath A B ≠ 0

A regular target matrix gives a nonzero determinant polynomial.

theorem NRR.FiniteGenericPerturbation.finite_badParameters {I : Type u_2} [Finite I] (P : I → Polynomial ℝ) (hP : ∀ (i : I), P i ≠ 0) : {t : ℝ | ∃ (i : I), Polynomial.eval t (P i) = 0}.Finite

The union of the real root sets of a finite family of nonzero polynomials is finite.

theorem NRR.FiniteGenericPerturbation.exists_small_positive_avoiding {I : Type u_2} [Finite I] (P : I → Polynomial ℝ) (hP : ∀ (i : I), P i ≠ 0) {eps : ℝ} (heps : 0 < eps) : ∃ (t : ℝ), 0 < t ∧ t < eps ∧ ∀ (i : I), Polynomial.eval t (P i) ≠ 0

Arbitrarily small positive parameters avoid all roots of a finite nonzero polynomial family.

theorem NRR.FiniteGenericPerturbation.exists_small_positive_regular {n : Type u_1} {I : Type u_2} [Fintype n] [DecidableEq n] [Finite I] (A B : I → Matrix n n ℝ) (hB : ∀ (i : I), (B i).det ≠ 0) {eps : ℝ} (heps : 0 < eps) : ∃ (t : ℝ), 0 < t ∧ t < eps ∧ ∀ (i : I), ((1 - t) • A i + t • B i).det ≠ 0

Simultaneous regularization of a finite family of matrix paths.