FiniteAdequacy.lean

1 import PaperXII.S3Standard
2 import PaperXII.S3Spectrum
3 import PaperXII.S3Adjoint
4 import PaperXII.S3Detection
5 import PaperXII.FiniteGroupCohomology
6 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
7 
8 /-!
9 # The finite adequacy certificate in original Claim 4.2
10 
11 The four adequacy clauses use actual group cohomology and every irreducible
12 subrepresentation of the actual trace-zero conjugation representation. The
13 ambient faithful, absolutely irreducible, split standard representation and
14 the two literal constituent witnesses are recorded in the final certificate.
15 No adequacy theorem is taken as an input.
16 -/
17 
18 set_option autoImplicit false
19 set_option backward.isDefEq.respectTransparency false
20 namespace PaperXII.FiniteAdequacy
21 
22 open S3Standard S3Adjoint S3Detection FiniteGroupCohomology
23 
24 /-- The trace criterion is quantified over every actual irreducible adjoint submodule. -/
25 def TraceDetection : Prop :=
26   ∀ (N : Subrepresentation adjoint), Representation.IsIrreducible (k := K) (G := Group) (V := N.toSubmodule) N.toRepresentation →
27     ∃ (g : Group) (α β : K) (P : S3Adjoint.Mat) (w : Adj),
28       CanonicalProjector (matrixRep K g) α β P ∧ w ∈ N ∧
29         Matrix.trace (P * (w : S3Adjoint.Mat)) ≠ 0
30 
31 /-- The four clauses of adequacy, for the standard S3 representation over F7. -/
32 structure Adequate : Prop where
33   h0_adjoint : Subsingleton (groupCohomology (Rep.of adjoint) 0)
34   h1_trivial : Subsingleton (groupCohomology (Rep.trivial K Group K) 1)
35   h1_adjoint : Subsingleton (groupCohomology (Rep.of adjoint) 1)
36   detection : TraceDetection
37 
38 /-- An irreducible subrepresentation has a nonzero underlying subspace. -/
39 theorem irreducible_subrepresentation_ne_bot (N : Subrepresentation adjoint)
40     (hN : Representation.IsIrreducible (k := K) (G := Group) (V := N.toSubmodule) N.toRepresentation) : N ≠ ⊥ := by
41   intro h
42   have := hN
43   have heq : (⊥ : Subrepresentation N.toRepresentation) = ⊤ := by
44     apply Subrepresentation.toSubmodule_injective
45     apply le_antisymm le_top
46     intro v _
47     have hv : (v : Adj) = 0 := by
48       change (v : Adj) ∈ (⊥ : Subrepresentation adjoint).toSubmodule
49       simpa only [h] using v.property
50     have hz : v = 0 := Subtype.ext hv
51     rw [hz]
52     exact Submodule.zero_mem _
53   exact bot_ne_top heq
54 
55 /-- Separation of all matrices gives the required detection on every irreducible submodule. -/
56 theorem trace_detection : TraceDetection := by
57   intro N hN
58   have hn : N.toSubmodule ≠ ⊥ := fun h =>
59     irreducible_subrepresentation_ne_bot N hN (Subrepresentation.toSubmodule_injective h)
60   obtain ⟨w, hw, hw0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hn
61   have hm : (w : S3Adjoint.Mat) ≠ 0 := fun h => hw0 (Subtype.ext h)
62   obtain ⟨g, α, β, P, hp, ht⟩ := detects_every_nonzero (w : S3Adjoint.Mat) hm
63   exact ⟨g, α, β, P, w, hp, hw, ht⟩
64 
65 /-- The concrete four-clause adequacy assertion. -/
66 theorem adequate : Adequate where
67   h0_adjoint := h0_subsingleton_of_fixed_eq_zero (Rep.of adjoint) fixed_eq_zero
68   h1_trivial := s3_h1_subsingleton (Rep.trivial K Group K)
69   h1_adjoint := s3_h1_subsingleton (Rep.of adjoint)
70   detection := trace_detection
71 
72 /-- Coefficient extension is the same matrix representation over the extension field. -/
73 theorem extension_matrix {L : Type*} [Field L] [Algebra K L] (g : Group) :
74     (matrixRep K g).map (algebraMap K L) = matrixRep L g :=
75   matrixRep_map K (algebraMap K L) g
76 
77 /-- Irreducibility persists over the algebraic closure of the original coefficient field. -/
78 theorem absolutely_irreducible :
79     Representation.IsIrreducible (rep (AlgebraicClosure K)) := irreducible_char_seven
80 
81 /-- Complete ambient hypotheses and the precise additional assertions printed in Claim 4.2. -/
82 structure StandardCertificate : Prop where
83   faithful : Function.Injective (rep K)
84   absolutely_irreducible : Representation.IsIrreducible (rep (AlgebraicClosure K))
85   split : ∀ g : Group, (matrixRep K g).charpoly.Splits
86   adequate : Adequate
87   decomposition : Nonempty ((signRep.prod (rep K)).Equiv adjoint)
88   sign_member : (⟨W 2 3 4, trace_W 2 3 4⟩ : Adj) ∈ signSummand
89   sign_projector : CanonicalProjector (matrixRep K cycle) 2 4 Pt2
90   sign_trace : Matrix.trace (Pt2 * W 2 3 4) = 3 ∧ (3 : K) ≠ 0
91   standard_member : (⟨W 6 4 3, trace_W 6 4 3⟩ : Adj) ∈ standardSummand
92   standard_projector : CanonicalProjector (matrixRep K transposition) 1 (-1) Ps1
93   standard_trace : Matrix.trace (Ps1 * W 6 4 3) = 6 ∧ (6 : K) ≠ 0
94 
95 /-- Original Claim 4.2, with no additional mathematical hypotheses. -/
96 theorem standard_S3_F7 : StandardCertificate where
97   faithful := rep_faithful K
98   absolutely_irreducible := absolutely_irreducible
99   split := S3Spectrum.all_charpolys_split
100   adequate := adequate
101   decomposition := ⟨decompositionEquiv⟩
102   sign_member := W_sign_mem
103   sign_projector := pt2_canonical
104   sign_trace := ⟨trace_sign_witness, by decide⟩
105   standard_member := W_standard_mem
106   standard_projector := ps1_canonical
107   standard_trace := ⟨trace_standard_witness, by decide⟩
108 
109 end PaperXII.FiniteAdequacy

Back to source controls