PolynomialFrameNormalization.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Ordinary-polynomial adapters for normalized determinant lifts

The additive-coaction interface uses ordinary and iterated Polynomial, while multivariate frames are convenient for the underlying unit rigidity argument. These adapters give the same normalization and uniqueness directly for the coaction parameter type, without changing variables through an equivalence.

theorem OAI.StableCoordinate.FrameLift.sameBase_map_aux line 20
Source documentation
Equality of base coordinates is preserved under every ring homomorphism.
```
private theorem sameBase_map_aux {F G : Frame R} (h : SameBase F G) (f : R →+* S) :
    SameBase (F.map f) (G.map f) := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.f
theorem OAI.StableCoordinate.FrameLift.univariate_unit_eq_C_constantCoeff line 28
Source documentation
Units of an ordinary polynomial ring over a reduced ring are constant.
```
theorem univariate_unit_eq_C_constantCoeff [IsReduced R]
    {p : Polynomial R} (hp : IsUnit p) :
    p = Polynomial.C (Polynomial.constantCoeff p) := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.FrameLift.polynomial_isReduced line 38
Source documentation
Reducedness passes to ordinary polynomial rings.
```
theorem polynomial_isReduced [IsReduced R] : IsReduced (Polynomial R) := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.FrameLift.normalized_bivariate_unique line 47
Source documentation
Iterated-polynomial version: normalization at the two-parameter origin is enough for the additive coaction group-law comparison.
```
theorem normalized_bivariate_unique [IsReduced R]
    {F G : Frame (Polynomial (Polynomial R))} (h : SameBase F G)
    (hzero : (F.map Polynomial.constantCoeff).map Polynomial.constantCoeff =
      (G.map Polynomial.constantCoeff).map Polynomial.constantCoeff) : F = G := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.SameBase
def OAI.StableCoordinate.FrameLift.normalizePolynomialFrame line 56
Source documentation
Normalize an ordinary-polynomial frame to a prescribed initial frame.
```
noncomputable def normalizePolynomialFrame (F : Frame (Polynomial R)) (G : Frame R)
    (h : SameBase (F.map Polynomial.constantCoeff) G) : Frame (Polynomial R) :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase
theorem OAI.StableCoordinate.FrameLift.normalizePolynomialFrame_sameBase line 61
Source documentation
Ordinary-polynomial normalization does not change the base-coordinate family.
```
theorem normalizePolynomialFrame_sameBase (F : Frame (Polynomial R)) (G : Frame R)
    (h : SameBase (F.map Polynomial.constantCoeff) G) :
    SameBase (normalizePolynomialFrame F G h) F :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.normalizePolynomialFrame
theorem OAI.StableCoordinate.FrameLift.normalizePolynomialFrame_at_zero line 68
Source documentation
The normalized ordinary-polynomial frame starts at exactly the chosen frame.
```
theorem normalizePolynomialFrame_at_zero (F : Frame (Polynomial R)) (G : Frame R)
    (h : SameBase (F.map Polynomial.constantCoeff) G) :
    (normalizePolynomialFrame F G h).map Polynomial.constantCoeff = G := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.normalizePolynomialFrame
theorem OAI.StableCoordinate.FrameLift.Frame.specializePolynomial_map line 80
Source documentation
Ordinary-polynomial coefficient specialization commutes with a ring map.
```
theorem Frame.specializePolynomial_map (F : Frame (Polynomial R)) (θ : R →+* S) :
    (F.map (Polynomial.mapRingHom θ)).map Polynomial.constantCoeff =
      (F.map Polynomial.constantCoeff).map θ := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame.map

theorem OAI.StableCoordinate.FrameLift.normalized_univariate_lift_scaling_equivariance line 86

Source documentation

Ordinary-polynomial covariance under a normalized fiber scaling.

theorem normalized_univariate_lift_scaling_equivariance [IsReduced R]
    (F : Frame (Polynomial R)) (F₀ : Frame R)
    (hzero : F.map Polynomial.constantCoeff = F₀)
    (θ : R →+* R) (u : Rˣ)
    (href : F₀.map θ = F₀.scale u)
    (hbase : SameBase (F.map (Polynomial.mapRingHom θ)) F) :
    F.map (Polynomial.mapRingHom θ) =
      F.scale (Units.map (Polynomial.C : R →+* Polynomial R).toMonoidHom u) := by
…

Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.SameBase