IdealCycles.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Reconstruction of effective homogeneous prime ideal cycles

def OAI.Nagata.Workers.W30.cycleEquation line 19
Source documentation
Choose an actual polynomial representing the product of prime classes with weights.
```
def cycleEquation (D : Associates TernaryPolynomial →₀ ℕ) : TernaryPolynomial :=
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.cycleEquation_mk line 22
theorem OAI.Nagata.Workers.W30.cycleEquation_nonzero line 26
theorem OAI.Nagata.Workers.W30.cycleEquation_multiplicity line 34
Source documentation
Full multiplicities of an arbitrary finite effective prime cycle are recovered exactly.
```
theorem cycleEquation_multiplicity (D : Associates TernaryPolynomial →₀ ℕ)
    (hD : ∀ a ∈ D.support, Prime a) : equationMultiplicity (cycleEquation D) = D := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial, OAI.Nagata.Workers.W30.cycleEquation
theorem OAI.Nagata.Workers.W30.cycleEquation_idealCycle line 42
theorem OAI.Nagata.Workers.W30.cycleEquation_equationMultiplicity line 49
Source documentation
Reconstructing the divisor of a nonzero equation returns that equation up to a unit.
```
theorem cycleEquation_equationMultiplicity (F : TernaryPolynomial) (hF : F ≠ 0) :
    Associated (cycleEquation (equationMultiplicity F)) F := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial, OAI.Nagata.Workers.W30.cycleEquation
theorem OAI.Nagata.Workers.W30.equationIdealCycle_one line 65
theorem OAI.Nagata.Workers.W30.equationIdealCycle_zero_iff line 69
theorem OAI.Nagata.Workers.W30.degree_pos_of_equationIdealCycle_ne_zero line 75
Source documentation
A nonzero effective cycle has positive polynomial degree.
```
theorem degree_pos_of_equationIdealCycle_ne_zero {F : TernaryPolynomial}
    (hF : F ≠ 0) (hcycle : equationIdealCycle F ≠ 0) : 0 < F.totalDegree := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationIdealCycle_pow line 80
Source documentation
Taking powers multiplies every actual prime-ideal cycle weight.
```
theorem equationIdealCycle_pow (F : TernaryPolynomial) (n : ℕ) :
    equationIdealCycle (F ^ n) = n • equationIdealCycle F := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.span_mem_equationIdealCycle_iff line 98
Source documentation
A principal ideal occurs precisely when its generator is a prime divisor of the equation.
```
theorem span_mem_equationIdealCycle_iff (F f : TernaryPolynomial) (hF : F ≠ 0) :
    Ideal.span ({f} : Set TernaryPolynomial) ∈ (equationIdealCycle F).support ↔
      Prime f ∧ f ∣ F := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
def OAI.Nagata.Workers.W30.principalIdealAssociate line 121
Source documentation
Associate class of a principal ideal; unsupported nonprincipal ideals map to zero.
```
def principalIdealAssociate (I : Ideal TernaryPolynomial) : Associates TernaryPolynomial := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.associatePrincipalIdeal_principalIdealAssociate line 126
theorem OAI.Nagata.Workers.W30.principalIdealAssociate_prime line 132
theorem OAI.Nagata.Workers.W30.exists_equation_of_prime_principal_cycle line 148
Source documentation
Every finite effective cycle on actual nonzero prime principal ideals is the factor cycle of a nonzero polynomial.
```
theorem exists_equation_of_prime_principal_cycle (D : Ideal TernaryPolynomial →₀ ℕ)
    (hD : ∀ I ∈ D.support, I.IsPrime ∧ I ≠ ⊥ ∧ I.IsPrincipal) :
    ∃ F : TernaryPolynomial, F ≠ 0 ∧ equationIdealCycle F = D := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial

theorem OAI.Nagata.Workers.W30.equationIdealCycle_homogeneous line 181

Source documentation

Every prime ideal in the cycle of a homogeneous equation is genuinely homogeneous.

theorem equationIdealCycle_homogeneous {F : TernaryPolynomial} {d : ℕ}
    (hF : F ≠ 0) (hhom : F.IsHomogeneous d) {I : Ideal TernaryPolynomial}
    (hI : I ∈ (equationIdealCycle F).support) :
    I.IsHomogeneous (homogeneousSubmodule (Fin 3) ℂ) := by
…

Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial

theorem OAI.Nagata.Workers.W30.homogeneous_of_equationIdealCycle line 199

Source documentation

If every ideal in the factor cycle is homogeneous, the equation is homogeneous.

theorem homogeneous_of_equationIdealCycle {F : TernaryPolynomial} (hF : F ≠ 0)
    (hhom : ∀ I ∈ (equationIdealCycle F).support,
      I.IsHomogeneous (homogeneousSubmodule (Fin 3) ℂ)) :
    F.IsHomogeneous F.totalDegree := by
…

Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial

theorem OAI.Nagata.Workers.W30.exists_homogeneous_equation_of_prime_principal_cycle line 215

Source documentation

Every finite effective cycle of actual homogeneous nonzero prime principal ideals comes from a nonzero homogeneous polynomial, with every multiplicity preserved.

theorem exists_homogeneous_equation_of_prime_principal_cycle
    (D : Ideal TernaryPolynomial →₀ ℕ)
    (hD : ∀ I ∈ D.support, I.IsPrime ∧ I ≠ ⊥ ∧ I.IsPrincipal ∧
      I.IsHomogeneous (homogeneousSubmodule (Fin 3) ℂ)) :
    ∃ F : TernaryPolynomial, F ≠ 0 ∧ F.IsHomogeneous F.totalDegree ∧
      equationIdealCycle F = D := by
…

Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial

theorem OAI.Nagata.Workers.W30.exists_positive_degree_equation_of_homogeneous_cycle line 242
Source documentation
A nonzero finite effective cycle of homogeneous prime principal ideals is represented by a nonzero homogeneous equation of positive degree, with exact weights.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:174 (different declaration text). Qualify references as OAI.Nagata.Workers.W30.exists_positive_degree_equation_of_homogeneous_cycle@path.
```
theorem exists_positive_degree_equation_of_homogeneous_cycle
    (D : Ideal TernaryPolynomial →₀ ℕ) (hD0 : D ≠ 0)
    (hD : ∀ I ∈ D.support, I.IsPrime ∧ I ≠ ⊥ ∧ I.IsPrincipal ∧
      I.IsHomogeneous (homogeneousSubmodule (Fin 3) ℂ)) :
    ∃ F : TernaryPolynomial, F ≠ 0 ∧ F.IsHomogeneous F.totalDegree ∧
      0 < F.totalDegree ∧ equationIdealCycle F = D := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial