NormalCoefficients.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Principal restrictions and local normal coefficient families

theorem OAI.Nagata.W18.not_dvd_remainder_of_maximal_power line 24
Source documentation
A factorization that cannot be extended by another G has a remainder not divisible by G. This implication needs no domain assumption.
```
theorem not_dvd_remainder_of_maximal_power {A : Type*} [CommRing A]
    (G S T : A) (j : ℕ) (hfactor : S = G ^ j * T)
    (hmaximal : ¬G ^ (j + 1) ∣ S) : ¬G ∣ T := by
…
```

theorem OAI.Nagata.W18.residue_ne_zero_of_maximal_power line 33

Source documentation

Maximal extracted powers give nonzero residues in the genuine quotient.

theorem residue_ne_zero_of_maximal_power {A : Type*} [CommRing A]
    (G S T : A) (j : ℕ) (hfactor : S = G ^ j * T)
    (hmaximal : ¬G ^ (j + 1) ∣ S) :
    Ideal.Quotient.mk (Ideal.span ({G} : Set A)) T ≠ 0 := by
…

theorem OAI.Nagata.W18.residue_ne_zero_of_not_dvd line 42

Source documentation

The direct form needed when maximal factorization returns ¬G ∣ T.

theorem residue_ne_zero_of_not_dvd {A : Type*} [CommRing A]
    (G T : A) (hT : ¬G ∣ T) :
    Ideal.Quotient.mk (Ideal.span ({G} : Set A)) T ≠ 0 := by
…

theorem OAI.Nagata.W18.principal_quotient_isDomain line 50
Source documentation
A prime hypersurface ideal supplies the expected domain structure. The preceding nonzero-residue statements hold even without this hypothesis.
```
theorem principal_quotient_isDomain {A : Type*} [CommRing A]
    (G : A) (hprime : (Ideal.span ({G} : Set A)).IsPrime) :
    IsDomain (A ⧸ Ideal.span ({G} : Set A)) := by
…
```

theorem OAI.Nagata.W18.principal_normal_polynomial_ne_zero line 56

Source documentation

The selected normal polynomial is nonzero over the hypersurface quotient.

theorem principal_normal_polynomial_ne_zero {A : Type*} [CommRing A]
    (s : Finset ℕ) (G : A) (S T : ℕ → A) (j : ℕ → ℕ) (u : ℕ)
    (hne : s.Nonempty) (hweight : ∀ a ∈ s, a + j a = u)
    (hfactor : ∀ a ∈ s, S a = G ^ j a * T a)
    (hmaximal : ∀ a ∈ s, ¬G ^ (j a + 1) ∣ S a) :
    (∑ a ∈ s, Polynomial.monomial (j a)
      (Ideal.Quotient.mk (Ideal.span ({G} : Set A)) (T a))) ≠ 0 := by
…

theorem OAI.Nagata.W18.principal_diagonal_polynomial_ne_zero line 69

Source documentation

Direct interface for maximal-factorization APIs returning indivisible remainders.

theorem principal_diagonal_polynomial_ne_zero {A : Type*} [CommRing A]
    (s : Finset ℕ) (G : A) (T : ℕ → A) (j : ℕ → ℕ) (u : ℕ)
    (hne : s.Nonempty) (hweight : ∀ a ∈ s, a + j a = u)
    (hT : ∀ a ∈ s, ¬G ∣ T a) :
    (∑ a ∈ s, Polynomial.monomial (j a)
      (Ideal.Quotient.mk (Ideal.span ({G} : Set A)) (T a))) ≠ 0 := by
…

theorem OAI.Nagata.W18.mvPolynomial_normal_polynomial_ne_zero line 80

Source documentation

Specialization to genuine multivariable coordinate polynomials.

theorem mvPolynomial_normal_polynomial_ne_zero {K σ : Type*} [Field K]
    (s : Finset ℕ) (G : MvPolynomial σ K) (S T : ℕ → MvPolynomial σ K)
    (j : ℕ → ℕ) (u : ℕ)
    (hne : s.Nonempty) (hweight : ∀ a ∈ s, a + j a = u)
    (hfactor : ∀ a ∈ s, S a = G ^ j a * T a)
    (hmaximal : ∀ a ∈ s, ¬G ^ (j a + 1) ∣ S a) :
    (∑ a ∈ s, Polynomial.monomial (j a)
      (Ideal.Quotient.mk (Ideal.span ({G} : Set (MvPolynomial σ K))) (T a))) ≠ 0 :=
…

theorem OAI.Nagata.W18.restriction_annihilates_principal line 91

Source documentation

