AmbientMaps.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Polynomial maps induced by coordinate-ring maps

The maps in this file carry actual coordinate polynomials and satisfy polynomial composition identities. In particular, the geometric interpretation of an algebra equivalence below is not merely a set-theoretic bijection of complex points.

def OAI.StableCoordinate.AmbientMaps.pointMap line 25
Source documentation
The point map contravariantly induced by a homomorphism of polynomial algebras.
```
def pointMap (φ : MvPolynomial τ k →ₐ[k] MvPolynomial σ k)
    (x : σ → k) : τ → k :=
…
```
theorem OAI.StableCoordinate.AmbientMaps.aeval_pointMap line 30
Source documentation
Pulling back a polynomial and evaluating agrees with evaluating it on the point map.
```
theorem aeval_pointMap (φ : MvPolynomial τ k →ₐ[k] MvPolynomial σ k)
    (x : σ → k) (p : MvPolynomial τ k) :
    aeval (pointMap φ x) p = aeval x (φ p) := by
…
```
Mentions: OAI.StableCoordinate.AmbientMaps.pointMap
theorem OAI.StableCoordinate.AmbientMaps.pointMap_id line 39

theorem OAI.StableCoordinate.AmbientMaps.pointMap_comp line 45

Source documentation

Composition is reversed, as it must be for maps of coordinate rings.

theorem pointMap_comp (φ : MvPolynomial τ k →ₐ[k] MvPolynomial σ k)
    (ψ : MvPolynomial υ k →ₐ[k] MvPolynomial τ k) (x : σ → k) :
    pointMap (φ.comp ψ) x = pointMap ψ (pointMap φ x) := by
…

Mentions: OAI.StableCoordinate.AmbientMaps.pointMap

structure OAI.StableCoordinate.AmbientMaps.PolynomialEquiv line 53
Source documentation
A polynomial isomorphism, with inverse identities in the polynomial rings, not just identities of functions on the base field.
```
structure PolynomialEquiv (k : Type*) [CommSemiring k] (σ τ : Type*) where
…
```
def OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.ofAlgEquiv line 62
Source documentation
An algebra isomorphism supplies polynomial coordinates for both directions.
```
def ofAlgEquiv (e : MvPolynomial τ k ≃ₐ[k] MvPolynomial σ k) :
    PolynomialEquiv k σ τ where
…
```
Mentions: OAI.StableCoordinate.AmbientMaps.PolynomialEquiv
def OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.toPointMap line 76
Source documentation
The forward polynomial map.
```
def toPointMap (e : PolynomialEquiv k σ τ) (x : σ → k) : τ → k :=
…
```
Mentions: OAI.StableCoordinate.AmbientMaps.PolynomialEquiv
def OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.invPointMap line 80
Source documentation
The inverse polynomial map.
```
def invPointMap (e : PolynomialEquiv k σ τ) (y : τ → k) : σ → k :=
…
```
Mentions: OAI.StableCoordinate.AmbientMaps.PolynomialEquiv
theorem OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.invPointMap_toPointMap line 84
theorem OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.toPointMap_invPointMap line 91
def OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.toEquiv line 98
Source documentation
The underlying point equivalence, retaining its polynomial witnesses in e.
```
def toEquiv (e : PolynomialEquiv k σ τ) : (σ → k) ≃ (τ → k) where
…
```
Mentions: OAI.StableCoordinate.AmbientMaps.PolynomialEquiv
theorem OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.ofAlgEquiv_toPointMap line 105
theorem OAI.StableCoordinate.AmbientMaps.PolynomialEquiv.ofAlgEquiv_invPointMap line 110
theorem OAI.StableCoordinate.AmbientMaps.pointMap_levelSet line 118
Source documentation
An ambient algebra equivalence transports every level set by an explicitly polynomial point equivalence. The inverse direction is the one matching pullback.
```
theorem pointMap_levelSet (e : MvPolynomial τ k ≃ₐ[k] MvPolynomial σ k)
    (p : MvPolynomial τ k) (c : k) :
    pointMap e.toAlgHom ⁻¹' {y | aeval y p = c} =
      {x | aeval x (e p) = c} := by
…
```
Mentions: OAI.StableCoordinate.AmbientMaps.pointMap