IteratedQuotient.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Successive hypersurface and fiber quotients

The source uses A = P/(H) and then A/(p-lam). This file identifies the successive quotient, as an algebra, with P/(H,p-lam). It is purely a quotient interface and contains no geometric or polynomial hypotheses.

abbrev OAI.StableCoordinate.IteratedQuotient.relationIdeal line 19
Source documentation
The ideal generated by a single equation.
```
abbrev relationIdeal (a : A) : Ideal A := Ideal.span {a}
```
abbrev OAI.StableCoordinate.IteratedQuotient.pairIdeal line 22
Source documentation
The ideal generated by two simultaneous equations.
```
abbrev pairIdeal (a b : A) : Ideal A := Ideal.span {a, b}
```
lemma OAI.StableCoordinate.IteratedQuotient.span_pair_eq_sup line 24
lemma OAI.StableCoordinate.IteratedQuotient.map_relationIdeal line 28
def OAI.StableCoordinate.IteratedQuotient.equiv line 35
Source documentation
Two successive principal quotients are the quotient by the pair of equations.
```
noncomputable def equiv (a b : A) :
    ((A ⧸ relationIdeal A a) ⧸
      Ideal.span {Ideal.Quotient.mk (relationIdeal A a) b}) ≃ₐ[k]
        A ⧸ pairIdeal A a b :=
…
```
Mentions: OAI.StableCoordinate.IteratedQuotient.relationIdeal, OAI.StableCoordinate.IteratedQuotient.pairIdeal
theorem OAI.StableCoordinate.IteratedQuotient.equiv_mk_mk line 44
theorem OAI.StableCoordinate.IteratedQuotient.equiv_symm_mk line 50
def OAI.StableCoordinate.IteratedQuotient.fiberEquiv line 58
Source documentation
Ring-theoretic fibers have the expected simultaneous-equation presentation, with the scalar subtraction performed in the appropriate algebra at each stage.
```
noncomputable def fiberEquiv (H p : A) (lam : k) :
    ((A ⧸ relationIdeal A H) ⧸ Ideal.span {
      Ideal.Quotient.mk (relationIdeal A H) p -
        algebraMap k (A ⧸ relationIdeal A H) lam}) ≃ₐ[k]
      A ⧸ pairIdeal A H (p - algebraMap k A lam) :=
…
```
Mentions: OAI.StableCoordinate.IteratedQuotient.relationIdeal, OAI.StableCoordinate.IteratedQuotient.pairIdeal
theorem OAI.StableCoordinate.IteratedQuotient.fiberEquiv_mk_mk line 67
theorem OAI.StableCoordinate.IteratedQuotient.fiberEquiv_symm_mk line 73