Factorization.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous factorization and height-one prime generators

abbrev OAI.Nagata.Workers.W30.TernaryPolynomial line 27
Also declared: ComparatorChallenges/Nagata.lean:157 (same declaration text).
def OAI.Nagata.Workers.W30.equationFactors line 32
Source documentation
An actual multiset of irreducible polynomial factors; repetitions retain multiplicity.
```
def equationFactors (F : TernaryPolynomial) : Multiset TernaryPolynomial := factors F
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationFactors_irreducible line 34
theorem OAI.Nagata.Workers.W30.equationFactors_product line 37
theorem OAI.Nagata.Workers.W30.equationFactors_unique line 42
Source documentation
Uniqueness means a multiset matching of associated irreducible factors, which includes arbitrary reorderings and multiplication of each factor by a unit.
```
theorem equationFactors_unique {F : TernaryPolynomial} (hF : F ≠ 0)
    (L : Multiset TernaryPolynomial) (hL : ∀ P ∈ L, Irreducible P)
    (hprod : Associated L.prod F) : Multiset.Rel Associated L (equationFactors F) :=
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial, OAI.Nagata.Workers.W30.equationFactors
def OAI.Nagata.Workers.W30.equationMultiplicity line 49
Source documentation
Canonical multiplicities indexed by polynomial associate classes.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:161 (different declaration text). Qualify references as OAI.Nagata.Workers.W30.equationMultiplicity@path.
```
def equationMultiplicity (F : TernaryPolynomial) : Associates TernaryPolynomial →₀ ℕ :=
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationMultiplicity_mul line 52
theorem OAI.Nagata.Workers.W30.equationMultiplicity_pow line 58
theorem OAI.Nagata.Workers.W30.equationMultiplicity_eq_iff line 65
Source documentation
No equation multiplicity is discarded: equality of canonical multiplicity vectors is equivalent to association of nonzero polynomial equations.
```
theorem equationMultiplicity_eq_iff {F G : TernaryPolynomial} (hF : F ≠ 0) (hG : G ≠ 0) :
    equationMultiplicity F = equationMultiplicity G ↔ Associated F G := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
def OAI.Nagata.Workers.W30.associatePrincipalIdeal line 77
Source documentation
Send an associate class to its actual principal ideal.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:165 (different declaration text). Qualify references as OAI.Nagata.Workers.W30.associatePrincipalIdeal@path.
```
def associatePrincipalIdeal (a : Associates TernaryPolynomial) : Ideal TernaryPolynomial :=
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.associatePrincipalIdeal_injective line 80
theorem OAI.Nagata.Workers.W30.associatePrincipalIdeal_mk line 85
def OAI.Nagata.Workers.W30.equationIdealCycle line 89
Source documentation
A finite effective cycle of actual principal ideals, with natural weights.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:169 (different declaration text). Qualify references as OAI.Nagata.Workers.W30.equationIdealCycle@path.
```
def equationIdealCycle (F : TernaryPolynomial) : Ideal TernaryPolynomial →₀ ℕ :=
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationIdealCycle_mul line 92
theorem OAI.Nagata.Workers.W30.equationIdealCycle_eq_iff line 96
theorem OAI.Nagata.Workers.W30.equationMultiplicity_support_prime line 104
Source documentation
Every supported associate class is prime.
```
theorem equationMultiplicity_support_prime (F : TernaryPolynomial)
    {a : Associates TernaryPolynomial} (ha : a ∈ (equationMultiplicity F).support) :
    Prime a := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationIdealCycle_support line 111
Source documentation
The effective ideal cycle is supported on nonzero prime principal ideals.
```
theorem equationIdealCycle_support (F : TernaryPolynomial)
    {I : Ideal TernaryPolynomial} (hI : I ∈ (equationIdealCycle F).support) :
    I.IsPrime ∧ I ≠ ⊥ ∧ I.IsPrincipal := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationIdealCycle_coefficient line 127
Source documentation
Each cycle coefficient is the full factor multiplicity, without merging nonassociated factors.
```
theorem equationIdealCycle_coefficient (F : TernaryPolynomial)
    (a : Associates TernaryPolynomial) :
    equationIdealCycle F (associatePrincipalIdeal a) = equationMultiplicity F a := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.equationMultiplicity_reconstruct line 133
Source documentation
The multiplicity vector reconstructs the original equation's associate class.
```
theorem equationMultiplicity_reconstruct (F : TernaryPolynomial) (hF : F ≠ 0) :
    (equationMultiplicity F).prod (fun a n => a ^ n) = Associates.mk F := by
…
```
Mentions: OAI.Nagata.Workers.W30.TernaryPolynomial
theorem OAI.Nagata.Workers.W30.nonzero_prime_eq_of_le_height_one line 154
Source documentation
There is no proper inclusion between a nonzero prime and a prime of height at most one.
```
theorem nonzero_prime_eq_of_le_height_one {I P : Ideal R} [I.IsPrime] [P.IsPrime]
    (hI : I ≠ ⊥) (hIP : I ≤ P) (hP : P.height ≤ 1) : I = P := by
