HomogeneousIdeals.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous relation components and principal cubic ideals

def OAI.Nagata.Workers.W25.scalarLinePolynomial line 19
Source documentation
Polynomial obtained by evaluating a multivariate polynomial on a scalar line.
```
def scalarLinePolynomial {σ : Type*} [Fintype σ]
    (P : MvPolynomial σ ℂ) (x : σ → ℂ) : Polynomial ℂ :=
…
```
theorem OAI.Nagata.Workers.W25.eval_scalarLinePolynomial line 24
theorem OAI.Nagata.Workers.W25.coeff_scalarLinePolynomial line 38
theorem OAI.Nagata.Workers.W25.homogeneousComponent_eval_zero_of_infinite_scalars line 49
theorem OAI.Nagata.Workers.W25.infinite_range_of_injective_multipliers line 74
Source documentation
An everywhere nonzero recurrence with injective successive multipliers cannot take only finitely many values.
```
theorem infinite_range_of_injective_multipliers (a b : ℕ → ℂ)
    (ha : ∀ n, a n ≠ 0) (hb : Function.Injective b)
    (hab : ∀ n, a (n + 1) = b n * a n) : (Set.range a).Infinite := by
…
```

def OAI.Nagata.Workers.W25.cubicOrbitScale line 91

Source documentation

The scalar accumulated along nonnegative iterates of the period.

def cubicOrbitScale (τ γ z : ℂ) : ℕ → ℂ
  | 0 => 1
  | n + 1 => γ * (τ ^ n * z) ^ (-3 : ℤ) * cubicOrbitScale τ γ z n

theorem OAI.Nagata.Workers.W25.cubicOrbitScale_ne_zero line 95
theorem OAI.Nagata.Workers.W25.cubic_section_eval_period_iterate line 102

theorem OAI.Nagata.Workers.W25.cubic_period_multiplier_injective line 113

Source documentation

Distinct period powers give distinct cubic automorphy multipliers.

theorem cubic_period_multiplier_injective {τ γ z : ℂ}
    (hτ : τ ≠ 0) (hτnorm : ‖τ‖ < 1) (hγ : γ ≠ 0) (hz : z ≠ 0) :
    Function.Injective (fun n : ℕ => γ * (τ ^ n * z) ^ (-3 : ℤ)) := by
…

theorem OAI.Nagata.Workers.W25.cubicOrbitScale_infinite line 128
Source documentation
At every nonzero point, the common cubic period scalars have infinite range.
```
theorem cubicOrbitScale_infinite {τ γ z : ℂ}
    (hτ : τ ≠ 0) (hτnorm : ‖τ‖ < 1) (hγ : γ ≠ 0) (hz : z ≠ 0) :
    (Set.range (cubicOrbitScale τ γ z)).Infinite :=
…
```
Mentions: OAI.Nagata.Workers.W25.cubicOrbitScale
theorem OAI.Nagata.Workers.W25.homogeneousComponent_mem_cubicSectionRelationIdeal line 149
Source documentation
Every homogeneous component of an actual section relation is again a relation. The common degree-three automorphy supplies infinitely many scalar zeros at each nonzero cover point. No injectivity or base-point-free hypothesis is needed.
```
theorem homogeneousComponent_mem_cubicSectionRelationIdeal {τ γ : ℂ}
    (hτ : τ ≠ 0) (hτnorm : ‖τ‖ < 1) (hγ : γ ≠ 0)
    (b : Fin 3 → Nagata.W08.automorphicSections τ 3 γ)
    (P : MvPolynomial (Fin 3) ℂ)
    (hP : P ∈ polynomialRelationIdeal (fun i => (b i).val)) (n : ℕ) :
    MvPolynomial.homogeneousComponent n P ∈
      polynomialRelationIdeal (fun i => (b i).val) := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.Workers.W25.polynomialRelationIdeal
theorem OAI.Nagata.Workers.W25.cubicSectionRelationIdeal_isHomogeneous line 180
theorem OAI.Nagata.Workers.W25.exists_actual_cubic_mem_relationIdeal line 202
theorem OAI.Nagata.Workers.W25.actualCubicSectionRelationIdeal_ne_bot line 214
theorem OAI.Nagata.Workers.W25.exists_relation_generator_of_independent_quotient line 235
theorem OAI.Nagata.Workers.W25.actualBasis_binaryCoordinates_algebraicIndependent line 275
theorem OAI.Nagata.Workers.W25.exists_actual_relation_generator line 287

theorem OAI.Nagata.Workers.W25.exists_actual_relation_generator_with_noncancellation line 300

Source documentation

Exact pointwise kernel description for a proved prime homogeneous generator.

theorem exists_actual_relation_generator_with_noncancellation {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1) {γ : ℂ} (hγ : γ ≠ 0)
    (b : Module.Basis (Fin 3) ℂ (Nagata.W08.automorphicSections (τ : ℂ) 3 γ)) :
    ∃ G : MvPolynomial (Fin 3) ℂ,
      Prime G ∧ G.IsHomogeneous G.totalDegree ∧
      0 < G.totalDegree ∧ G.totalDegree ≤ 3 ∧
      polynomialRelationIdeal (fun i => (b i).val) = Ideal.span {G} ∧
      ∀ P : MvPolynomial (Fin 3) ℂ, ¬ G ∣ P →
        ∃ z : ℂ, z ≠ 0 ∧ MvPolynomial.eval (fun i => (b i).val z) P ≠ 0 := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.Workers.W25.polynomialRelationIdeal