SourceLocalizedDerivation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Homogeneity through the source's actual Laurent presentation

The integer grading on G is the quotient grading with generator weights (-1,0,0,1,1). The canonical map into the Laurent algebra over the quadric ring sends degree n to the single Laurent exponent -n. In particular, a homogeneous derivation of degree m, when intertwined with a derivation on that Laurent algebra, satisfies the precise homogeneity hypothesis of LaurentDescent with exponent -m.

def OAI.StableCoordinate.SourceLocalizedDerivation.generatorCoefficients line 30
Source documentation
The coefficient part of the five canonical Laurent generator images.
```
def generatorCoefficients : Fin 5 → B k :=
…
```
theorem OAI.StableCoordinate.SourceLocalizedDerivation.toLaurentBase_generator line 34
Source documentation
The canonical generator images have exactly the assigned integer weights.
```
theorem toLaurentBase_generator (i : Fin 5) :
    LaurentPresentation.toLaurentBase k (gX k i) =
      LaurentPolynomial.C (generatorCoefficients k i) *
        LaurentPolynomial.T (-presentationWeight i) := by
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.toLaurentBase, OAI.StableCoordinate.SourceLocalizedDerivation.generatorCoefficients
theorem OAI.StableCoordinate.SourceLocalizedDerivation.toLaurentBase_mk_homogeneous line 42
Source documentation
A homogeneous representative maps to its expected Laurent monomial.
```
theorem toLaurentBase_mk_homogeneous {p : P k 5} {n : ℤ}
    (hp : p.IsWeightedHomogeneous presentationWeight n) :
    LaurentPresentation.toLaurentBase k (Ideal.Quotient.mk (idealG k) p) =
      LaurentPolynomial.C (aeval (generatorCoefficients k) p) *
        LaurentPolynomial.T (-n) := by
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.toLaurentBase, OAI.StableCoordinate.SourceLocalizedDerivation.generatorCoefficients
theorem OAI.StableCoordinate.SourceLocalizedDerivation.toLaurentBase_coeff_eq_zero line 52
Source documentation
The image of every homogeneous element has support at one Laurent exponent.
```
theorem toLaurentBase_coeff_eq_zero {r : G k} {n : ℤ}
    (hr : r ∈ gPiece k n) (j : ℤ) (hj : j ≠ -n) :
    (LaurentPresentation.toLaurentBase k r).coeff j = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.toLaurentBase

theorem OAI.StableCoordinate.SourceLocalizedDerivation.toLaurentBase_homogeneous line 61

Source documentation

The singleton-support statement in the exact normalization used by descent.

theorem toLaurentBase_homogeneous {r : G k} {n : ℤ}
    (hr : r ∈ gPiece k n) :
    LaurentPresentation.toLaurentBase k r =
      LaurentPolynomial.C ((LaurentPresentation.toLaurentBase k r).coeff (-n)) *
        LaurentPolynomial.T (-n) := by
…

Mentions: OAI.StableCoordinate.LaurentPresentation.toLaurentBase

theorem OAI.StableCoordinate.SourceLocalizedDerivation.baseMap_eq_baseToDegeneration line 74
Source documentation
The two constructions of the canonical quadric map agree.
```
theorem baseMap_eq_baseToDegeneration :
    LaurentPresentation.baseMap k = baseToDegeneration k := by
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.baseMap
theorem OAI.StableCoordinate.SourceLocalizedDerivation.baseMap_mem_piece line 84
Source documentation
The existing Laurent-presentation base map has degree-zero image.
```
theorem baseMap_mem_piece (b : B k) :
    LaurentPresentation.baseMap k b ∈ gPiece k 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.baseMap

theorem OAI.StableCoordinate.SourceLocalizedDerivation.homogeneousOnConstants_of_intertwining line 92

Source documentation

Actual homogeneous-degree transport gives the hypothesis of Laurent descent. The intertwining identity is supplied by the invariant-localization construction.

theorem homogeneousOnConstants_of_intertwining
    (D : Derivation k (G k) (G k))
    (δ : Derivation k (LaurentPresentation.Laurent k) (LaurentPresentation.Laurent k))
    (m : ℤ)
    (hD : ∀ (n : ℤ) (r : G k), r ∈ gPiece k n → D r ∈ gPiece k (n + m))
    (hintertwine : ∀ r : G k,
      δ (LaurentPresentation.toLaurentBase k r) = LaurentPresentation.toLaurentBase k (D r)) :
    LaurentDescent.HomogeneousOnConstants δ (-m) := by
…

Mentions: OAI.StableCoordinate.LaurentPresentation.Laurent, OAI.StableCoordinate.LaurentPresentation.toLaurentBase, OAI.StableCoordinate.LaurentDescent.HomogeneousOnConstants