CertificateIsomorphisms.lean

1 import PaperX.MatrixWitnessLimits
2 import PaperX.RepresentationClasses
3 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 
5 /-! A nonzero determinant at one fixed finite precision certifies a genuinely
6 invertible comparison matrix over an injectively containing coefficient field.
7 The matrix is constructed before the conclusion of conjugacy is obtained. -/
8 set_option autoImplicit false
9 
10 namespace PaperX.CertificateIsomorphisms
11 open PaperX.RepresentationLimits PaperX.RepresentationClasses
12 open PaperX.MatrixWitnessLimits
13 
14 variable {R : Type*} [CommRing R] (I : Ideal R)
15 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
16 
17 /-- A single finite-depth nonvanishing certificate detects a nonzero integral
18 determinant.  The determinant need not be an integral unit. -/
19 theorem det_ne_zero_of_reduction (P : Matrix ι ι R) (d : ℕ)
20     (h : (P.map (Ideal.Quotient.mk (I ^ d))).det ≠ 0) : P.det ≠ 0 := by
21   intro hP
22   apply h
23   change ((Ideal.Quotient.mk (I ^ d)).mapMatrix P).det = 0
24   rw [← RingHom.map_det, hP, map_zero]
25 
26 /-- Applying the detector to the actual reconstructed witness. -/
27 theorem reconstructed_det_ne_zero [IsAdicComplete I R]
28     (P : MatrixFamily R I ι) (d : ℕ) (h : (P.maps d).det ≠ 0) :
29     (reconstructMatrix I P).det ≠ 0 := by
30   apply det_ne_zero_of_reduction I (reconstructMatrix I P) d
31   rw [reconstructMatrix_reduces]
32   exact h
33 
34 variable {K : Type*} [Field K]
35 
36 /-- The field image is an actual matrix unit; this uses injectivity and the
37 determinant criterion, not a supplied inverse matrix. -/
38 theorem mapped_matrix_isUnit (inc : R →+* K) (hinj : Function.Injective inc)
39     (P : Matrix ι ι R) (hP : P.det ≠ 0) : IsUnit (P.map inc) := by
40   apply (Matrix.isUnit_iff_isUnit_det _).mpr
41   apply isUnit_iff_ne_zero.mpr
42   change (inc.mapMatrix P).det ≠ 0
43   rw [← RingHom.map_det]
44   intro h
45   exact hP (hinj (h.trans (map_zero inc).symm))
46 
47 variable {G : Type*} [Group G]
48 
49 /-- A nonsingular integral intertwiner becomes an explicit conjugating unit
50 over the coefficient field.  Its value is exactly the image of the supplied
51 matrix. -/
52 theorem exists_conjugating_unit (inc : R →+* K) (hinj : Function.Injective inc)
53     (ρ τ : MatrixRep R G ι) (P : Matrix ι ι R) (hP : P.det ≠ 0)
54     (h : ∀ g, ρ g * P = P * τ g) :
55     ∃ u : (Matrix ι ι K)ˣ, (u : Matrix ι ι K) = P.map inc ∧
56       conjugate u (changeCoefficients inc τ) = changeCoefficients inc ρ := by
57   obtain ⟨u, hu⟩ := mapped_matrix_isUnit inc hinj P hP
58   refine ⟨u, hu, ?_⟩
59   apply MonoidHom.ext
60   intro g
61   have heq : changeCoefficients inc ρ g * (u : Matrix ι ι K) =
62       (u : Matrix ι ι K) * changeCoefficients inc τ g := by
63     rw [hu]
64     have hρ : changeCoefficients inc ρ g = (ρ g).map inc := by ext i j; rfl
65     have hτ : changeCoefficients inc τ g = (τ g).map inc := by ext i j; rfl
66     rw [hρ, hτ]
67     simpa only [Matrix.map_mul] using congrArg (fun M => M.map inc) (h g)
68   change (u : Matrix ι ι K) * changeCoefficients inc τ g *
69     (↑(u⁻¹) : Matrix ι ι K) = _
70   rw [← heq, mul_assoc]
71   simp
72 
73 /-- A finite-depth determinant certificate suffices for the full field-valued
74 representation conjugacy conclusion. -/
75 theorem conjugate_of_finite_certificate (inc : R →+* K)
76     (hinj : Function.Injective inc) (ρ τ : MatrixRep R G ι)
77     (P : Matrix ι ι R) (d : ℕ)
78     (hP : (P.map (Ideal.Quotient.mk (I ^ d))).det ≠ 0)
79     (h : ∀ g, ρ g * P = P * τ g) :
80     Conjugate (changeCoefficients inc τ) (changeCoefficients inc ρ) := by
81   obtain ⟨u, _, hu⟩ := exists_conjugating_unit inc hinj ρ τ P
82     (det_ne_zero_of_reduction I P d hP) h
83   exact ⟨u, hu⟩
84 
85 end PaperX.CertificateIsomorphisms

Back to source controls