NonzeroFiberTransport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Transport of the proved nonzero-fiber calculation

This module connects the simultaneous-equation calculation in NonzeroFiber to the manuscript's successive quotient A/(p-l), then transports it through any proved polynomial-presentation equivalence. The eventual exact-polynomial endpoint supplies the presentation equivalence; these generic transport lemmas are not substituted for that endpoint.

abbrev OAI.StableCoordinate.NonzeroFiber.Source line 26
Source documentation
The manuscript's five-generator single-relation presentation.
```
abbrev Source (K : Type*) [Field K] := P5 K ⧸ Ideal.span {(H : P5 K)}
```
Mentions: OAI.StableCoordinate.NonzeroFiber.P5, OAI.StableCoordinate.NonzeroFiber.H
def OAI.StableCoordinate.NonzeroFiber.sourceP line 29
Source documentation
The distinguished element p in the manuscript presentation.
```
def sourceP : Source K := Ideal.Quotient.mk _ (X 0)
```
Mentions: OAI.StableCoordinate.NonzeroFiber.Source
def OAI.StableCoordinate.NonzeroFiber.sourceFiberEquiv line 32
Source documentation
Every nonzero fiber of the manuscript presentation is a polynomial algebra.
```
def sourceFiberEquiv (l : K) (hl : l≠0) :
    (Source K ⧸ Ideal.span {sourceP - algebraMap K (Source K) l}) ≃ₐ[K] P3 K :=
…
```
Mentions: OAI.StableCoordinate.NonzeroFiber.Source, OAI.StableCoordinate.NonzeroFiber.sourceP, OAI.StableCoordinate.NonzeroFiber.P3
def OAI.StableCoordinate.NonzeroFiber.transportedFiberEquiv line 38
Source documentation
Transfer the proved nonzero-fiber equivalence through a separately proved presentation equivalence that carries p to a specified polynomial.
```
def transportedFiberEquiv {B : Type*} [CommRing B] [Algebra K B]
    (e : Source K ≃ₐ[K] B) (g : B) (hg : e sourceP=g) (l : K) (hl : l≠0) :
    (B ⧸ Ideal.span {g-algebraMap K B l}) ≃ₐ[K] P3 K :=
…
```
Mentions: OAI.StableCoordinate.NonzeroFiber.Source, OAI.StableCoordinate.NonzeroFiber.sourceP, OAI.StableCoordinate.NonzeroFiber.P3