RelationIdeals.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial relation ideals, generators, and prime relations

def OAI.Nagata.Workers.W25.polynomialRelationIdeal line 19
Source documentation
Every relation is tested by evaluation at every point of the punctured plane.
```
def polynomialRelationIdeal (s : Fin 3 → ℂ → ℂ) :
    Ideal (MvPolynomial (Fin 3) ℂ) :=
…
```
theorem OAI.Nagata.Workers.W25.mem_polynomialRelationIdeal line 23
theorem OAI.Nagata.Workers.W25.one_not_mem_polynomialRelationIdeal line 31
Source documentation
The constant one never vanishes, since the punctured plane contains one.
```
theorem one_not_mem_polynomialRelationIdeal (s : Fin 3 → ℂ → ℂ) :
    (1 : MvPolynomial (Fin 3) ℂ) ∉ polynomialRelationIdeal s := by
…
```
Mentions: OAI.Nagata.Workers.W25.polynomialRelationIdeal
theorem OAI.Nagata.Workers.W25.polynomialRelationIdeal_ne_top line 38
Source documentation
Properness is unconditional and does not assume an algebraic image theorem.
```
theorem polynomialRelationIdeal_ne_top (s : Fin 3 → ℂ → ℂ) :
    polynomialRelationIdeal s ≠ ⊤ := by
…
```
Mentions: OAI.Nagata.Workers.W25.polynomialRelationIdeal

theorem OAI.Nagata.Workers.W25.span_le_polynomialRelationIdeal line 44

Source documentation

Relation-ideal containment is exactly vanishing of each chosen generator.

theorem span_le_polynomialRelationIdeal (s : Fin 3 → ℂ → ℂ)
    (E : Set (MvPolynomial (Fin 3) ℂ)) :
    Ideal.span E ≤ polynomialRelationIdeal s ↔
      ∀ P ∈ E, ∀ z : ℂ, z ≠ 0 → MvPolynomial.eval (fun i => s i z) P = 0 := by
…

Mentions: OAI.Nagata.Workers.W25.polynomialRelationIdeal

theorem OAI.Nagata.Workers.W25.relation_generator_dvd_iff line 64
theorem OAI.Nagata.Workers.W25.exists_eval_ne_zero_of_not_dvd_relation_generator line 71
theorem OAI.Nagata.Workers.W25.polynomialRelationIdeal_isPrime line 95
Source documentation
The identity principle on the connected punctured plane makes its polynomial relation ideal prime. Holomorphicity is an explicit, ordinary function hypothesis.
```
theorem polynomialRelationIdeal_isPrime (s : Fin 3 → ℂ → ℂ)
    (hs : ∀ i, DifferentiableOn ℂ (s i) {z : ℂ | z ≠ 0}) :
    (polynomialRelationIdeal s).IsPrime := by
…
```
Mentions: OAI.Nagata.Workers.W25.polynomialRelationIdeal
theorem OAI.Nagata.Workers.W25.cubicSectionRelationIdeal_isPrime line 106
Source documentation
Specialization to actual degree-three automorphic sections, with their holomorphicity derived from membership in the concrete section space.
```
theorem cubicSectionRelationIdeal_isPrime {τ γ : ℂ}
    (b : Fin 3 → Nagata.W08.automorphicSections τ 3 γ) :
    (polynomialRelationIdeal (fun i => (b i).val)).IsPrime :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.Workers.W25.polynomialRelationIdeal

theorem OAI.Nagata.Workers.W25.exists_cubic_mem_relationIdeal line 114

Source documentation

The actual cubic relation belongs to the relation ideal. Only the stated finite-dimensional degree-nine section input is used here.

theorem exists_cubic_mem_relationIdeal {τ γ : ℂ}
    (b : Fin 3 → Nagata.W08.automorphicSections τ 3 γ)
    [Module.Finite ℂ (Nagata.W08.automorphicSections τ 9 (γ ^ 3))]
    (hdim : Module.finrank ℂ (Nagata.W08.automorphicSections τ 9 (γ ^ 3)) ≤ 9) :
    ∃ P : MvPolynomial (Fin 3) ℂ, P ≠ 0 ∧ P.IsHomogeneous 3 ∧
      P ∈ polynomialRelationIdeal (fun i => (b i).val) := by
…

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

theorem OAI.Nagata.Workers.W25.basis_pair_linear_relation_trivial line 137