DeterminantLiftWeights.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Fiber-weight compatibility of normalized lifts on the determinant quotient

This specializes normalized-frame uniqueness to the actual source rings and the actual Laurent fiber coaction. A normalized polynomial lift extending a base polynomial family has the exact fiber weights coefficient by coefficient; no fiber-linearity or equivariance is assumed of the chosen lift.

def OAI.StableCoordinate.DeterminantLiftWeights.sourceFrame line 34
Source documentation
The original determinant frame on SL₂ × A¹.
```
def sourceFrame : Frame (C k) where
…
```
def OAI.StableCoordinate.DeterminantLiftWeights.parameterUnit line 42
Source documentation
The invertible Laurent parameter of fiber scaling.
```
def parameterUnit : (LaurentPolynomial (C k))ˣ where
…
```
def OAI.StableCoordinate.DeterminantLiftWeights.constants line 49
Source documentation
Constant Laurent polynomials as a base-algebra map.
```
def constants : C k →ₐ[k] LaurentPolynomial (C k) where
…
```
theorem OAI.StableCoordinate.DeterminantLiftWeights.constants_apply line 53
abbrev OAI.StableCoordinate.DeterminantLiftWeights.quadricMap line 56
Source documentation
The actual base-quadric inclusion; definitions agree with the chart API.
```
abbrev quadricMap : BundleCharts.QuadricRing k →ₐ[k] C k := BundleCharts.baseMap k
```
Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.baseMap
theorem OAI.StableCoordinate.DeterminantLiftWeights.sourceFrame_scales line 59
Source documentation
The original source frame has the prescribed scaling, with no assumption.
```
theorem sourceFrame_scales :
    (sourceFrame k).map (fiberCoaction k).toRingHom =
      Frame.scale (R := LaurentPolynomial (C k))
…
```
Mentions: OAI.StableCoordinate.DeterminantLiftWeights.sourceFrame, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.DeterminantLiftWeights.fiberCoaction_quadricMap line 78
Source documentation
The base-quadric subalgebra is fixed by the fiber coaction.
```
theorem fiberCoaction_quadricMap :
    (fiberCoaction k).comp (quadricMap k) = (constants k).comp (quadricMap k) := by
…
```
Mentions: OAI.StableCoordinate.DeterminantLiftWeights.quadricMap, OAI.StableCoordinate.DeterminantLiftWeights.constants

theorem OAI.StableCoordinate.DeterminantLiftWeights.normalized_lift_scaling line 101

Source documentation

A normalized polynomial frame above three base polynomial functions is fiber-equivariant in the source's actual determinant ring.

theorem normalized_lift_scaling
    (F : Frame (C k)[X]) (x y z : (BundleCharts.QuadricRing k)[X])
    (hx : F.a * F.b = x.map (quadricMap k).toRingHom)
    (hy : F.d * F.c = y.map (quadricMap k).toRingHom)
    (hz : F.d * F.b = z.map (quadricMap k).toRingHom)
    (hnormal : F.map Polynomial.constantCoeff = sourceFrame k) :
    F.map (Polynomial.mapRingHom (fiberCoaction k).toRingHom) =
      Frame.scale (R := (LaurentPolynomial (C k))[X])
…

Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.DeterminantLiftWeights.quadricMap, OAI.StableCoordinate.DeterminantLiftWeights.sourceFrame, OAI.StableCoordinate.R

theorem OAI.StableCoordinate.DeterminantLiftWeights.normalized_lift_coefficient_weights line 121

Source documentation

Every coefficient of the positive/negative frame coordinates has its prescribed fiber weight. In particular the infinitesimal coefficients have weights 1,1,-1,-1; no weight hypothesis has been placed on the lift itself.

theorem normalized_lift_coefficient_weights
    (F : Frame (C k)[X]) (x y z : (BundleCharts.QuadricRing k)[X])
    (hx : F.a * F.b = x.map (quadricMap k).toRingHom)
    (hy : F.d * F.c = y.map (quadricMap k).toRingHom)
    (hz : F.d * F.b = z.map (quadricMap k).toRingHom)
    (hnormal : F.map Polynomial.constantCoeff = sourceFrame k) (n : ℕ) :
    fiberCoaction k (F.a.coeff n) = AddMonoidAlgebra.single 1 (F.a.coeff n) ∧
    fiberCoaction k (F.d.coeff n) = AddMonoidAlgebra.single 1 (F.d.coeff n) ∧
    fiberCoaction k (F.b.coeff n) = AddMonoidAlgebra.single (-1) (F.b.coeff n) ∧
    fiberCoaction k (F.c.coeff n) = AddMonoidAlgebra.single (-1) (F.c.coeff n) := by
…

Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.DeterminantLiftWeights.quadricMap, OAI.StableCoordinate.DeterminantLiftWeights.sourceFrame

theorem OAI.StableCoordinate.DeterminantLiftWeights.base_polynomial_coefficient_fixed line 146
Source documentation
Every polynomial coefficient pulled back from the base quadric is fixed by fiber scaling.
```
theorem base_polynomial_coefficient_fixed (p : (BundleCharts.QuadricRing k)[X]) (n : ℕ) :
    fiberCoaction k ((p.map (quadricMap k).toRingHom).coeff n) =
      AddMonoidAlgebra.single 0 ((p.map (quadricMap k).toRingHom).coeff n) := by
…
```
Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.DeterminantLiftWeights.quadricMap
theorem OAI.StableCoordinate.DeterminantLiftWeights.generator_coefficient_weights_of_normalized_lift line 159
Source documentation
An arbitrary normalized polynomial lift of a base polynomial family has exactly the five source fiber weights, coefficient by coefficient. In particular no linearity, group law, or equivariance is assumed of the lift.
```
theorem generator_coefficient_weights_of_normalized_lift
    (φ : C k →ₐ[k] (C k)[X])
    (β : BundleCharts.QuadricRing k →ₐ[k] (BundleCharts.QuadricRing k)[X])
    (hext : ∀ p, φ (quadricMap k p) = (β p).map (quadricMap k).toRingHom)
    (hidentity : ∀ q, (φ q).coeff 0 = q) (i : Fin 5) (n : ℕ) :
    fiberCoaction k ((φ (generator k i)).coeff n) =
      AddMonoidAlgebra.single (Obstruction.fiberWeight i) ((φ (generator k i)).coeff n) := by
…
```
Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.DeterminantLiftWeights.quadricMap, OAI.StableCoordinate.Obstruction.fiberWeight