DeterminantDomain.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Domain properties of the two concrete auxiliary rings

The determinant equation and the quadric relation are irreducible primitive linear polynomials in one of their variables. This file proves their principal ideals prime, and hence the corresponding affine coordinate rings are domains, over every unique factorization domain.

def OAI.StableCoordinate.DeterminantDomain.determinantRelation line 21
Source documentation
Variables are ordered a,d,b,c,u.
```
def determinantRelation : MvPolynomial (Fin 5) k :=
…
```
def OAI.StableCoordinate.DeterminantDomain.quadricRelation line 25
Source documentation
Variables are ordered x,y,z,u.
```
def quadricRelation : MvPolynomial (Fin 4) k :=
…
```
theorem OAI.StableCoordinate.DeterminantDomain.determinantRelation_irreducible line 29
theorem OAI.StableCoordinate.DeterminantDomain.quadricRelation_irreducible line 52
theorem OAI.StableCoordinate.DeterminantDomain.determinantIdeal_isPrime line 77
Source documentation
The actual determinant hypersurface ideal is prime.
```
theorem determinantIdeal_isPrime :
    (Ideal.span {determinantRelation k}).IsPrime :=
…
```
Mentions: OAI.StableCoordinate.DeterminantDomain.determinantRelation
theorem OAI.StableCoordinate.DeterminantDomain.quadricIdeal_isPrime line 82
Source documentation
The actual quadric hypersurface ideal is prime.
```
theorem quadricIdeal_isPrime :
    (Ideal.span {quadricRelation k}).IsPrime :=
…
```
Mentions: OAI.StableCoordinate.DeterminantDomain.quadricRelation
abbrev OAI.StableCoordinate.DeterminantDomain.DeterminantRing line 87
Source documentation
Coordinate ring of the determinant hypersurface, ordered a,d,b,c,u.
```
abbrev DeterminantRing :=
…
```
abbrev OAI.StableCoordinate.DeterminantDomain.QuadricRing line 91
Source documentation
Coordinate ring of the quadric times the u-line, ordered x,y,z,u.
```
abbrev QuadricRing :=
…
```
instance OAI.StableCoordinate.DeterminantDomain.determinantRing_isDomain line 94
instance OAI.StableCoordinate.DeterminantDomain.quadricRing_isDomain line 97