LaurentWeightObstruction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Negative weights cannot occur in a nonnegatively generated subalgebra

We use Laurent polynomial coactions to express an integral weight. The argument applies directly inside an ambient algebra: no reflection of a quotient grading and no injectivity of a chosen polynomial presentation is required. In the determinant algebra, the subalgebra generated by a,d,u has only nonnegative fiber weights, whereas the last coefficient in the source rigidity argument would have weight -2.

def OAI.StableCoordinate.LaurentWeightObstruction.nonnegativePart line 32
Source documentation
Laurent polynomials with no negative powers, viewed as a k-subalgebra.
```
def nonnegativePart : Subalgebra k A[T;T⁻¹] :=
…
```
theorem OAI.StableCoordinate.LaurentWeightObstruction.single_mem_nonnegativePart line 36
Source documentation
A single nonnegative Laurent monomial is an ordinary polynomial.
```
theorem single_mem_nonnegativePart (n : ℤ) (hn : 0 ≤ n) (a : A) :
    AddMonoidAlgebra.single n a ∈ nonnegativePart (k := k) (A := A) := by
…
```
Mentions: OAI.StableCoordinate.LaurentWeightObstruction.nonnegativePart
theorem OAI.StableCoordinate.LaurentWeightObstruction.eq_zero_of_single_mem_nonnegativePart line 45
Source documentation
An ordinary polynomial cannot equal a nonzero Laurent monomial of strictly negative degree.
```
theorem eq_zero_of_single_mem_nonnegativePart {n : ℤ} (hn : n < 0) {a : A}
    (h : AddMonoidAlgebra.single n a ∈ nonnegativePart (k := k) (A := A)) :
…
```
Mentions: OAI.StableCoordinate.LaurentWeightObstruction.nonnegativePart
theorem OAI.StableCoordinate.LaurentWeightObstruction.adjoin_mem_nonnegativePart line 66
Source documentation
If every element of a generating set has nonnegative weights under an algebra homomorphism to Laurent polynomials, then its generated subalgebra does too.
```
theorem adjoin_mem_nonnegativePart
    (ρ : A →ₐ[k] A[T;T⁻¹]) {s : Set A}
    (hs : ∀ a ∈ s, ρ a ∈ nonnegativePart (k := k) (A := A))
…
```
Mentions: OAI.StableCoordinate.LaurentWeightObstruction.nonnegativePart
theorem OAI.StableCoordinate.LaurentWeightObstruction.eq_zero_of_adjoin_of_negative_weight line 78
Source documentation
The final weight obstruction in an arbitrary ambient algebra. ρ may be the weight coaction of a quotient algebra; no polynomial subalgebra injectivity is needed.
```
theorem eq_zero_of_adjoin_of_negative_weight
    (ρ : A →ₐ[k] A[T;T⁻¹]) {s : Set A}
    (hs : ∀ a ∈ s, ρ a ∈ nonnegativePart (k := k) (A := A))
…
```
Mentions: OAI.StableCoordinate.LaurentWeightObstruction.nonnegativePart
def OAI.StableCoordinate.LaurentWeightObstruction.weightedEval line 88
Source documentation
Evaluation with each variable tagged by its integral weight.
```
def weightedEval {σ : Type*} (w : σ → ℤ) (f : σ → A) :
    MvPolynomial σ k →ₐ[k] A[T;T⁻¹] :=
…
```
Mentions: OAI.StableCoordinate.f
theorem OAI.StableCoordinate.LaurentWeightObstruction.weightedEval_of_homogeneous line 94
Source documentation
A homogeneous polynomial evaluates to one Laurent monomial under the weighted evaluation homomorphism.
```
theorem weightedEval_of_homogeneous {σ : Type*} (w : σ → ℤ) (f : σ → A)
    {p : MvPolynomial σ k} {n : ℤ} (hp : p.IsWeightedHomogeneous w n) :
    weightedEval w f p = AddMonoidAlgebra.single n (MvPolynomial.aeval f p) := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.LaurentWeightObstruction.weightedEval
theorem OAI.StableCoordinate.LaurentWeightObstruction.coeff_weightedEval line 110
Source documentation
Coefficient extraction from weighted evaluation is evaluation of the corresponding weighted homogeneous component.
```
theorem coeff_weightedEval {σ : Type*} (w : σ → ℤ) (f : σ → A)
    (p : MvPolynomial σ k) (n : ℤ) :
    (weightedEval w f p).coeff n =
      MvPolynomial.aeval f (MvPolynomial.weightedHomogeneousComponent w n p) := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.LaurentWeightObstruction.weightedEval