QuotientTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Transporting hypersurface coordinate rings

The polynomial-presentation, stabilization, and fiber arguments use algebra equivalences of ambient rings. This file records the induced equivalences of principal quotients, including their action on representatives. In particular, transporting a distinguished element transports all of its fibers, without excluding the zero fiber.

def OAI.StableCoordinate.principalQuotientEquiv line 24
Source documentation
An ambient algebra equivalence carrying one equation to another induces an algebra equivalence of their hypersurface coordinate rings.
```
def principalQuotientEquiv (e : A ≃ₐ[k] B) (p : A) (q : B) (hpq : e p = q) :
    (A ⧸ Ideal.span {p}) ≃ₐ[k] (B ⧸ Ideal.span {q}) :=
…
```
theorem OAI.StableCoordinate.principalQuotientEquiv_mk line 31
theorem OAI.StableCoordinate.principalQuotientEquiv_symm_mk line 37
def OAI.StableCoordinate.fiberQuotientEquiv line 44
Source documentation
The equivalence induced on the fiber over an arbitrary scalar c. No nonzero hypothesis is needed: this is equally valid for the zero fiber.
```
def fiberQuotientEquiv (e : A ≃ₐ[k] B) (p : A) (q : B)
    (hpq : e p = q) (c : k) :
    (A ⧸ Ideal.span {p - algebraMap k A c}) ≃ₐ[k]
      (B ⧸ Ideal.span {q - algebraMap k B c}) :=
…
```
theorem OAI.StableCoordinate.fiberQuotientEquiv_mk line 51
theorem OAI.StableCoordinate.fiberQuotientEquiv_symm_mk line 57