CoefficientIdeals.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Local coefficient ideals and ideal-power order

theorem OAI.Nagata.W18.coefficient_dvd_of_coordinate_ideal_power line 20

Source documentation

Coefficients of a member of (g,W)^m have the expected divisibility.

theorem coefficient_dvd_of_coordinate_ideal_power {R : Type*} [CommRing R]
    (g : R) (m : ℕ) (H : Polynomial R)
    (hH : H ∈ (Ideal.span ({C g, X} : Set (Polynomial R))) ^ m) :
    ∀ J : ℕ, g ^ (m - J) ∣ H.coeff J := by
…

def OAI.Nagata.W18.nestedPointIdeal line 72
Source documentation
The actual maximal point ideal in the nested bivariate polynomial ring.
```
def nestedPointIdeal {K : Type*} [CommRing K] (a c : K) :
    Ideal (Polynomial (Polynomial K)) :=
…
```

theorem OAI.Nagata.W18.map_nestedPointIdeal_taylor line 77

Source documentation

Translating the outer variable sends (U-a,W-c) to (U-a,W).

theorem map_nestedPointIdeal_taylor {K : Type*} [CommRing K] (a c : K) :
    (nestedPointIdeal a c).map (taylorAlgHom (C c)).toRingHom =
      Ideal.span ({C (X - C a), X} : Set (Polynomial (Polynomial K))) := by
…

Mentions: OAI.Nagata.W18.nestedPointIdeal

theorem OAI.Nagata.W18.top_coefficient_taylor line 86

Source documentation

Translation preserves the coefficient at any index at least the degree.

theorem top_coefficient_taylor {R : Type*} [CommRing R]
    (H : Polynomial R) (r : R) (J : ℕ) (hJ : H.natDegree ≤ J) :
    (taylor r H).coeff J = H.coeff J := by
…

theorem OAI.Nagata.W18.top_coefficient_base_divisibility line 98

Source documentation

Surface order at an arbitrary displacement forces base order m-J of the highest possible fiber coefficient.

theorem top_coefficient_base_divisibility {K : Type*} [CommRing K]
    (H : Polynomial (Polynomial K)) (a c : K) (m J : ℕ)
    (hJ : H.natDegree ≤ J) (hH : H ∈ (nestedPointIdeal a c) ^ m) :
    (X - C a) ^ (m - J) ∣ H.coeff J := by
…

Mentions: OAI.Nagata.W18.nestedPointIdeal

def OAI.Nagata.W18.fiberRestriction line 109
Source documentation
Restriction to the marked base fiber is coefficientwise evaluation U=a.
```
def fiberRestriction {K : Type*} [CommRing K] (a : K) :
    Polynomial (Polynomial K) →+* Polynomial K :=
…
```
theorem OAI.Nagata.W18.fiberRestriction_coeff line 114
Source documentation
Restriction evaluates each base coefficient at the marked point.
```
theorem fiberRestriction_coeff {K : Type*} [CommRing K]
    (H : Polynomial (Polynomial K)) (a : K) (j : ℕ) :
    (fiberRestriction a H).coeff j = (H.coeff j).eval a :=
…
```
Mentions: OAI.Nagata.W18.fiberRestriction
theorem OAI.Nagata.W18.fiberRestriction_natDegree_le line 120
Source documentation
Restriction cannot increase the degree in the fiber variable.
```
theorem fiberRestriction_natDegree_le {K : Type*} [CommRing K]
    (H : Polynomial (Polynomial K)) (a : K) :
    (fiberRestriction a H).natDegree ≤ H.natDegree :=
…
```
Mentions: OAI.Nagata.W18.fiberRestriction

theorem OAI.Nagata.W18.fiberRestriction_leadingCoeff line 126

Source documentation

A surviving top coefficient is the leading coefficient on the fiber.

theorem fiberRestriction_leadingCoeff {K : Type*} [CommRing K]
    (H : Polynomial (Polynomial K)) (a : K) (J : ℕ)
    (hJ : H.natDegree ≤ J) (hne : (H.coeff J).eval a ≠ 0) :
    (fiberRestriction a H).leadingCoeff = (H.coeff J).eval a := by
…

Mentions: OAI.Nagata.W18.fiberRestriction

theorem OAI.Nagata.W18.map_nestedPointIdeal_fiber line 136
Source documentation
The point ideal maps to the principal fiber point ideal (W-c).
```
theorem map_nestedPointIdeal_fiber {K : Type*} [CommRing K] (a c : K) :
    (nestedPointIdeal a c).map (fiberRestriction a) =
      Ideal.span ({X - C c} : Set (Polynomial K)) := by
…
```
Mentions: OAI.Nagata.W18.nestedPointIdeal, OAI.Nagata.W18.fiberRestriction
theorem OAI.Nagata.W18.fiber_power_divides_of_surface_order line 145
Source documentation
Surface ideal-power order restricts to fiber root divisibility, including when the entire fiber restriction is zero.
```
theorem fiber_power_divides_of_surface_order {K : Type*} [CommRing K]
    (H : Polynomial (Polynomial K)) (a c : K) (m : ℕ)
    (hH : H ∈ (nestedPointIdeal a c) ^ m) :
    (X - C c) ^ m ∣ fiberRestriction a H := by
…
```
Mentions: OAI.Nagata.W18.nestedPointIdeal, OAI.Nagata.W18.fiberRestriction

theorem OAI.Nagata.W18.fiber_rootMultiplicity_ge line 155

Source documentation

For nonzero fiber restrictions, the same condition is the actual ordinary root-multiplicity lower bound.

theorem fiber_rootMultiplicity_ge {K : Type*} [CommRing K] [IsDomain K]
    (H : Polynomial (Polynomial K)) (a c : K) (m : ℕ)
    (hH : H ∈ (nestedPointIdeal a c) ^ m) (hne : fiberRestriction a H ≠ 0) :
    m ≤ (fiberRestriction a H).rootMultiplicity c := by
…

Mentions: OAI.Nagata.W18.nestedPointIdeal, OAI.Nagata.W18.fiberRestriction