ChainSharpness.lean

1 import PaperXI.MonodromyChain
2 
3 set_option autoImplicit false
4 noncomputable section
5 namespace PaperXI.MonodromyChain
6 variable {K W : Type*} [Field K] [AddCommGroup W] [Module K W]
7 variable {m : ℕ}
8 
9 theorem identity_path (i r : ℕ) : path (K := K) (W := W) (fun _ => 1) i r = 1 := by
10   induction r with
11   | zero => rfl
12   | succ r ih => simp [ih]
13 
14 /-- The bound in Proposition 2.3 cannot be decreased uniformly: the identity
15 transfer chain has no vanishing power before m. -/
16 theorem identity_shift_power_ne_zero [Nontrivial W] {r : ℕ} (hr : r < m) :
17     (shift (K := K) (W := W) (m := m) (fun _ => 1)) ^ r ≠ 0 := by
18   obtain ⟨w, hw⟩ := exists_ne (0 : W)
19   intro h
20   have hm : 0 < m := by omega
21   have hx := congrArg (fun f : Module.End K (Fin m → W) => f (fun _ => w) ⟨0, hm⟩) h
22   have hz : w = 0 := by simpa [pow_apply, hr, identity_path] using hx
23   exact hw hz
24 
25 end PaperXI.MonodromyChain

Back to source controls