PolynomialChartIntersection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Constants in polynomial charts

Section 5 identifies two localizations of the determinant ring with polynomial rings over principal localizations of k[a,d,u]. The needed intersection with k(a,d,u) is not a set-theoretic assertion: a polynomial over the chart's coefficient ring which becomes constant over the fraction field has that constant in its coefficient ring. The lemmas here prove that exact algebraic interface without assuming the manuscript's chart identifications.

theorem OAI.StableCoordinate.PolynomialChartIntersection.constant_mem_range_map_iff line 27
Source documentation
Taking the constant coefficient recovers a constant in the range of an actual polynomial coefficient map. No injectivity assumption is needed.
```
theorem constant_mem_range_map_iff (f : R →+* S) (s : S) :
    C s ∈ Set.range (Polynomial.map f) ↔ s ∈ Set.range f := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.PolynomialChartIntersection.map_eq_C_iff line 38
Source documentation
A mapped polynomial that becomes constant was itself constant when the coefficient map is injective.
```
theorem map_eq_C_iff (f : R →+* S) (hf : Function.Injective f)
    (p : R[X]) (s : S) :
    Polynomial.map f p = C s ↔ ∃ r : R, p = C r ∧ f r = s := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.PolynomialChartIntersection.polynomial_range_inf_constants line 54
Source documentation
The intersection of coefficientwise images with the constant polynomials is exactly the image of the original coefficient ring.
```
theorem polynomial_range_inf_constants (f : R →+* S) :
    (Polynomial.mapRingHom f).rangeS ⊓ (C : S →+* S[X]).rangeS =
      ((C : S →+* S[X]).comp f).rangeS := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.R

theorem OAI.StableCoordinate.PolynomialChartIntersection.mem_coefficient_range_of_compatible_chart line 82

Source documentation

If a polynomial chart and a coefficient-field embedding agree in a common ambient ring, injectivity of the polynomial chart forces the putative constant to belong to the chart coefficient ring. All maps and commuting-square conditions are explicit; no identification of abstractly isomorphic rings is silently used.

theorem mem_coefficient_range_of_compatible_chart
    (f : A →+* K) (chart : C →+* A[X])
    (inclusion : C →+* Ω) (coefficients : K →+* Ω)
    (polynomialEmbedding : K[X] →+* Ω)
    (hinj : Function.Injective polynomialEmbedding)
    (hchart : (polynomialEmbedding.comp (Polynomial.mapRingHom f)).comp chart = inclusion)
    (hcoeff : polynomialEmbedding.comp (Polynomial.C : K →+* K[X]) = coefficients)
    {c : C} {q : K} (h : inclusion c = coefficients q) :
    q ∈ Set.range f := by
…

Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.PolynomialChartIntersection.chart_eq_constant_of_compatible_chart line 101

Source documentation

The previous lemma also records the stronger conclusion that the chart polynomial itself is constant whenever its coefficient map is injective.

theorem chart_eq_constant_of_compatible_chart
    (f : A →+* K) (hf : Function.Injective f) (chart : C →+* A[X])
    (inclusion : C →+* Ω) (coefficients : K →+* Ω)
    (polynomialEmbedding : K[X] →+* Ω)
    (hinj : Function.Injective polynomialEmbedding)
    (hchart : (polynomialEmbedding.comp (Polynomial.mapRingHom f)).comp chart = inclusion)
    (hcoeff : polynomialEmbedding.comp (Polynomial.C : K →+* K[X]) = coefficients)
    {c : C} {q : K} (h : inclusion c = coefficients q) :
    ∃ a : A, chart c = Polynomial.C a ∧ f a = q := by
…

Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.PolynomialChartIntersection.polynomial_algRange_inf_constants line 127
Source documentation
The constants-in-chart statement in the form of an equality of k-subalgebras, for direct use with affine coordinate rings.
```
theorem polynomial_algRange_inf_constants (f : R →ₐ[k] S) :
    (Polynomial.mapAlgHom f).range ⊓ (Polynomial.CAlgHom : S →ₐ[k] S[X]).range =
      ((Polynomial.CAlgHom : S →ₐ[k] S[X]).comp f).range := by
…
```
Mentions: OAI.StableCoordinate.f, OAI.StableCoordinate.R