A chart ring map annihilating G annihilates its principal ideal.

theorem restriction_annihilates_principal {A B : Type*} [CommRing A] [CommRing B]
    (G : A) (f : A →+* B) (hG : f G = 0) :
    ∀ a ∈ Ideal.span ({G} : Set A), f a = 0 := by
…

def OAI.Nagata.W18.principalRestriction line 99

Source documentation

The induced chart restriction on the genuine hypersurface quotient.

def principalRestriction {A B : Type*} [CommRing A] [CommRing B]
    (G : A) (f : A →+* B) (hG : f G = 0) :
    A ⧸ Ideal.span ({G} : Set A) →+* B :=
…

theorem OAI.Nagata.W18.principalRestriction_residue line 105

Source documentation

A quotient coefficient restricts to the original coefficient's chart value.

theorem principalRestriction_residue {A B : Type*} [CommRing A] [CommRing B]
    (G : A) (f : A →+* B) (hG : f G = 0) (a : A) :
    principalRestriction G f hG (Ideal.Quotient.mk (Ideal.span ({G} : Set A)) a) =
      f a := rfl

Mentions: OAI.Nagata.W18.principalRestriction

theorem OAI.Nagata.W18.selected_coefficient_restriction line 112

Source documentation

Extracting a selected coefficient and then restricting agrees with its original chart restriction. No injectivity of the chart ring map is assumed.

theorem selected_coefficient_restriction {A B : Type*} [CommRing A] [CommRing B]
    (s : Finset ℕ) (G : A) (T : ℕ → A) (j : ℕ → ℕ) (u : ℕ)
    (hweight : ∀ a ∈ s, a + j a = u)
    (f : A →+* B) (hG : f G = 0) (a : ℕ) (ha : a ∈ s) :
    principalRestriction G f hG
      ((∑ b ∈ s, Polynomial.monomial (j b)
        (Ideal.Quotient.mk (Ideal.span ({G} : Set A)) (T b))).coeff (j a)) =
      f (T a) := by
…

Mentions: OAI.Nagata.W18.principalRestriction

def OAI.Nagata.W18.bivariateToNested line 136
Source documentation
Coordinate 0 is the base variable U; coordinate 1 is the fiber variable W.
```
def bivariateToNested : MvPolynomial (Fin 2) K →+* Polynomial (Polynomial K) :=
…
```
def OAI.Nagata.W18.nestedToBivariate line 141
Source documentation
The inverse substitution sends inner X to coordinate 0 and outer X to 1.
```
def nestedToBivariate : Polynomial (Polynomial K) →+* MvPolynomial (Fin 2) K :=
…
```
theorem OAI.Nagata.W18.nestedToBivariate_comp_bivariateToNested line 145
theorem OAI.Nagata.W18.bivariateToNested_comp_nestedToBivariate line 153
def OAI.Nagata.W18.bivariateNestedEquiv line 168
Source documentation
The two concrete polynomial coordinate rings are isomorphic.
```
def bivariateNestedEquiv : MvPolynomial (Fin 2) K ≃+* Polynomial (Polynomial K) :=
…
```

theorem OAI.Nagata.W18.eval_bivariateToNested line 173

Source documentation

Explicit compatibility of both coordinate evaluations.

theorem eval_bivariateToNested (a c : K) (F : MvPolynomial (Fin 2) K) :
    ((bivariateToNested F).eval (Polynomial.C c)).eval a =
      MvPolynomial.eval ![a, c] F := by
…

Mentions: OAI.Nagata.W18.bivariateToNested

theorem OAI.Nagata.W18.nestedPointIdeal_mem_iff line 188
Source documentation
The generated point ideal is exactly the evaluation kernel, not a substitute notion of multiplicity.
```
theorem nestedPointIdeal_mem_iff (a c : K) (H : Polynomial (Polynomial K)) :
    H ∈ nestedPointIdeal a c ↔ (H.eval (Polynomial.C c)).eval a = 0 :=
…
```
Mentions: OAI.Nagata.W18.nestedPointIdeal
theorem OAI.Nagata.W18.pointIdeal_map_bivariateNestedEquiv line 192
theorem OAI.Nagata.W18.nested_order_of_affine_order line 212
Source documentation
The source ordinary multiplicity hypothesis supplies the nested ideal power.
```
theorem nested_order_of_affine_order (a c : K) (m : ℕ)
    (F : MvPolynomial (Fin 2) K)
    (hF : Nagata.AffineMultiplicity.orderAtLeast ![a, c] m F) :
    bivariateToNested F ∈ (nestedPointIdeal a c) ^ m := by
…
```
Mentions: OAI.Nagata.W18.bivariateToNested, OAI.Nagata.W18.nestedPointIdeal
theorem OAI.Nagata.W18.affine_top_coefficient_base_divisibility line 220
theorem OAI.Nagata.W18.affine_fiber_power_divides line 227

