BundlePrincipalization.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit global principalization in the quadric bundle

This module gives polynomial identities, valid in every commutative ring, for the principalization in source Section 4, Lemma bun:principalization. Unlike the source proof, the argument uses an explicit global Bezout identity and requires neither localization nor prime-spectrum gluing.

def OAI.StableCoordinate.Bundle.s line 21
Source documentation
Pullback of the source element s_B under x = ab, y = dc.
```
def s (a d b c u : R) : R := d * c - (a * b) * (a * b + u ^ 2)
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.Bundle.f₀ line 24
Source documentation
First generator of the pulled-back distinguished ideal.
```
def f₀ (a d b c u : R) : R := a * b - s a d b c u ^ 2 + u ^ 2
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Bundle.s
def OAI.StableCoordinate.Bundle.g₀ line 27
Source documentation
Second generator of the pulled-back distinguished ideal.
```
def g₀ (a d b c u : R) : R := d * b - s a d b c u * (a * b)
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Bundle.s
def OAI.StableCoordinate.Bundle.v line 30
Source documentation
The global generator of the pulled-back ideal.
```
def v (a d b u : R) : R := a ^ 3 * b + a ^ 2 * u ^ 2 - d ^ 2
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.Bundle.coeffA line 33
Source documentation
First coefficient in the global Bezout relation.
```
def coeffA (a d b : R) : R := a ^ 2 * (1 - 2 * b * d)
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.Bundle.coeffB line 36
Source documentation
Second coefficient in the global Bezout relation.
```
def coeffB (a d b u : R) : R :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.Bundle.g₀_factor line 39
theorem OAI.StableCoordinate.Bundle.f₀_factor line 44
theorem OAI.StableCoordinate.Bundle.coefficients_bezout line 49
theorem OAI.StableCoordinate.Bundle.generator_bezout line 55
theorem OAI.StableCoordinate.Bundle.principalization line 62
Source documentation
The exact global principalization claimed in Section 4.
```
theorem principalization (a d b c u : R) (h : a * c - b * d = 1) :
    Ideal.span ({f₀ a d b c u, g₀ a d b c u} : Set R) =
      Ideal.span ({v a d b u} : Set R) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Bundle.f₀, OAI.StableCoordinate.Bundle.g₀, OAI.StableCoordinate.Bundle.v
theorem OAI.StableCoordinate.Bundle.exists_factor_of_mem line 82
Source documentation
Membership in the pulled-back ideal gives an actual factorization by v.
```
theorem exists_factor_of_mem (a d b c u : R) (h : a * c - b * d = 1)
    {r : R} (hr : r ∈ Ideal.span ({f₀ a d b c u, g₀ a d b c u} : Set R)) :
    ∃ q : R, r = v a d b u * q := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Bundle.f₀, OAI.StableCoordinate.Bundle.g₀, OAI.StableCoordinate.Bundle.v