DeterminantRigidity.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Rigidity helpers on the actual determinant quotient

These results instantiate the general derivation arguments on the exact ring k[a,d,b,c,u]/(ac-bd-1). Generator nonvanishing is proved by an algebraic point, not assumed or inferred from an unproved localization identification.

def OAI.StableCoordinate.DeterminantRing.v line 25
Source documentation
The distinguished element of source equation bun:v.
```
def v : C k := a k ^ 3 * b k + a k ^ 2 * u k ^ 2 - d k ^ 2
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.a, OAI.StableCoordinate.DeterminantRing.b, OAI.StableCoordinate.DeterminantRing.u, OAI.StableCoordinate.DeterminantRing.d
def OAI.StableCoordinate.DeterminantRing.factorPoint line 28
Source documentation
A point at which the factors used by the rigidity argument are nonzero.
```
def factorPoint : C k →ₐ[k] k := lift 1 0 0 1 1 (by simp)
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.lift
theorem OAI.StableCoordinate.DeterminantRing.factorPoint_a line 30
theorem OAI.StableCoordinate.DeterminantRing.factorPoint_d line 31
theorem OAI.StableCoordinate.DeterminantRing.factorPoint_u line 32
theorem OAI.StableCoordinate.DeterminantRing.algebraMap_injective line 35
Source documentation
The scalar inclusion is injective, witnessed by factorPoint.
```
theorem algebraMap_injective : Function.Injective (algebraMap k (C k)) := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C
instance OAI.StableCoordinate.DeterminantRing.instCharZero line 40
instance OAI.StableCoordinate.DeterminantRing.instNontrivial line 43
theorem OAI.StableCoordinate.DeterminantRing.a_ne_zero line 47
Source documentation
The first base variable is nonzero in the actual quotient.
```
theorem a_ne_zero [Nontrivial k] : a k ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.a
theorem OAI.StableCoordinate.DeterminantRing.u_ne_zero line 53
Source documentation
The added base variable is nonzero in the actual quotient.
```
theorem u_ne_zero [Nontrivial k] : u k ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.u
theorem OAI.StableCoordinate.DeterminantRing.au_sub_d_ne_zero line 59
Source documentation
The two factors of the highest auxiliary part of v are nonzero.
```
theorem au_sub_d_ne_zero [Nontrivial k] : a k * u k - d k ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.a, OAI.StableCoordinate.DeterminantRing.u, OAI.StableCoordinate.DeterminantRing.d
theorem OAI.StableCoordinate.DeterminantRing.au_add_d_ne_zero line 64
theorem OAI.StableCoordinate.DeterminantRing.mk_surjective line 70
Source documentation
Every element of the determinant ring has a polynomial representative.
```
theorem mk_surjective : Function.Surjective (mk k) :=
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.mk
theorem OAI.StableCoordinate.DeterminantRing.adjoin_range_generator_via_quotient line 74
Source documentation
The five canonical quotient variables generate the full algebra.
```
theorem adjoin_range_generator_via_quotient :
    Algebra.adjoin k (Set.range (generator k)) = ⊤ := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.generator
theorem OAI.StableCoordinate.DeterminantRing.derivation_eq_zero line 83
Source documentation
A derivation is determined by its five generator values.
```
theorem derivation_eq_zero (D : Derivation k (C k) (C k))
    (ha : D (a k) = 0) (hd : D (d k) = 0) (hb : D (b k) = 0)
    (hc : D (c k) = 0) (hu : D (u k) = 0) : D = 0 := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.a, OAI.StableCoordinate.DeterminantRing.d, OAI.StableCoordinate.DeterminantRing.b, OAI.StableCoordinate.DeterminantRing.c, OAI.StableCoordinate.DeterminantRing.u
theorem OAI.StableCoordinate.DeterminantRing.coefficient_ne_zero line 107
Source documentation
The coefficient of a nonzero derivation fixing a,d,u is nonzero.
```
theorem coefficient_ne_zero (D : Derivation k (C k) (C k))
    (hD : D ≠ 0) (ha : D (a k) = 0) (hd : D (d k) = 0) (hu : D (u k) = 0) :
    rigidityCoefficient D (b k) (c k) ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.a, OAI.StableCoordinate.DeterminantRing.d, OAI.StableCoordinate.DeterminantRing.u, OAI.StableCoordinate.rigidityCoefficient, OAI.StableCoordinate.DeterminantRing.b, OAI.StableCoordinate.DeterminantRing.c
theorem OAI.StableCoordinate.DeterminantRing.fixed_of_difference_of_squares line 117
Source documentation
The difference-of-squares argument instantiated on the actual quotient.
```
theorem fixed_of_difference_of_squares [Nontrivial k] [IsDomain (C k)] [CharZero (C k)]
    (D : Derivation k (C k) (C k)) (hD : IsLocallyNilpotent D)
    (hv : D (a k ^ 2 * u k ^ 2 - d k ^ 2) = 0) :
    D (a k) = 0 ∧ D (d k) = 0 ∧ D (u k) = 0 :=
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.DeterminantRing.a, OAI.StableCoordinate.DeterminantRing.u, OAI.StableCoordinate.DeterminantRing.d