DeterminantIntersection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual coefficient-ring intersection for the determinant hypersurface

This is the two-chart coefficient-membership step in source Section 5, now instantiated on the exact quotient k[a,d,b,c,u]/(ac-bd-1). The chart maps, their injectivity, the domain property, and independence of a,d,u are all proved constructions. No chart or domain assumption remains in the theorems.

theorem OAI.StableCoordinate.DeterminantRing.exists_base_of_constant_charts line 24
Source documentation
If an element of the determinant ring is a coefficient in each of its two polynomial charts, it belongs to the actual polynomial subring k[a,d,u].
```
theorem exists_base_of_constant_charts {q : C k}
    {v : BaseAway k 0} {w : BaseAway k 1}
    (hA : chartMapA k q = Polynomial.C v)
    (hD : chartMapD k q = Polynomial.C w) :
    ∃ r : Base k, baseMap r = q := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.v, OAI.StableCoordinate.DeterminantRing.BaseAway, OAI.StableCoordinate.DeterminantRing.chartMapA, OAI.StableCoordinate.DeterminantRing.chartMapD, OAI.StableCoordinate.DeterminantRing.Base, OAI.StableCoordinate.DeterminantRing.baseMap
theorem OAI.StableCoordinate.DeterminantRing.mem_range_baseMap_iff_constant_charts line 38
Source documentation
Exact membership characterization, with both implications retained.
```
theorem mem_range_baseMap_iff_constant_charts (q : C k) :
    q ∈ Set.range (baseMap (k := k)) ↔
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.baseMap