FiniteJet.GraphKoszul.pow_smul_ker_d1_inter_subset
Mathematical summary.
There is an integer z_E ≥ 0 such that ϖ^{z_E}(ker(d_{1,E}) ∩ T_{E,0}^m) ⊆ d_{2,E}(∧²T_{E,0}^m).
Lean uses the standard finite-free coordinate model of ∧²T_E^m, whose unit ball is ∧²T_{E,0}^m. Choose C such that every y∈ker(d₁) has a preimage x under d₂ with ‖x‖≤C‖y‖, and then choose z_E with |ϖ|^{z_E}C≤1.
Original Lean docstring
Equation (10), lattice-inclusion form ([FJP] Lemma 5.1, generic vertex E):
literally ϖ^z (ker d_{1} ∩ P_{E,0}^m) ⊆ d_{2}(⋀² P_{E,0}^m). Here ker d₁ = {u | d₁ u = 0},P_{E,0}^m = {u | ‖u‖ ≤ 1}, and the second exterior power ⋀² P_{E,0}^m is modelled as
the sup-norm unit ball {v : Pairs m → P E m | ‖v‖ ≤ 1} of P_E^{⊕binom m 2} under the
campaign's ordered-pair d₂ model; ϖ = tP = polyToP (C t).
Used in the paper for: Lemma 5.1 (unit-ball specialization: syzygy denominators)
theorem pow_smul_ker_d1_inter_subset [IsNoetherianRing (P E m)]
(hE₀ : IsNoetherianRing (unitBall E))
(t : E) (htu : IsUnit t) (ht1 : ‖t‖ < 1) (ht0 : 0 < ‖t‖)
(hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖)
(g : E) (f : Fin m → E) (hunit : Ideal.span ({g} ∪ Set.range f) = ⊤)
(r : Fin m → P E m)
(hr : ∀ i, r i = polyToP (MvPolynomial.C g * MvPolynomial.X i - MvPolynomial.C (f i))) :
∃ z : ℕ, (fun u : Fin m → P E m => fun i => polyToP (MvPolynomial.C t) ^ z * u i) ''
({u : Fin m → P E m | d1 r u = 0} ∩ {u | ‖u‖ ≤ 1}) ⊆
(fun v : Pairs m → P E m => d2 r v) '' {v | ‖v‖ ≤ 1}