HolonomyResidual.lean

1 import Mathlib.LinearAlgebra.Pi
2 import Mathlib.Tactic
3 
4 /-! Paper XI, Proposition 14.6. The supplied equivalences are actual
5 root-to-vertex transports. Constructing the graph/tree is a separate obligation. -/
6 set_option autoImplicit false
7 namespace PaperXI.HolonomyResidual
8 
9 variable {K Vr Vu Vv Wr Wu Wv : Type*} [Field K]
10 variable [AddCommGroup Vr] [Module K Vr] [AddCommGroup Vu] [Module K Vu]
11 variable [AddCommGroup Vv] [Module K Vv] [AddCommGroup Wr] [Module K Wr]
12 variable [AddCommGroup Wu] [Module K Wu] [AddCommGroup Wv] [Module K Wv]
13 
14 def transported (U : Vr ≃ₗ[K] Wr) (A : Vr ≃ₗ[K] Vu) (B : Wr ≃ₗ[K] Wu) :
15     Vu ≃ₗ[K] Wu := (A.symm.trans U).trans B
16 
17 @[simp] theorem transported_apply (U : Vr ≃ₗ[K] Wr) (A : Vr ≃ₗ[K] Vu)
18     (B : Wr ≃ₗ[K] Wu) (x : Vu) : transported U A B x = B (U (A.symm x)) := rfl
19 
20 def cycleDefect (U : Vr ≃ₗ[K] Wr)
21     (Au : Vr ≃ₗ[K] Vu) (Av : Vr ≃ₗ[K] Vv)
22     (Bu : Wr ≃ₗ[K] Wu) (Bv : Wr ≃ₗ[K] Wv)
23     (A : Vu ≃ₗ[K] Vv) (B : Wu ≃ₗ[K] Wv) : Vr →ₗ[K] Wr :=
24   U.toLinearMap.comp (Av.symm.toLinearMap.comp (A.toLinearMap.comp Au.toLinearMap)) -
25     Bv.symm.toLinearMap.comp (B.toLinearMap.comp (Bu.toLinearMap.comp U.toLinearMap))
26 
27 def edgeResidual (U : Vr ≃ₗ[K] Wr)
28     (Au : Vr ≃ₗ[K] Vu) (Av : Vr ≃ₗ[K] Vv)
29     (Bu : Wr ≃ₗ[K] Wu) (Bv : Wr ≃ₗ[K] Wv)
30     (A : Vu ≃ₗ[K] Vv) (B : Wu ≃ₗ[K] Wv) : Vu →ₗ[K] Wv :=
31   (transported U Av Bv).toLinearMap.comp A.toLinearMap -
32     B.toLinearMap.comp (transported U Au Bu).toLinearMap
33 
34 theorem residual_factorization (U : Vr ≃ₗ[K] Wr)
35     (Au : Vr ≃ₗ[K] Vu) (Av : Vr ≃ₗ[K] Vv)
36     (Bu : Wr ≃ₗ[K] Wu) (Bv : Wr ≃ₗ[K] Wv)
37     (A : Vu ≃ₗ[K] Vv) (B : Wu ≃ₗ[K] Wv) :
38     edgeResidual U Au Av Bu Bv A B =
39       Bv.toLinearMap.comp ((cycleDefect U Au Av Bu Bv A B).comp Au.symm.toLinearMap) := by
40   ext x
41   simp [edgeResidual, cycleDefect, transported]
42 
43 theorem residual_zero_iff (U : Vr ≃ₗ[K] Wr)
44     (Au : Vr ≃ₗ[K] Vu) (Av : Vr ≃ₗ[K] Vv)
45     (Bu : Wr ≃ₗ[K] Wu) (Bv : Wr ≃ₗ[K] Wv)
46     (A : Vu ≃ₗ[K] Vv) (B : Wu ≃ₗ[K] Wv) :
47     edgeResidual U Au Av Bu Bv A B = 0 ↔ cycleDefect U Au Av Bu Bv A B = 0 := by
48   rw [residual_factorization]
49   constructor
50   · intro h
51     apply LinearMap.ext
52     intro x
53     have hx := LinearMap.congr_fun h (Au x)
54     simpa using hx
55   · intro h; simp [h]
56 
57 end PaperXI.HolonomyResidual

Back to source controls