AffineMultiplicity.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Affine maximal ideals, local rings, and multiplicity predicates

def OAI.Nagata.AffineMultiplicity.pointIdeal line 22
Source documentation
The ideal of polynomials vanishing at an affine point.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:42 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.pointIdeal@path.
```
noncomputable def pointIdeal (p : σ → K) : Ideal (MvPolynomial σ K) :=
…
```
def OAI.Nagata.AffineMultiplicity.orderAtLeast line 27
Source documentation
A polynomial vanishes to order at least m when it belongs to the mth power of the point's evaluation ideal.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:45 (different declaration text). Qualify references as OAI.Nagata.AffineMultiplicity.orderAtLeast@path.
```
def orderAtLeast (p : σ → K) (m : ℕ) (f : MvPolynomial σ K) : Prop :=
…
```
theorem OAI.Nagata.AffineMultiplicity.pointIdeal_mem_iff line 30
theorem OAI.Nagata.AffineMultiplicity.coordinate_difference_mem line 34
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_zero line 39
theorem OAI.Nagata.AffineMultiplicity.zero_orderAtLeast line 43
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_one_iff line 46
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_mono line 50
theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_add line 54

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_unit_mul_iff line 59

Source documentation

Multiplication by a polynomial unit does not change the order condition.

theorem orderAtLeast_unit_mul_iff (p : σ → K) (m : ℕ)
    (u : (MvPolynomial σ K)ˣ) (f : MvPolynomial σ K) :
    orderAtLeast p m ((u : MvPolynomial σ K) * f) ↔ orderAtLeast p m f :=
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_mul line 65

Source documentation

Multiplication adds lower bounds for affine vanishing order.

theorem orderAtLeast_mul {p : σ → K} {m n : ℕ} {f g : MvPolynomial σ K}
    (hf : orderAtLeast p m f) (hg : orderAtLeast p n g) :
    orderAtLeast p (m + n) (f * g) := by
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_pow line 73

Source documentation

Taking a power scales every affine multiplicity lower bound.

theorem orderAtLeast_pow {p : σ → K} {m : ℕ} {f : MvPolynomial σ K}
    (hf : orderAtLeast p m f) (N : ℕ) : orderAtLeast p (m * N) (f ^ N) := by
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_prod line 80

Source documentation

Product form used by the permutation reduction, with unequal bounds.

theorem orderAtLeast_prod {ι : Type*} (s : Finset ι) (p : σ → K)
    (m : ι → ℕ) (f : ι → MvPolynomial σ K)
    (h : ∀ i ∈ s, orderAtLeast p (m i) (f i)) :
    orderAtLeast p (∑ i ∈ s, m i) (∏ i ∈ s, f i) := by
…

theorem OAI.Nagata.AffineMultiplicity.pointIdeal_map_of_eval_compatible line 96

Source documentation

An isomorphism of polynomial coordinate rings carrying evaluation at q to evaluation at p carries the actual point ideal to the actual point ideal.

theorem pointIdeal_map_of_eval_compatible {τ : Type*}
    (p : σ → K) (q : τ → K)
    (e : MvPolynomial σ K ≃+* MvPolynomial τ K)
    (h : ∀ f, MvPolynomial.eval q (e f) = MvPolynomial.eval p f) :
    Ideal.map e (pointIdeal p) = pointIdeal q := by
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_equiv_iff line 114

Source documentation

Algebraic coordinate-ring isomorphisms preserve ideal-power multiplicity. The compatibility hypothesis concerns evaluation, not any order bound.

theorem orderAtLeast_equiv_iff {τ : Type*}
    (p : σ → K) (q : τ → K)
    (e : MvPolynomial σ K ≃+* MvPolynomial τ K)
    (h : ∀ f, MvPolynomial.eval q (e f) = MvPolynomial.eval p f)
    (m : ℕ) (f : MvPolynomial σ K) :
    orderAtLeast q m (e f) ↔ orderAtLeast p m f := by
…

theorem OAI.Nagata.AffineMultiplicity.pointIdeal_isMaximal line 129
Source documentation
Over a field, the ideal used by orderAtLeast really is maximal.
```
theorem pointIdeal_isMaximal (p : σ → F) : (pointIdeal p).IsMaximal := by
…
```
theorem OAI.Nagata.AffineMultiplicity.maximalIdeal_power_radical line 158
theorem OAI.Nagata.AffineMultiplicity.maximalIdeal_power_isPrimary line 162
theorem OAI.Nagata.AffineMultiplicity.maximalIdeal_power_mul_iff line 168
Source documentation
Elements outside a maximal ideal cancel from membership in every power.
```
theorem maximalIdeal_power_mul_iff (m : ℕ) (f g : R) (hg : g ∉ I) :
    g * f ∈ I ^ m ↔ f ∈ I ^ m := by
…
```
theorem OAI.Nagata.AffineMultiplicity.maximalIdeal_power_comap_map line 182