…
```

theorem OAI.Nagata.Workers.W30.height_one_prime_generator line 169

Source documentation

A nonzero prime ideal of height at most one is the principal ideal of a prime element.

theorem height_one_prime_generator (P : Ideal R) [hPprime : P.IsPrime]
    (hP : P ≠ ⊥) (hheight : P.height ≤ 1) :
    ∃ f : R, Prime f ∧ P = Ideal.span {f} := by
…

lemma OAI.Nagata.Workers.W30.topHomogeneousComponent_ne_zero line 200
Source documentation
The top homogeneous component never vanishes for a nonzero polynomial.
```
lemma topHomogeneousComponent_ne_zero {p : MvPolynomial σ K} (hp : p ≠ 0) :
    homogeneousComponent p.totalDegree p ≠ 0 := by
…
```

lemma OAI.Nagata.Workers.W30.topHomogeneousComponent_mul line 213

Source documentation

Only the two top-degree components contribute to the top component of a product.

lemma topHomogeneousComponent_mul (p q : MvPolynomial σ K) :
    homogeneousComponent (p.totalDegree + q.totalDegree) (p*q) =
      homogeneousComponent p.totalDegree p * homogeneousComponent q.totalDegree q := by
…

lemma OAI.Nagata.Workers.W30.degree_pos_of_nonzero_nonunit line 252

theorem OAI.Nagata.Workers.W30.exists_homogeneous_irreducible_factors line 267

Source documentation

Every nonzero homogeneous polynomial is, up to a unit, a finite product of irreducible homogeneous polynomials. Repeated factors are retained in the multiset.

theorem exists_homogeneous_irreducible_factors (p : MvPolynomial σ K) {d : ℕ}
    (hp : p ≠ 0) (hhom : p.IsHomogeneous d) :
    ∃ L : Multiset (MvPolynomial σ K),
      (∀ P ∈ L, Irreducible P ∧ P.IsHomogeneous P.totalDegree) ∧ Associated L.prod p := by
…

lemma OAI.Nagata.Workers.W30.unit_polynomial_totalDegree line 326
lemma OAI.Nagata.Workers.W30.homogeneous_of_associated line 332

theorem OAI.Nagata.Workers.W30.factors_homogeneous line 340

Source documentation

All irreducible factors returned by the actual UFD factorization are homogeneous.

theorem factors_homogeneous {p : MvPolynomial σ K} {d : ℕ}
    (hp : p ≠ 0) (hhom : p.IsHomogeneous d) :
    ∀ f ∈ factors p, f.IsHomogeneous f.totalDegree := by
…

theorem OAI.Nagata.Workers.W30.homogeneous_prime_factor_in_ideal line 368

Source documentation

An actual nonzero homogeneous element of a prime ideal has an irreducible homogeneous factor in that ideal.

theorem homogeneous_prime_factor_in_ideal (P : Ideal (MvPolynomial σ K)) [hP : P.IsPrime]
    {x : MvPolynomial σ K} {d : ℕ} (hx : x ∈ P) (hx0 : x ≠ 0)
    (hhom : x.IsHomogeneous d) :
    ∃ f : MvPolynomial σ K, f ∈ P ∧ Irreducible f ∧ f.IsHomogeneous f.totalDegree := by
…

theorem OAI.Nagata.Workers.W30.homogeneous_height_one_prime_generator line 379

Source documentation

Every nonzero homogeneous prime ideal of height at most one is generated by an irreducible homogeneous polynomial of positive degree.

theorem homogeneous_height_one_prime_generator (P : Ideal (MvPolynomial σ K))
    [hP : P.IsPrime] (hP0 : P ≠ ⊥) (hheight : P.height ≤ 1)
    (hhom : P.IsHomogeneous (homogeneousSubmodule σ K)) :
    ∃ f : MvPolynomial σ K, Prime f ∧ f.IsHomogeneous f.totalDegree ∧
      0 < f.totalDegree ∧ P = Ideal.span {f} := by
…

lemma OAI.Nagata.Workers.W30.homogeneous_multiset_prod line 412

theorem OAI.Nagata.Workers.W30.homogeneous_of_dvd line 423

Source documentation

Every actual polynomial divisor of a nonzero homogeneous polynomial is homogeneous.

theorem homogeneous_of_dvd {p f : MvPolynomial σ K} {d : ℕ}
    (hp : p ≠ 0) (hhom : p.IsHomogeneous d) (hf : f ∣ p) :
    f.IsHomogeneous f.totalDegree := by
…

theorem OAI.Nagata.Workers.W30.homogeneous_of_span_homogeneous line 453

Source documentation

A homogeneous principal ideal has a homogeneous generator.

theorem homogeneous_of_span_homogeneous {f : MvPolynomial σ K} (hf : f ≠ 0)
    (hI : (Ideal.span ({f} : Set (MvPolynomial σ K))).IsHomogeneous
      (homogeneousSubmodule σ K)) : f.IsHomogeneous f.totalDegree := by
…

theorem OAI.Nagata.Workers.W30.span_homogeneous_of_homogeneous line 467

Source documentation

Conversely, a homogeneous equation generates a homogeneous ideal.

theorem span_homogeneous_of_homogeneous {f : MvPolynomial σ K} {d : ℕ}
    (hf : f.IsHomogeneous d) :
    (Ideal.span ({f} : Set (MvPolynomial σ K))).IsHomogeneous (homogeneousSubmodule σ K) := by
…

theorem OAI.Nagata.Workers.W30.span_homogeneous_iff line 476