QuadricFactorization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Lifting a quadric point to a determinant-one frame over a GCD domain

This is an algebraic substitute for the local trivialization step in the additive-action lift. It constructs a frame, rather than assuming a line bundle is trivial. After pullback to the factorial ring of the determinant-one quadric, it can be applied over that ring's polynomial extension.

theorem OAI.StableCoordinate.QuadricFactorization.exists_frame_of_ne_zero line 24
Source documentation
Every point of xy=z(z+1) over a GCD domain with nonzero x admits a factorization by a determinant-one matrix. No Bezout-domain assumption is used.
```
theorem exists_frame_of_ne_zero (x y z : R) (hx : x ≠ 0)
    (h : x * y = z * (z + 1)) :
    ∃ a d b c : R,
      a * b = x ∧ d * b = z ∧ d * c = y ∧ a * c = z + 1 ∧
        a * c - b * d = 1 := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.QuadricFactorization.exists_frame line 62
Source documentation
The zero-x cases are elementary, so a determinant frame exists without any nonvanishing assumption on the given quadric point.
```
theorem exists_frame (x y z : R) (h : x * y = z * (z + 1)) :
    ∃ a d b c : R,
      a * b = x ∧ d * b = z ∧ d * c = y ∧ a * c = z + 1 ∧
        a * c - b * d = 1 := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.QuadricFactorization.exists_frameAbove line 77
Source documentation
Existence in the canonical frame type used by the action-lift construction.
```
theorem exists_frameAbove (x y z : R) (h : x * y = z * (z + 1)) :
    ∃ F : FrameLift.Frame R,
      F.a * F.b = x ∧ F.d * F.c = y ∧ F.d * F.b = z := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame
def OAI.StableCoordinate.QuadricFactorization.frameAbove line 84
Source documentation
A choice of determinant-one frame above a quadric point.
```
def frameAbove (x y z : R) (h : x * y = z * (z + 1)) : FrameLift.Frame R :=
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.FrameLift.Frame
theorem OAI.StableCoordinate.QuadricFactorization.frameAbove_ab line 88
theorem OAI.StableCoordinate.QuadricFactorization.frameAbove_dc line 93
theorem OAI.StableCoordinate.QuadricFactorization.frameAbove_db line 98