PolynomialPrescribedTowerLimit.lean

1 module
2 public import PolynomialParameterPath
3 public import PolynomialParameterSystem
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 open Filter Topology
10 
11 namespace Komorebi.PolynomialPrescribedTowerLimit
12 open Komorebi.PolynomialObstruction Komorebi.PolynomialPadicLift
13 open Komorebi.PolynomialParameterSystem
14 
15 variable {m k e : ℕ}
16 
17 /-- Completion preserves prescribed parameter coordinates. The existence of the
18 compatible polynomial tower is an explicit hypothesis of this helper. -/
19 theorem prescribed_tower_limit (p L : ℕ) [Fact (Nat.Prime p)]
20     (F : Fin e → MvPolynomial (Fin (m+k)) ℤ)
21     (z : ℕ → Fin (m+k) → ℤ) (t : ℕ → Fin k → ℤ) (τ : Fin k → ℤ_[p])
22     (hroot : ∀ n i, (p : ℤ)^(L+n) ∣ evalSystem F (z n) i)
23     (hstep : ∀ n i, (p : ℤ)^(L+n) ∣ (z (n+1) - z n) i)
24     (hfree : ∀ n, freePart (z n) = t n)
25     (htlim : Tendsto (fun n i => (t n i : ℤ_[p])) atTop (𝓝 τ)) :
26     ∃ b : Fin (m+k) → ℤ_[p],
27       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 b) ∧
28       (∀ n i, (p : ℤ_[p])^(L+n) ∣ b i - (z n i : ℤ_[p])) ∧
29       (∀ i, padicEval p F b i = 0) ∧ freePart b = τ := by
30   obtain ⟨b, hlim, hprecision⟩ :=
31     PadicTowerLimit.compatible_vector_tower_limit p L z hstep
32   refine ⟨b, hlim, hprecision, polynomial_tower_limit_root p L F z b hroot hlim, ?_⟩
33   funext i
34   have hb := tendsto_pi_nhds.mp hlim (Fin.natAdd m i)
35   have ht := tendsto_pi_nhds.mp htlim i
36   have hseq : (fun n => (z n (Fin.natAdd m i) : ℤ_[p])) =
37       (fun n => (t n i : ℤ_[p])) := by
38     funext n
39     exact congrArg (fun a : ℤ => (a : ℤ_[p])) (congrFun (hfree n) i)
40   rw [hseq] at hb
41   exact tendsto_nhds_unique hb ht
42 
43 #print axioms prescribed_tower_limit
44 
45 end Komorebi.PolynomialPrescribedTowerLimit

Back to source controls