ChartIntersection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The coefficient-ring step in the two-chart rigidity argument

A polynomial chart over a principal localization detects coefficients which belong to the fraction field of the coefficient ring. This module proves the step by denominator clearing. In particular, it does not require choosing a common overfield or treating a set-theoretic chart as an algebraic chart.

The intended application is R = k[a,d,u] and A = k[a,d,b,c,u]/(ac-bd-1). The two actual injective algebra maps to R[a⁻¹][b] and R[d⁻¹][c] are supplied by the determinant-ring charts.

theorem OAI.StableCoordinate.ChartIntersection.eq_C_of_mul_C_eq_C line 27
Source documentation
A polynomial which becomes constant on multiplication by a nonzero constant was already constant.
```
theorem eq_C_of_mul_C_eq_C {S : Type*} [CommRing S] [NoZeroDivisors S]
    {p : Polynomial S} {r s : S} (hr : r ≠ 0)
    (h : p * C r = C s) : p = C (p.coeff 0) := by
…
```
theorem OAI.StableCoordinate.ChartIntersection.away_algebraMap_injective line 47
Source documentation
The canonical map to a localization away from a nonzero element is injective.
```
theorem away_algebraMap_injective (ha : a ≠ 0) :
    Function.Injective (algebraMap R S) := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ChartIntersection.has_power_denominator_of_chart_constant line 56
Source documentation
An injective polynomial chart whose value is constant supplies a power of the localized element as a denominator in the original algebra.
```
theorem has_power_denominator_of_chart_constant
    (e : A →ₐ[R] Polynomial S) (he : Function.Injective e)
    {q : A} {v : S} (hconst : e q = C v) :
    ∃ (m : ℕ) (t : R), q * algebraMap R A (a ^ m) = algebraMap R A t := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ChartIntersection.has_power_denominator_of_chart line 69
Source documentation
If an element of an algebra is a fraction over the coefficient ring, an injective polynomial chart over R[a⁻¹] gives an a-power denominator. This is the precise content of "there are no b terms" in Section 5.
```
theorem has_power_denominator_of_chart
    (ha : a ≠ 0) (e : A →ₐ[R] Polynomial S) (he : Function.Injective e)
    {q : A} {r s : R} (hr : r ≠ 0)
    (h : q * algebraMap R A r = algebraMap R A s) :
    ∃ (m : ℕ) (t : R), q * algebraMap R A (a ^ m) = algebraMap R A t := by
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.ChartIntersection.mem_range_of_two_constant_charts line 97
Source documentation
A constant in both polynomial charts lies in the base ring. This version is suited to locally nilpotent derivations of the two chart rings, which directly show that both chart images of the rigidity coefficient are constant; no common fraction field needs to be constructed.
```
theorem mem_range_of_two_constant_charts
    (ha : a ≠ 0) (had : IsRelPrime a d)
    (e : A →ₐ[R] Polynomial S) (he : Function.Injective e)
    (f : A →ₐ[R] Polynomial T) (hf : Function.Injective f)
    {q : A} {v : S} {w : T} (hq : e q = C v) (hq' : f q = C w) :
    q ∈ Set.range (algebraMap R A) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.f
theorem OAI.StableCoordinate.ChartIntersection.mem_range_of_fraction_eq_of_two_charts line 116
Source documentation
Two injective polynomial charts at relatively prime coefficient variables force the intersection with the coefficient fraction field to be the original coefficient ring. The fraction-field condition is encoded without an overfield as the equation q*r=s with r ≠ 0.
```
theorem mem_range_of_fraction_eq_of_two_charts
    (ha : a ≠ 0) (hd : d ≠ 0) (had : IsRelPrime a d)
    (e : A →ₐ[R] Polynomial S) (he : Function.Injective e)
    (f : A →ₐ[R] Polynomial T) (hf : Function.Injective f)
    {q : A} {r s : R} (hr : r ≠ 0)
    (h : q * algebraMap R A r = algebraMap R A s) :
    q ∈ Set.range (algebraMap R A) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.f

theorem OAI.StableCoordinate.ChartIntersection.exists_base_of_two_ring_charts line 144

Source documentation

Ring-homomorphism interface for actual quotient charts. The commuting squares are explicit, so callers do not have to install an algebra structure on the hypersurface over its polynomial coefficient subring.

theorem exists_base_of_two_ring_charts
    (ι : R →+* A) (ha : a ≠ 0) (had : IsRelPrime a d)
    (e : A →+* Polynomial S) (he : Function.Injective e)
    (f : A →+* Polynomial T) (hf : Function.Injective f)
    (heBase : ∀ r, e (ι r) = Polynomial.C (algebraMap R S r))
    (hfBase : ∀ r, f (ι r) = Polynomial.C (algebraMap R T r))
    {q : A} {v : S} {w : T}
    (hq : e q = Polynomial.C v) (hq' : f q = Polynomial.C w) :
    ∃ t : R, ι t = q := by
…

Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.f