theorem OAI.Nagata.AffineMultiplicity.maximalIdeal_power_localization_iff line 196

Source documentation

Affine maximal-ideal power membership equals membership after passing to the actual local ring at that ideal.

theorem maximalIdeal_power_localization_iff
    [I.IsPrime] (S : Type*) [CommRing S] [Algebra R S]
    [IsLocalization.AtPrime S I] [IsLocalRing S] (m : ℕ) (f : R) :
    algebraMap R S f ∈ IsLocalRing.maximalIdeal S ^ m ↔ f ∈ I ^ m := by
…

theorem OAI.Nagata.AffineMultiplicity.orderAtLeast_nonvanishing_mul_iff line 212
Source documentation
Cancellation by an affine polynomial nonvanishing at the point. This applies in particular to the denominators on projective chart overlaps.
```
theorem orderAtLeast_nonvanishing_mul_iff (p : σ → F) (m : ℕ)
    (f g : MvPolynomial σ F) (hg : MvPolynomial.eval p g ≠ 0) :
    orderAtLeast p m (g * f) ↔ orderAtLeast p m f := by
…
```
instance OAI.Nagata.AffineMultiplicity.pointIdeal_isPrime line 219
abbrev OAI.Nagata.AffineMultiplicity.PointLocalRing line 223
Source documentation
The genuine local ring of affine space at the indicated rational point.
```
abbrev PointLocalRing (p : σ → F) := Localization.AtPrime (pointIdeal p)
```
def OAI.Nagata.AffineMultiplicity.residueEval line 227
Source documentation
Evaluation at the point extends to its actual local ring, because the allowed denominators have nonzero values in the coefficient field.
```
noncomputable def residueEval (p : σ → F) : PointLocalRing p →+* F :=
…
```
Mentions: OAI.Nagata.AffineMultiplicity.PointLocalRing
theorem OAI.Nagata.AffineMultiplicity.residueEval_algebraMap line 234
theorem OAI.Nagata.AffineMultiplicity.residueEval_surjective line 239
theorem OAI.Nagata.AffineMultiplicity.ker_residueEval line 245
Source documentation
The kernel of residue evaluation is the actual local maximal ideal.
```
theorem ker_residueEval (p : σ → F) :
    RingHom.ker (residueEval p) = IsLocalRing.maximalIdeal (PointLocalRing p) :=
…
```
Mentions: OAI.Nagata.AffineMultiplicity.residueEval, OAI.Nagata.AffineMultiplicity.PointLocalRing
theorem OAI.Nagata.AffineMultiplicity.residueEval_isUnit line 249
def OAI.Nagata.AffineMultiplicity.localOrderAtLeast line 257
Source documentation
Multiplicity in the actual local ring uses its maximal ideal.
```
def localOrderAtLeast (p : σ → F) (m : ℕ) (f : MvPolynomial σ F) : Prop :=
…
```
theorem OAI.Nagata.AffineMultiplicity.localOrderAtLeast_iff line 263
Source documentation
The affine ideal-power definition is faithfully identified with local maximal-ideal power membership; no extra geometric assumption is used.
```
theorem localOrderAtLeast_iff (p : σ → F) (m : ℕ) (f : MvPolynomial σ F) :
    localOrderAtLeast p m f ↔ orderAtLeast p m f :=
…
```
Mentions: OAI.Nagata.AffineMultiplicity.localOrderAtLeast

theorem OAI.Nagata.AffineMultiplicity.local_fraction_order_iff line 270

Source documentation

A fraction with a denominator invertible at the point has the same local order lower bounds as its numerator.

theorem local_fraction_order_iff (p : σ → F) (m : ℕ)
    (f : MvPolynomial σ F) (s : (pointIdeal p).primeCompl) :
    IsLocalization.mk' (PointLocalRing p) f s ∈
      IsLocalRing.maximalIdeal (PointLocalRing p) ^ m ↔ orderAtLeast p m f := by
…

Mentions: OAI.Nagata.AffineMultiplicity.PointLocalRing