FrameLiftUniqueness.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of normalized polynomial lifts of determinant frames

The bundle in the source is described by a*c - b*d = 1, with base coordinates a*b, d*c, and d*b. This file proves directly in rings that two frames over the same base differ by a unit. Consequently two polynomial families over a reduced ring, having the same base and the same specialization at the zero parameter, agree. In the action-lift argument this is the algebraic group-law normalization step; the existence of a lifted polynomial family is a separate obligation.

structure OAI.StableCoordinate.FrameLift.Frame line 22
Source documentation
A frame for the rank-one bundle underlying the determinant presentation.
```
structure Frame (R : Type*) [CommRing R] where
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.FrameLift.Frame.ext line 32
def OAI.StableCoordinate.FrameLift.Frame.map line 37
Source documentation
Extend each coordinate of a frame by a ring homomorphism.
```
def Frame.map (f : R →+* S) (F : Frame R) : Frame S where
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame
def OAI.StableCoordinate.FrameLift.SameBase line 45
Source documentation
Equality of the three quadric base coordinates.
```
def SameBase (F G : Frame R) : Prop :=
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R
def OAI.StableCoordinate.FrameLift.comparison line 49
Source documentation
Concrete scalar comparing two frames over the same base.
```
def comparison (F G : Frame R) : R := F.c * G.a - F.b * G.d
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.FrameLift.sameBase_symm line 51
theorem OAI.StableCoordinate.FrameLift.comparison_a line 54
theorem OAI.StableCoordinate.FrameLift.comparison_d line 59
theorem OAI.StableCoordinate.FrameLift.comparison_b line 64
theorem OAI.StableCoordinate.FrameLift.comparison_c line 69
theorem OAI.StableCoordinate.FrameLift.comparison_mul_reverse line 75
Source documentation
The two comparison scalars are inverse units, without any domain hypothesis.
```
theorem comparison_mul_reverse {F G : Frame R} (h : SameBase F G) :
    comparison F G * comparison G F = 1 := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.comparison
def OAI.StableCoordinate.FrameLift.comparisonUnit line 87
Source documentation
The unique unit changing one frame into the other.
```
def comparisonUnit {F G : Frame R} (h : SameBase F G) : Rˣ where
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase
theorem OAI.StableCoordinate.FrameLift.comparison_self line 94
theorem OAI.StableCoordinate.FrameLift.comparison_map line 98
theorem OAI.StableCoordinate.FrameLift.comparison_unique line 103
Source documentation
The scalar is determined by its action on the two positive-weight coordinates.
```
theorem comparison_unique (F G : Frame R) {q : R}
    (ha : q * F.a = G.a) (hd : q * F.d = G.d) : q = comparison F G := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.comparison
theorem OAI.StableCoordinate.FrameLift.eq_of_comparison_eq_one line 109
Source documentation
Comparison scalar one forces equality of the entire frame.
```
theorem eq_of_comparison_eq_one {F G : Frame R} (h : SameBase F G)
    (hq : comparison F G = 1) : F = G := by
…
```
Mentions: OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.SameBase, OAI.StableCoordinate.FrameLift.comparison
theorem OAI.StableCoordinate.FrameLift.normalized_polynomial_unique line 124
Source documentation
Two polynomial families of frames over a reduced coefficient ring are equal if they have the same base coordinates and agree at the zero parameter.
In particular this proves the group law for a normalized polynomial-family lift: compare the iterated lift over two parameters with the lift at their sum.
```
theorem normalized_polynomial_unique {σ : Type*} [IsReduced R]
    {F G : Frame (MvPolynomial σ R)} (h : SameBase F G)
    (hzero : F.map MvPolynomial.constantCoeff = G.map MvPolynomial.constantCoeff) :
    F = G := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame, OAI.StableCoordinate.FrameLift.SameBase