Oka's lemma on relations with polynomial coefficients #
Oka's lemma [Fre17, Ch. I, 10.4] is the algebraic heart of the coherence of the structure sheaf:
for an πͺ_n-linear map F : πͺ_n^p β πͺ_n whose matrix entries are normalized polynomials in
πͺ_{nβ1}[z_n] of degree < d, the kernel of F is generated, as an πͺ_n-module, by the
relations whose components are polynomials in z_n of degree < 3d.
Here πͺ_n is the ring Conv K (m + 1) of convergent power series in m + 1 variables over
K β {β, β}, the distinguished variable is x_0 (splitFirst, liftTail, weierstrassPoly),
and πͺ_{nβ1}[x_0 : N] is the set of series of x_0-degree < N (DegLt N, DegLt.lean). The
statement rowKer_le_span_degLt says: every relation P (β_j F_j P_j = 0) with F_0 a monic
polynomial in x_0 of degree < d and the other F_j of x_0-degree < d lies in the
πͺ_n-span of the relations whose components have x_0-degree < 3d. The proof follows the two
steps of Freitag's:
- Case A (
rowKer_le_span_degLt_of_weierstrass),F_0 = Qa Weierstrass polynomial of degreed' < d: divide the other components of a relation byQ(Weierstrass division,Hironaka/Analytic/Weierstrass/Division.lean), subtract the trivial relationsH^{(j)} = (βF_j, 0, β¦, Q, β¦, 0), and read the first component off the polynomial division ofβ_j F_j r_jby the monicQthrough the uniqueness of Weierstrass division (this gives the boundd, sharper than the2dof the printed proof). - Case B (
rowKer_le_span_degLt),F_0monic: the preparationF_0 = u Β· Q(Hironaka/Analytic/Weierstrass/Preparation.lean), where the unituis itself a polynomial of degreeβ€ e β d'(degLt_unit_of_monic: polynomial division ofF_0byQand uniqueness of Weierstrass division); the relations of(Q, F_1, β¦)are carried to those of(F_0, F_1, β¦)by(b_0, b_1, β¦) β¦ (b_0, u b_1, β¦, u b_p), which raises the degree bound by less thand.
The real and complex cases have the same proof. The lemma feeds the coherence of the ideal of
relations (Hironaka/AnalyticSpace/Oka).
The relations of a row G over πͺ_n: {P β£ β_j G j * P j = 0} (the relation module of a
system at one point, relationSubmodule of Hironaka/AnalyticSpace/Coherent.lean, is this with the
germs of the entries).
Equations
- Analytic.rowKer G = Manifold.relKer fun (x : Fin 1) => G
Instances For
The relations of G whose components have x_0-degree < N: the submodule K_N of
[Fre17, Ch. I, 10.4].
Equations
- Analytic.degLtRel N G = {b : Fin p β β₯(Analytic.Conv K (m + 1)) | (β (j : Fin p), Analytic.DegLt N β(b j)) β§ b β Analytic.rowKer G}
Instances For
The trivial relation H^{(j)} = (βF_j, 0, β¦, 0, Q, 0, β¦, 0) (Q in slot j + 1).
Equations
- Analytic.trivialRel Q F j = Fin.cons (-F j) (Pi.single j Q)
Instances For
Case A of Oka's lemma (the first step of the proof of [Fre17, Ch. I, 10.4]): for Q a
Weierstrass polynomial of degree d' < d and F_1, β¦, F_p of x_0-degree < d, every relation
of (Q, F_1, β¦, F_p) is an πͺ_n-combination of relations whose components have x_0-degree
< d.
A monic polynomial in x_0 with convergent tail coefficients is convergent.
The second step of the proof of [Fre17, Ch. I, 10.4]: for Fβ = ofPoly Q with Q monic in
x_0 of degree e, regular of order d', the unit u of its Weierstrass preparation
Fβ = u Β· Q' is itself a polynomial in x_0 of degree β€ e β d', by the polynomial division of
Q by the monic Weierstrass polynomial Q' and the uniqueness of the Weierstrass division.
Oka's lemma [Fre17, Ch. I, 10.4]: for Fβ a monic polynomial in x_0 of degree e < d
and F_1, β¦, F_p of x_0-degree < d, every relation of (Fβ, F_1, β¦, F_p) is an
πͺ_n-combination of relations whose components have x_0-degree < 3d (the proof gives < 2d).
The hypothesis is weaker than the printed one, where Fβ is a Weierstrass polynomial (monic with
coefficients in the maximal ideal): only monicity of Fβ is used.