ModificationPieces.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous pieces of an affine modification

For an ideal I of R, this file identifies the Laurent subalgebra R[T, I/T] with the Laurent polynomials whose coefficient at exponent n belongs to I ^ max (-n) 0. The grading in the source is opposite to the Laurent exponent, so its positive degree-ℓ piece is T^(-ℓ) I^ℓ.

def OAI.StableCoordinate.ModificationPieces.extendedRees line 25
Source documentation
The coefficient realization of the extended Rees algebra R[T,I/T].
```
def extendedRees (I : Ideal R) : Subalgebra R R[T;T⁻¹] where
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ModificationPieces.mem_extendedRees_iff line 62
theorem OAI.StableCoordinate.ModificationPieces.single_mem_extendedRees_iff line 66
def OAI.StableCoordinate.ModificationPieces.modification line 79
Source documentation
The Laurent subalgebra generated by T and r/T for r ∈ I.
```
def modification (I : Ideal R) : Subalgebra R R[T;T⁻¹] :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ModificationPieces.T_one_mem_modification line 83
theorem OAI.StableCoordinate.ModificationPieces.numerator_mem_modification line 87
theorem OAI.StableCoordinate.ModificationPieces.modification_le_extendedRees line 91
theorem OAI.StableCoordinate.ModificationPieces.negative_single_mem_modification line 104
theorem OAI.StableCoordinate.ModificationPieces.nonnegative_single_mem_modification line 125
theorem OAI.StableCoordinate.ModificationPieces.single_mem_modification_of_mem_power line 133
theorem OAI.StableCoordinate.ModificationPieces.modification_eq_extendedRees line 143
Source documentation
The generator and coefficient definitions of the extended Rees algebra coincide.
```
theorem modification_eq_extendedRees (I : Ideal R) :
    modification I = extendedRees I := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification, OAI.StableCoordinate.ModificationPieces.extendedRees
theorem OAI.StableCoordinate.ModificationPieces.single_mem_modification_iff line 154
Source documentation
Exact Laurent monomial membership.
```
theorem single_mem_modification_iff (I : Ideal R) (n : ℤ) (r : R) :
    AddMonoidAlgebra.single n r ∈ modification I ↔ r ∈ I ^ (-n).toNat := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification
theorem OAI.StableCoordinate.ModificationPieces.positive_piece line 159
Source documentation
The source's degree-ℓ piece, using deg T = -1.
```
theorem positive_piece (I : Ideal R) (ℓ : ℕ) (r : R) :
    C r * T (-(ℓ : ℤ)) ∈ modification I ↔ r ∈ I ^ ℓ := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification
theorem OAI.StableCoordinate.ModificationPieces.coefficient_mem_power line 166
Source documentation
Every negative-exponent coefficient of a modification element lies in the corresponding power of the center ideal.
```
theorem coefficient_mem_power {I : Ideal R} {p : R[T;T⁻¹]}
    (hp : p ∈ modification I) (ℓ : ℕ) :
    p.coeff (-(ℓ : ℤ)) ∈ I ^ ℓ := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification
def OAI.StableCoordinate.ModificationPieces.numeratorIdeal line 173
Source documentation
Numerators whose division by T lies in a specified Laurent subalgebra.
```
def numeratorIdeal (S : Subalgebra R R[T;T⁻¹]) : Ideal R where
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.ModificationPieces.generatedModification line 185
Source documentation
A presentation by an arbitrary chosen set of generators of the center.
```
def generatedModification (s : Set R) : Subalgebra R R[T;T⁻¹] :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ModificationPieces.modification_span_eq line 190
Source documentation
Passing from ideal generators to every numerator in the ideal does not change the generated Laurent subalgebra.
```
theorem modification_span_eq (s : Set R) :
    modification (Ideal.span s) = generatedModification s := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification, OAI.StableCoordinate.ModificationPieces.generatedModification
theorem OAI.StableCoordinate.ModificationPieces.modification_pair_eq line 208
Source documentation
The exact two-generator presentation used for the distinguished ideal I=(f₀,g₀).
```
theorem modification_pair_eq (f g : R) :
    modification (Ideal.span ({f, g} : Set R)) =
      Algebra.adjoin R ({T 1, C f * T (-1), C g * T (-1)} : Set R[T;T⁻¹]) := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification
