ReleaseTransferMatrix.lean

1 import Mathlib.LinearAlgebra.Matrix.Adjugate
2 
3 /-! Shared determinant-adjugate construction and endpoint contraction.
4 The only inverse premise is for the scalar determinant. The power-series
5 specializations construct that inverse from the proved constant coefficient 1.
6 -/
7 set_option autoImplicit false
8 open scoped BigOperators
9 
10 namespace Komorebi.PaperII.ReleaseTransferMatrix
11 universe u v w
12 variable {V : Type u} {P : Type v} {S : Type w}
13 variable [Fintype V] [DecidableEq V] [CommRing P] [CommRing S]
14 
15 noncomputable def rationalMatrix (f : P →+* S) (T : Matrix V V P) (d : S) :
16     Matrix V V S := d • f.mapMatrix (Matrix.adjugate T)
17 
18 theorem map_mul_adjugate (f : P →+* S) (T : Matrix V V P) :
19     f.mapMatrix T * f.mapMatrix (Matrix.adjugate T) =
20       f (Matrix.det T) • (1 : Matrix V V S) := by
21   calc
22     _ = f.mapMatrix (Matrix.det T • (1 : Matrix V V P)) := by
23       simpa using congrArg f.mapMatrix (Matrix.mul_adjugate T)
24     _ = _ := by
25       ext i j
26       by_cases h : i = j <;> simp [RingHom.mapMatrix_apply, Matrix.map_apply, h]
27 
28 theorem map_adjugate_mul (f : P →+* S) (T : Matrix V V P) :
29     f.mapMatrix (Matrix.adjugate T) * f.mapMatrix T =
30       f (Matrix.det T) • (1 : Matrix V V S) := by
31   calc
32     _ = f.mapMatrix (Matrix.det T • (1 : Matrix V V P)) := by
33       simpa using congrArg f.mapMatrix (Matrix.adjugate_mul T)
34     _ = _ := by
35       ext i j
36       by_cases h : i = j <;> simp [RingHom.mapMatrix_apply, Matrix.map_apply, h]
37 
38 theorem mul_rationalMatrix (f : P →+* S) (T : Matrix V V P) (d : S)
39     (h : d * f (Matrix.det T) = 1) :
40     f.mapMatrix T * rationalMatrix f T d = 1 := by
41   rw [rationalMatrix, Matrix.mul_smul, map_mul_adjugate, smul_smul, h, one_smul]
42 
43 theorem rationalMatrix_mul (f : P →+* S) (T : Matrix V V P) (d : S)
44     (h : d * f (Matrix.det T) = 1) :
45     rationalMatrix f T d * f.mapMatrix T = 1 := by
46   rw [rationalMatrix, Matrix.smul_mul, map_adjugate_mul, smul_smul, h, one_smul]
47 
48 theorem denominator_smul_rationalMatrix (f : P →+* S) (T : Matrix V V P) (d : S)
49     (h : f (Matrix.det T) * d = 1) :
50     f (Matrix.det T) • rationalMatrix f T d = f.mapMatrix (Matrix.adjugate T) := by
51   rw [rationalMatrix, smul_smul, h, one_smul]
52 
53 def contract (u : V → P) (M : Matrix V V P) (v : V → P) : P :=
54   ∑ i, ∑ j, u i * M i j * v j
55 
56 theorem contract_map (f : P →+* S) (u v : V → P) (M : Matrix V V P) :
57     contract (f ∘ u) (f.mapMatrix M) (f ∘ v) = f (contract u M v) := by
58   simp [contract, map_sum, map_mul, RingHom.mapMatrix_apply, Matrix.map_apply]
59 
60 omit [DecidableEq V] in
61 theorem mul_contract (a : P) (u v : V → P) (M : Matrix V V P) :
62     a * contract u M v = contract u (a • M) v := by
63   simp only [contract, Finset.mul_sum]
64   apply Finset.sum_congr rfl
65   intro i _
66   apply Finset.sum_congr rfl
67   intro j _
68   change a * (u i * M i j * v j) = u i * (a * M i j) * v j
69   ac_rfl
70 
71 theorem rational_endpoint_identity (f : P →+* S) (T : Matrix V V P) (d : S)
72     (h : f (Matrix.det T) * d = 1) (u v : V → P) :
73     f (Matrix.det T) * contract (f ∘ u) (rationalMatrix f T d) (f ∘ v) =
74       f (contract u (Matrix.adjugate T) v) := by
75   rw [mul_contract, denominator_smul_rationalMatrix f T d h, contract_map]
76 
77 end Komorebi.PaperII.ReleaseTransferMatrix

Back to source controls