ReleaseResultantDVR.lean

1 import KomorebiVerification.PaperII.ReleaseResultantPolynomial
2 import KomorebiVerification.PaperII.ReleaseGluingPrecisionBridge
3 
4 /-! The actual polynomial resultant supplies the normalized DVR clearing bound. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace Komorebi.PaperII.ReleaseResultantDVR
8 open Polynomial ResultantSeparation ReleaseResultantPolynomial ReleaseGluing
9 open scoped TensorProduct
10 universe u v w
11 variable {O : Type u} {K : Type v} {L : Type w}
12 variable [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
13 variable [Field K] [Algebra O K]
14 variable [AddCommGroup L] [Module O L] [Module.Free O L] [Module.Finite O L]
15 
16 /-- Construct the projector and its uniformizer-power lattice bound from
17 the integral characteristic factorization, with no clearing premise. -/
18 theorem resultant_projector_valuation_bound
19     (pi : O) (hpi : Irreducible pi) (A : Module.End O L) (f g : O[X])
20     (hf : f.Monic) (hg : g.Monic)
21     (hc : IsCoprime (f.map (algebraMap O K)) (g.map (algebraMap O K)))
22     (hchar : A.charpoly = f * g) :
23     ∃ E : Module.End K (K ⊗[O] L),
24       E * E = E ∧
25       LinearMap.range E = LinearMap.ker (aeval (A.baseChange K) (f.map (algebraMap O K))) ∧
26       LinearMap.ker E = LinearMap.ker (aeval (A.baseChange K) (g.map (algebraMap O K))) ∧
27       IsSeparationWeight (algebraMap O K pi) E
28         (tensorLattice (K := K) (R := O) (L := L)).toAddSubgroup
29         (IsDiscreteValuationRing.addVal O (f.resultant g)).toNat := by
30   obtain ⟨u, v, _hbez, cert, hidem, hrange, hker, _hcompl, hclear⟩ :=
31     integral_resultant_projector (K := K) A f g hf hg hc hchar
32   let E := separator (algebraMap O K (f.resultant g))
33     (aeval (A.baseChange K) (v.map (algebraMap O K)))
34     (aeval (A.baseChange K) (g.map (algebraMap O K)))
35   have hr : f.resultant g ≠ 0 := by
36     intro hzero
37     have hn := mapped_resultant_nonzero (K := K) f g hf hg hc
38     exact hn (by rw [hzero, map_zero])
39   refine ⟨E, hidem, hrange, hker, ?_⟩
40   apply original_clearing_weight_at_valuation
41     (tensorLattice (K := K) (R := O) (L := L)) pi hpi (f.resultant g) hr E
42   intro x hx
43   simpa only [LinearMap.smul_apply, algebraMap_smul] using hclear x hx
44 
45 end Komorebi.PaperII.ReleaseResultantDVR

Back to source controls