CarrierExamples.lean

1 import PaperX.CarrierCompatibility
2 import PaperX.TraceExamples
3 import Mathlib.Tactic.FinCases
4 import Mathlib.Tactic.NormNum
5 
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.CarrierExamples
9 open scoped BigOperators Matrix
10 open Polynomial
11 open PaperX.CarrierSummands PaperX.CarrierPolynomials PaperX.CarrierCompatibility
12 open PaperX.TraceExamples
13 
14 abbrev Selected := Copies (fun _ : Fin 3 => Fin 1 → ℚ) multiplicities
15 abbrev Ambient := Copies (fun _ : Fin 3 => Fin 1 → ℚ) capacities
16 
17 def selectedRep : Representation ℚ G Selected := copiesRep rep multiplicities
18 
19 def ambientRep : Representation ℚ G Ambient := copiesRep rep capacities
20 
21 def embed : Selected →ₗ[ℚ] Ambient := inclusion multiplicities_admissible
22 
23 def retract : Ambient →ₗ[ℚ] Selected := retraction multiplicities_admissible
24 
25 theorem selected_dimension : Module.finrank ℚ Selected = 3 := by
26   rw [copies_finrank]
27   simp [multiplicities, Fin.sum_univ_succ]
28 
29 theorem ambient_dimension : Module.finrank ℚ Ambient = 7 := by
30   rw [copies_finrank]
31   simp [capacities, Fin.sum_univ_succ]
32 
33 theorem example_split (x : Selected) : retract (embed x) = x :=
34   retraction_inclusion (R := ℚ) multiplicities_admissible x
35 
36 theorem example_equivariant (g : G) (x : Selected) :
37     embed (selectedRep g x) = ambientRep g (embed x) :=
38   inclusion_equivariant rep multiplicities_admissible g x
39 
40 theorem actual_observations :
41     (fun j => LinearMap.trace ℚ _ (selectedRep (samples j))) = observed := by
42   rw [show selectedRep = copiesRep rep multiplicities from rfl, sampled_trace]
43   have hc : (fun j i => LinearMap.trace ℚ _ (rep i (samples j))) = separator :=
44     actual_trace_matrix
45   rw [hc]
46   exact observed_trace
47 
48 theorem constituent_charpoly (i : Fin 3) (g : G) :
49     (rep i g).charpoly = X - C (chi i g) := by
50   have he : rep i g = (Matrix.diagonal (fun _ : Fin 1 => chi i g)).toLin' := by
51     apply LinearMap.ext
52     intro x
53     ext k
54     simp [rep, chiHom, Matrix.toLin'_apply,
55       Algebra.algebraMap_eq_smul_one]
56   rw [he, Matrix.charpoly_toLin', Matrix.charpoly_diagonal]
57   simp
58 
59 theorem example_charpoly :
60     (selectedRep (samples 2)).charpoly = (X - 1)^2 * (X + 1) := by
61   rw [show selectedRep = copiesRep rep multiplicities from rfl, copies_charpoly]
62   simp [constituent_charpoly, multiplicities, samples, chi, Fin.prod_univ_succ]
63 
64 /-- A split pair of vector-space maps does not by itself preserve an action. -/
65 def swapMatrix : Matrix (Fin 2) (Fin 2) ℚ := !![0,1;1,0]
66 def partialInclusion : Matrix (Fin 2) (Fin 1) ℚ := fun i _ => if i = 0 then 1 else 0
67 def partialRetraction : Matrix (Fin 1) (Fin 2) ℚ := fun _ i => if i = 0 then 1 else 0
68 
69 theorem partial_split : partialRetraction * partialInclusion = 1 := by
70   ext i j
71   fin_cases i; fin_cases j
72   norm_num [partialRetraction, partialInclusion, Matrix.mul_apply, Fin.sum_univ_succ]
73 
74 theorem swap_square : swapMatrix * swapMatrix = 1 := by
75   ext i j
76   fin_cases i <;> fin_cases j <;>
77     norm_num [swapMatrix, Matrix.mul_apply, Fin.sum_univ_succ]
78 
79 theorem compressed_swap_zero : partialRetraction * swapMatrix * partialInclusion = 0 := by
80   ext i j
81   fin_cases i; fin_cases j
82   norm_num [partialRetraction, partialInclusion, swapMatrix, Matrix.mul_apply, Fin.sum_univ_succ]
83 
84 theorem compression_fails_multiplication :
85     (partialRetraction * swapMatrix * partialInclusion) *
86       (partialRetraction * swapMatrix * partialInclusion) ≠
87     partialRetraction * (swapMatrix * swapMatrix) * partialInclusion := by
88   rw [compressed_swap_zero, swap_square, Matrix.mul_one, partial_split, Matrix.zero_mul]
89   exact zero_ne_one
90 
91 end PaperX.CarrierExamples

Back to source controls