FrameScaling.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Fiber scaling of normalized polynomial determinant frames

A normalized polynomial lift over the quadric is automatically equivariant for fiber scaling. The proof compares the scaled and coefficientwise-transformed frames over the Laurent coefficient ring; both have the same base and the same zero-parameter frame. Unit rigidity gives equality. No linearity assumption on the chosen lift is smuggled into the statement.

theorem OAI.StableCoordinate.FrameLift.Frame.map_map line 24
theorem OAI.StableCoordinate.FrameLift.sameBase_scale line 30
Source documentation
Fiber scaling does not alter any of the three base coordinates.
```
theorem sameBase_scale (F : Frame R) (q : Rˣ) : SameBase F (F.scale q) := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase
theorem OAI.StableCoordinate.FrameLift.normalized_univariate_unique line 39
Source documentation
Univariate version of normalized-polynomial-frame uniqueness, allowing any reduced coefficient ring, in particular a Laurent parameter extension.
```
theorem normalized_univariate_unique [IsReduced R] {F G : Frame R[X]}
    (h : SameBase F G)
    (hzero : F.map Polynomial.constantCoeff = G.map Polynomial.constantCoeff) :
    F = G := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.SameBase
theorem OAI.StableCoordinate.FrameLift.Frame.map_polynomial_constantCoeff line 59
Source documentation
Coefficientwise ring maps commute with specialization of a polynomial family of determinant frames.
```
theorem Frame.map_polynomial_constantCoeff (F : Frame R[X]) (f : R →+* S) :
    (F.map (Polynomial.mapRingHom f)).map Polynomial.constantCoeff =
      (F.map Polynomial.constantCoeff).map f := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.f, OAI.StableCoordinate.FrameLift.Frame.map

theorem OAI.StableCoordinate.FrameLift.normalized_frame_scaling line 67

Source documentation

Fiber equivariance follows from normalization and equality of the base coordinates alone. For the source, S is the Laurent extension of R, ι is the constant inclusion, ρ is fiber scaling, and q is its parameter.

theorem normalized_frame_scaling [IsReduced S]
    (F : Frame R[X]) (F₀ : Frame R) (ρ ι : R →+* S) (q : Sˣ)
    (hnormal : F.map Polynomial.constantCoeff = F₀)
    (hzero : F₀.map ρ = (F₀.map ι).scale q)
    (hbase : SameBase (F.map (Polynomial.mapRingHom ρ))
      (F.map (Polynomial.mapRingHom ι))) :
    F.map (Polynomial.mapRingHom ρ) =
      (F.map (Polynomial.mapRingHom ι)).scale (Units.map (Polynomial.C : S →+* S[X]).toMonoidHom q) := by
…

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

theorem OAI.StableCoordinate.FrameLift.sameBase_map_of_base_polynomials line 85

Source documentation

If the base coordinate polynomials come from a fixed subring, two coefficient homomorphisms agreeing on that subring produce frames over the same base.

theorem sameBase_map_of_base_polynomials
    {B : Type*} [CommRing B] (F : Frame R[X]) (j : B →+* R)
    (ρ ι : R →+* S) (hbase : ρ.comp j = ι.comp j)
    (x y z : B[X])
    (hx : F.a * F.b = x.map j)
    (hy : F.d * F.c = y.map j)
    (hz : F.d * F.b = z.map j) :
    SameBase (F.map (Polynomial.mapRingHom ρ))
      (F.map (Polynomial.mapRingHom ι)) := by
…

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

theorem OAI.StableCoordinate.FrameLift.normalized_frame_scaling_of_base line 104

Source documentation

Version ready for an algebraic-action lift: the base coordinate polynomials have been constructed in the base ring, whose scaling is trivial.

theorem normalized_frame_scaling_of_base [IsReduced S]
    {B : Type*} [CommRing B] (F : Frame R[X]) (F₀ : Frame R)
    (j : B →+* R) (ρ ι : R →+* S) (q : Sˣ)
    (hbase : ρ.comp j = ι.comp j)
    (x y z : B[X])
    (hx : F.a * F.b = x.map j)
    (hy : F.d * F.c = y.map j)
    (hz : F.d * F.b = z.map j)
    (hnormal : F.map Polynomial.constantCoeff = F₀)
    (hzero : F₀.map ρ = (F₀.map ι).scale q) :
    F.map (Polynomial.mapRingHom ρ) =
      (F.map (Polynomial.mapRingHom ι)).scale
…

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

theorem OAI.StableCoordinate.FrameLift.coefficient_scaling line 122

Source documentation

The exact coefficient equations implied by frame-scaling equivariance. The case n=1 is the infinitesimal fiber-weight preservation statement.

theorem coefficient_scaling (F : Frame R[X]) (ρ ι : R →+* S) (q : Sˣ)
    (h : F.map (Polynomial.mapRingHom ρ) =
      (F.map (Polynomial.mapRingHom ι)).scale
        (Units.map (Polynomial.C : S →+* S[X]).toMonoidHom q)) (n : ℕ) :
    ρ (F.a.coeff n) = ↑q * ι (F.a.coeff n) ∧
    ρ (F.d.coeff n) = ↑q * ι (F.d.coeff n) ∧
    ρ (F.b.coeff n) = ↑q⁻¹ * ι (F.b.coeff n) ∧
    ρ (F.c.coeff n) = ↑q⁻¹ * ι (F.c.coeff n) := by
…

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