feat: a Cartan matrix of a reduced crystallographic root system cannot have eigenvalue 4 (leanprover-community#39491)

This proves the TODO that a Cartan matrix of a reduced crystallographic root system cannot have eigenvalue 4.

Co-authored-by: Oliver Nash <github@olivernash.org>

Author: Yu-Misaka

Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

@@ -8,8 +8,10 @@ module
 public import Mathlib.Algebra.CharZero.Infinite
 public import Mathlib.Algebra.Module.Submodule.Union
 public import Mathlib.Data.Int.Star
+public import Mathlib.LinearAlgebra.Determinant
 public import Mathlib.LinearAlgebra.Matrix.BilinearForm
 public import Mathlib.LinearAlgebra.Matrix.PosDef
+public import Mathlib.LinearAlgebra.Matrix.ZMatrix
 public import Mathlib.LinearAlgebra.RootSystem.Base
 public import Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
 public import Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
@@ -208,6 +210,21 @@ lemma exists_cartanMatrix_diagaonal_mul_posDef [DecidableEq ι] [P.IsRootSystem]
   rw [← PosDef.transpose_iff] at hd'
   aesop
 
+open LinearMap Module.End in
+lemma det_four_sub_cartanMatrix_ne_zero [DecidableEq ι] [P.IsRootSystem] :
+    (4 - b.cartanMatrix).det ≠ 0 := by
+  suffices ¬ HasEigenvalue b.cartanMatrix.toLin' 4 by
+    have aux : (4 - b.cartanMatrix).toLin' = - (b.cartanMatrix.toLin' - (4 : ℤ) • 1) := by ext; simp
+    rwa [ne_eq, ← det_toLin', det_eq_zero_iff_ker_ne_bot, aux, ker_neg, ← eigenspace_def,
+      ← hasEigenvalue_iff]
+  obtain ⟨d, hd, hdS⟩ := b.exists_cartanMatrix_diagaonal_mul_posDef
+  have aux (i j : b.support) : b.cartanMatrix i j ≤ if i = j then 2 else 0 := by
+    rcases eq_or_ne i j with rfl | hij
+    · simp
+    · simpa [hij] using cartanMatrix_le_zero_of_ne b i j hij
+  have := b.cartanMatrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen d hdS hd 2 4 aux
+  aesop
+
 /-- A characterisation of the connectedness of the Dynkin diagram for irreducible root pairings. -/
 lemma induction_on_cartanMatrix [P.IsReduced] [P.IsIrreducible]
     (p : b.support → Prop) {i j : b.support} (hi : p i)

Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basis.lean

@@ -91,9 +91,6 @@ def basis :
 instance : (cartanSubalgebra' b).IsCartanSubalgebra :=
   inferInstanceAs (basis b).cartan.IsCartanSubalgebra
 
--- TODO drop this after: https://github.com/leanprover-community/mathlib4/issues/28713
-variable [Fact ((4 - b.cartanMatrix).det ≠ 0)]
-
 open LieAlgebra.IsKilling in
 /-- Up to equivalence, `LieAlgebra.IsKilling.rootSystem` is left inverse to
 `RootPairing.GeckConstruction.lieAlgebra`. -/

Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean

@@ -352,9 +352,7 @@ lemma coe_genWeightSpace_zero_eq_span_range_u :
     rintro ⟨⟨x, -⟩, hx⟩
     exact ⟨1, funext fun j ↦ by simpa using apply_sum_inl_eq_zero_of_mem_span_h i j hx⟩
 
--- TODO Turn this `Fact` into a lemma: it is always true and may be proved via Perron-Frobenius
--- See https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Eigenvalues.20of.20Cartan.20matrices/near/516844801
-variable [Fact ((4 - b.cartanMatrix).det ≠ 0)] [P.IsReduced] [P.IsIrreducible]
+variable [P.IsReduced] [P.IsIrreducible]
 
 /-- Lemma 4.2 from [Geck](Geck2017). -/
 instance instIsIrreducible [Nonempty ι] :
@@ -369,7 +367,8 @@ instance instIsIrreducible [Nonempty ι] :
   obtain ⟨c, hc⟩ : ∃ c : b.support → K, ∑ i, c i • u i = x :=
     (mem_span_range_iff_exists_fun K).mp <| hU hx
   suffices c = 0 by simp [this, ← hc]
-  have hCM : (4 - b.cartanMatrix).det ≠ 0 := Fact.out
+  have hCM : (4 - b.cartanMatrix).det ≠ 0 :=
+    RootPairing.Base.det_four_sub_cartanMatrix_ne_zero b
   contrapose! hCM
   suffices ((Int.castRingHom K).mapMatrix (4 - b.cartanMatrix)).det = 0 by
     simpa only [← RingHom.map_det, eq_intCast, Int.cast_eq_zero] using this