FrameNormalization.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Normalizing a polynomial determinant frame

A choice of trivialization gives a frame above the desired quadric base, but its specialization need not be the prescribed initial frame. A constant unit rescaling corrects it. This construction needs no domain or reducedness hypothesis; those hypotheses enter only the separate uniqueness theorem.

def OAI.StableCoordinate.FrameLift.Frame.scale line 20
Source documentation
Fiber scaling: the positive-weight column is multiplied by a unit and the negative-weight row by its inverse.
```
def Frame.scale (F : Frame R) (u : Rˣ) : Frame R where
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.FrameLift.Frame.scale_one line 33
theorem OAI.StableCoordinate.FrameLift.Frame.scale_mul line 37
theorem OAI.StableCoordinate.FrameLift.Frame.scale_sameBase line 42
Source documentation
Scaling acts within a fiber of the map to the quadric.
```
theorem Frame.scale_sameBase (F : Frame R) (u : Rˣ) : SameBase (F.scale u) F := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase
theorem OAI.StableCoordinate.FrameLift.Frame.map_scale line 60
theorem OAI.StableCoordinate.FrameLift.scale_comparison line 65
Source documentation
The comparison unit sends the first frame exactly to the second.
```
theorem scale_comparison {F G : Frame R} (h : SameBase F G) :
    F.scale (comparisonUnit h) = G := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.comparisonUnit
theorem OAI.StableCoordinate.FrameLift.sameBase_trans line 74
Source documentation
Transitivity of equality of the three base coordinates.
```
theorem sameBase_trans {F G H : Frame R} (hFG : SameBase F G) (hGH : SameBase G H) :
    SameBase F H :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase
def OAI.StableCoordinate.FrameLift.normalizeFrame line 86
Source documentation
Correct an arbitrary polynomial lift to the prescribed initial frame by a constant, invertible fiber scaling.
```
noncomputable def normalizeFrame (F : Frame (MvPolynomial σ R)) (G : Frame R)
    (h : SameBase (F.map constantCoeff) G) : Frame (MvPolynomial σ R) :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase
theorem OAI.StableCoordinate.FrameLift.normalizeFrame_sameBase line 91
Source documentation
Normalization leaves all three base-coordinate polynomials unchanged.
```
theorem normalizeFrame_sameBase (F : Frame (MvPolynomial σ R)) (G : Frame R)
    (h : SameBase (F.map constantCoeff) G) : SameBase (normalizeFrame F G h) F :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.normalizeFrame
theorem OAI.StableCoordinate.FrameLift.normalizeFrame_at_zero line 97
Source documentation
The normalized polynomial lift has exactly the specified initial frame.
```
theorem normalizeFrame_at_zero (F : Frame (MvPolynomial σ R)) (G : Frame R)
    (h : SameBase (F.map constantCoeff) G) :
    (normalizeFrame F G h).map constantCoeff = G := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.normalizeFrame
theorem OAI.StableCoordinate.FrameLift.normalizeFrame_unique line 109
Source documentation
Normalization is canonical over a reduced ring.
```
theorem normalizeFrame_unique [IsReduced R]
    (F : Frame (MvPolynomial σ R)) (G : Frame R)
    (h : SameBase (F.map constantCoeff) G)
    (F' : Frame (MvPolynomial σ R)) (hbase : SameBase F' F)
    (hzero : F'.map constantCoeff = G) : F' = normalizeFrame F G h := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.normalizeFrame
theorem OAI.StableCoordinate.FrameLift.Frame.specialize_map line 121
Source documentation
Coefficient specialization commutes with a coefficient-ring homomorphism.
```
theorem Frame.specialize_map (F : Frame (MvPolynomial σ R)) (θ : R →+* S) :
    (F.map (MvPolynomial.map θ)).map constantCoeff =
      (F.map constantCoeff).map θ := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame.map
theorem OAI.StableCoordinate.FrameLift.normalized_lift_scaling_equivariance line 132
Source documentation
A normalized lift automatically commutes with a fiber scaling whenever its base-coordinate polynomials are unchanged by that scaling.
For the source's multiplicative fiber action, apply this over the coefficient ring containing an invertible scaling parameter. The hypothesis on base coordinates is checked on the embedded quadric algebra.
```
theorem normalized_lift_scaling_equivariance [IsReduced R]
    (F : Frame (MvPolynomial σ R)) (F₀ : Frame R)
    (hzero : F.map constantCoeff = F₀)
    (θ : R →+* R) (u : Rˣ)
    (href : F₀.map θ = F₀.scale u)
    (hbase : SameBase (F.map (MvPolynomial.map θ)) F) :
    F.map (MvPolynomial.map θ) =
      F.scale (Units.map (C : R →+* MvPolynomial σ R).toMonoidHom u) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.SameBase