NormalizedDeterminantLift.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Constructing the normalized polynomial lift on the determinant ring

For every actual polynomial additive action on the exact quadric ring B, this file constructs a polynomial family of algebra maps on the exact C = k[a,d,b,c,u]/(ac-bd-1). Its restriction is the given action on B, and its parameter-zero specialization is the identity on all of C.

Existence uses the proved UFD structure on C[T], the concrete gcd frame factorization, and normalization by a constant comparison unit. No line bundle, arbitrary frame, or lift-existence premise is assumed. The additive group law for this normalized family is proved separately by frame uniqueness.

def OAI.StableCoordinate.NormalizedDeterminantLift.pulledBase line 33
Source documentation
Pull the base action back along the actual quadric-to-determinant-ring map.
```
def pulledBase (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    Obstruction.B k →ₐ[k] Polynomial (Obstruction.C k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.NormalizedDeterminantLift.pulledBase_apply line 37
theorem OAI.StableCoordinate.NormalizedDeterminantLift.pulledBase_at_zero line 41
theorem OAI.StableCoordinate.NormalizedDeterminantLift.pulledBase_relation line 49
Source documentation
The polynomial base coordinates satisfy the quadric equation identically.
```
theorem pulledBase_relation (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    pulledBase α (bX k 0) * pulledBase α (bX k 1) =
      pulledBase α (bX k 2) * (pulledBase α (bX k 2) + 1) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.NormalizedDeterminantLift.pulledBase
def OAI.StableCoordinate.NormalizedDeterminantLift.rawFrame line 56
Source documentation
A genuine polynomial determinant frame exists by unique factorization.
```
def rawFrame (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    Frame (Polynomial (Obstruction.C k)) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.NormalizedDeterminantLift.rawFrame_ab line 61
theorem OAI.StableCoordinate.NormalizedDeterminantLift.rawFrame_dc line 65
theorem OAI.StableCoordinate.NormalizedDeterminantLift.rawFrame_db line 69
theorem OAI.StableCoordinate.NormalizedDeterminantLift.rawFrame_at_zero_sameBase line 74
Source documentation
At parameter zero the raw frame and the original frame have the same base.
```
theorem rawFrame_at_zero_sameBase (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    SameBase ((rawFrame α).map Polynomial.constantCoeff) (sourceFrame k) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.NormalizedDeterminantLift.rawFrame
def OAI.StableCoordinate.NormalizedDeterminantLift.normalizedFrame line 92
Source documentation
The chosen polynomial frame has exactly the original frame at parameter zero.
```
def normalizedFrame (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    Frame (Polynomial (Obstruction.C k)) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.NormalizedDeterminantLift.normalizedFrame_sameBase line 96
theorem OAI.StableCoordinate.NormalizedDeterminantLift.normalizedFrame_at_zero line 100
theorem OAI.StableCoordinate.NormalizedDeterminantLift.normalizedFrame_ab line 104
theorem OAI.StableCoordinate.NormalizedDeterminantLift.normalizedFrame_dc line 108
theorem OAI.StableCoordinate.NormalizedDeterminantLift.normalizedFrame_db line 112
def OAI.StableCoordinate.NormalizedDeterminantLift.liftHom line 118
Source documentation
The actual normalized polynomial-family homomorphism on the determinant ring. The independent u coordinate is lifted through the same base action.
```
def liftHom (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    Obstruction.C k →ₐ[k] Polynomial (Obstruction.C k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.NormalizedDeterminantLift.liftHom_comp_baseMap line 123
Source documentation
The family restricts to the original base action on the whole base algebra.
```
theorem liftHom_comp_baseMap (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    (liftHom α).comp (sourceBaseMap k) = pulledBase α :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.NormalizedDeterminantLift.liftHom, OAI.StableCoordinate.NormalizedDeterminantLift.pulledBase
theorem OAI.StableCoordinate.NormalizedDeterminantLift.liftHom_baseMap line 129
Source documentation
Pointwise form of the exact base-extension identity.
```
theorem liftHom_baseMap (α : PolynomialAdditiveAction k (Obstruction.B k))
    (b : Obstruction.B k) :
    liftHom α (sourceBaseMap k b) = (α.toAlgHom b).map (sourceBaseMap k).toRingHom :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.NormalizedDeterminantLift.liftHom
def OAI.StableCoordinate.NormalizedDeterminantLift.atZero line 135
Source documentation
Zero-parameter specialization, bundled as a coefficient-algebra homomorphism.
```
def atZero : Polynomial (Obstruction.C k) →ₐ[k] Obstruction.C k where
…
```
Mentions: OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.NormalizedDeterminantLift.atZero_comp_liftHom line 140
Source documentation
The normalization is an equality of actual algebra maps, not just of points.
```
theorem atZero_comp_liftHom (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    atZero.comp (liftHom α) = AlgHom.id k (Obstruction.C k) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.NormalizedDeterminantLift.liftHom, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.NormalizedDeterminantLift.liftHom_identity line 150
Source documentation
The lifted polynomial family is normalized on every element of C.
```
@[simp] theorem liftHom_identity (α : PolynomialAdditiveAction k (Obstruction.B k))
    (c : Obstruction.C k) : (liftHom α c).coeff 0 = c :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.NormalizedDeterminantLift.liftHom

theorem OAI.StableCoordinate.NormalizedDeterminantLift.exists_normalized_lift line 155

Source documentation

Unconditional existence of a normalized polynomial lift over the exact rings.

theorem exists_normalized_lift (α : PolynomialAdditiveAction k (Obstruction.B k)) :
    ∃ β : Obstruction.C k →ₐ[k] Polynomial (Obstruction.C k),
      (∀ c, (β c).coeff 0 = c) ∧
      (∀ b, β (sourceBaseMap k b) = (α.toAlgHom b).map (sourceBaseMap k).toRingHom) :=
…

Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C