def OAI.Nagata.W18.normalCoefficientFamily line 250

Source documentation

The actual finite normal polynomial Σ_{j≤J} q_j(U) W^j.

def normalCoefficientFamily {K : Type*} [CommRing K]
    (J : ℕ) (q : ℕ → Polynomial K) : Polynomial (Polynomial K) :=
…

theorem OAI.Nagata.W18.normalCoefficientFamily_coeff line 255
Source documentation
Coefficient extraction identifies the finite list with the polynomial.
```
theorem normalCoefficientFamily_coeff {K : Type*} [CommRing K]
    (J : ℕ) (q : ℕ → Polynomial K) (j : ℕ) (hj : j ≤ J) :
    (normalCoefficientFamily J q).coeff j = q j := by
…
```
Mentions: OAI.Nagata.W18.normalCoefficientFamily
theorem OAI.Nagata.W18.normalCoefficientFamily_natDegree_le line 263
Source documentation
The finite list has the required fiber degree bound, even with zero coefficients.
```
theorem normalCoefficientFamily_natDegree_le {K : Type*} [CommRing K]
    (J : ℕ) (q : ℕ → Polynomial K) :
    (normalCoefficientFamily J q).natDegree ≤ J := by
…
```
Mentions: OAI.Nagata.W18.normalCoefficientFamily

theorem OAI.Nagata.W18.family_top_base_divisibility line 271

Source documentation

Surface order at arbitrary (a,c) forces order m-J of the top list coefficient.

theorem family_top_base_divisibility {K : Type*} [CommRing K]
    (J : ℕ) (q : ℕ → Polynomial K) (a c : K) (m : ℕ)
    (hH : normalCoefficientFamily J q ∈ (nestedPointIdeal a c) ^ m) :
    (X - C a) ^ (m - J) ∣ q J := by
…

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

theorem OAI.Nagata.W18.all_coefficients_base_divisibility_at_zero line 281
Source documentation
At zero fiber displacement, every coefficient has the base-order bound. No degree assumption is needed for this statement.
```
theorem all_coefficients_base_divisibility_at_zero {K : Type*} [CommRing K]
    (H : Polynomial (Polynomial K)) (a : K) (m : ℕ)
    (hH : H ∈ (nestedPointIdeal a 0) ^ m) (j : ℕ) :
    (X - C a) ^ (m - j) ∣ H.coeff j := by
…
```
Mentions: OAI.Nagata.W18.nestedPointIdeal

theorem OAI.Nagata.W18.family_coefficient_base_divisibility_at_zero line 289

Source documentation

Finite-list version of the nine-zero coefficient condition.

theorem family_coefficient_base_divisibility_at_zero {K : Type*} [CommRing K]
    (J : ℕ) (q : ℕ → Polynomial K) (a : K) (m j : ℕ) (hj : j ≤ J)
    (hH : normalCoefficientFamily J q ∈ (nestedPointIdeal a 0) ^ m) :
    (X - C a) ^ (m - j) ∣ q j := by
…

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

theorem OAI.Nagata.W18.surface_order_penultimate_coefficient line 298

Source documentation

The actual surface ideal condition supplies the square-case penultimate fiber coefficient identity, retaining the nonzero leading coefficient.

theorem surface_order_penultimate_coefficient {K : Type*} [Field K]
    (H : Polynomial (Polynomial K)) (a c : K) (m : ℕ) (hm : 0 < m)
    (hdeg : H.natDegree ≤ m) (hH : H ∈ (nestedPointIdeal a c) ^ m)
    (htop : (H.coeff m).eval a ≠ 0) :
    (H.coeff (m - 1)).eval a = (-(m : K) * (H.coeff m).eval a) * c := by
…

Mentions: OAI.Nagata.W18.nestedPointIdeal

theorem OAI.Nagata.W18.family_penultimate_coefficient line 309

Source documentation

Finite normal coefficient list version of the square-case fiber identity.

theorem family_penultimate_coefficient {K : Type*} [Field K]
    (q : ℕ → Polynomial K) (a c : K) (m : ℕ) (hm : 0 < m)
    (hH : normalCoefficientFamily m q ∈ (nestedPointIdeal a c) ^ m)
    (htop : (q m).eval a ≠ 0) :
    (q (m - 1)).eval a = (-(m : K) * (q m).eval a) * c := by
…

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