def OAI.StableCoordinate.ModificationPieces.Homogeneous line 215
Source documentation
Laurent homogeneity for the source convention deg T = -1.
```
def Homogeneous (ℓ : ℤ) (p : R[T;T⁻¹]) : Prop :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ModificationPieces.eq_single_of_homogeneous line 218
theorem OAI.StableCoordinate.ModificationPieces.homogeneous_single line 230
theorem OAI.StableCoordinate.ModificationPieces.homogeneous_zero line 235
theorem OAI.StableCoordinate.ModificationPieces.homogeneous_C line 239
theorem OAI.StableCoordinate.ModificationPieces.Homogeneous.add line 244
theorem OAI.StableCoordinate.ModificationPieces.Homogeneous.mul line 249
theorem OAI.StableCoordinate.ModificationPieces.Homogeneous.pow line 255
theorem OAI.StableCoordinate.ModificationPieces.Homogeneous.sum line 263
theorem OAI.StableCoordinate.ModificationPieces.Homogeneous.prod line 273
theorem OAI.StableCoordinate.ModificationPieces.homogeneous_aeval line 288
Source documentation
Weighted polynomial evaluation preserves the source-to-Laurent grading whenever the images of the independent variables have the specified weights.
```
theorem homogeneous_aeval {k σ : Type*} [CommRing k] [Algebra k R]
    (w : σ → ℤ) (v : σ → R[T;T⁻¹]) (hv : ∀ i, Homogeneous (w i) (v i))
    {p : MvPolynomial σ k} {d : ℤ} (hp : p.IsWeightedHomogeneous w d) :
    Homogeneous d (MvPolynomial.aeval v p) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.Homogeneous
theorem OAI.StableCoordinate.ModificationPieces.homogeneous_numerator line 307
Source documentation
Every homogeneous positive-degree element has a numerator from the exact power of the center ideal.
```
theorem homogeneous_numerator {I : Ideal R} {ℓ : ℕ} {p : R[T;T⁻¹]}
    (hp : p ∈ modification I) (hh : Homogeneous (ℓ : ℤ) p) :
    ∃ r ∈ I ^ ℓ, p = C r * T (-(ℓ : ℤ)) :=
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification, OAI.StableCoordinate.ModificationPieces.Homogeneous
theorem OAI.StableCoordinate.ModificationPieces.homogeneous_nonzero_numerator line 314
Source documentation
The nonzero-numerator form consumed by the coordinate obstruction.
```
theorem homogeneous_nonzero_numerator {I : Ideal R} {ℓ : ℕ} {p : R[T;T⁻¹]}
    (hp : p ∈ modification I) (hh : Homogeneous (ℓ : ℤ) p) (hne : p ≠ 0) :
    ∃ r ∈ I ^ ℓ, r ≠ 0 ∧ p = C r * T (-(ℓ : ℤ)) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification, OAI.StableCoordinate.ModificationPieces.Homogeneous
theorem OAI.StableCoordinate.ModificationPieces.positive_nonzero_numerator line 324
Source documentation
In strictly positive degree the numerator lies in the center ideal itself.
```
theorem positive_nonzero_numerator {I : Ideal R} {ℓ : ℕ} {p : R[T;T⁻¹]}
    (hℓ : 0 < ℓ) (hp : p ∈ modification I)
    (hh : Homogeneous (ℓ : ℤ) p) (hne : p ≠ 0) :
    ∃ r ∈ I, r ≠ 0 ∧ p = C r * T (-(ℓ : ℤ)) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.ModificationPieces.modification, OAI.StableCoordinate.ModificationPieces.Homogeneous