RigidityCoefficients.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Coefficients of derivations on the determinant-one hypersurface

This file formalizes the coefficient step of §5, equation rig:q, from the supplied manuscript. No local nilpotence or domain hypothesis is needed for this purely algebraic step. The nonzero criterion uses the stated generation hypothesis rather than silently assuming the five displayed elements generate.

theorem OAI.StableCoordinate.determinant_coefficient_left line 22
Source documentation
The first coefficient identity follows from the determinant-one relation.
```
theorem determinant_coefficient_left (a d b c B C : A)
    (hdet : a * c - b * d = 1) (hcompat : a * C = d * B) :
    B = a * (c * B - b * C) := by
…
```

theorem OAI.StableCoordinate.determinant_coefficient_right line 31

Source documentation

The second coefficient identity follows from the same relation.

theorem determinant_coefficient_right (a d b c B C : A)
    (hdet : a * c - b * d = 1) (hcompat : a * C = d * B) :
    C = d * (c * B - b * C) := by
…

theorem OAI.StableCoordinate.determinant_coefficient_unique line 40

Source documentation

The coefficient is unique, without cancellation or nonzero hypotheses.

theorem determinant_coefficient_unique (a d b c B C q : A)
    (hdet : a * c - b * d = 1) (hB : B = a * q) (hC : C = d * q) :
    q = c * B - b * C := by
…

theorem OAI.StableCoordinate.derivation_determinant_compatibility line 55

Source documentation

Differentiating ac - bd = 1, when a,d are invariant.

theorem derivation_determinant_compatibility (D : Derivation k A A)
    (a d b c : A) (hdet : a * c - b * d = 1)
    (ha : D a = 0) (hd : D d = 0) :
    a * D c = d * D b := by
…

def OAI.StableCoordinate.rigidityCoefficient line 64
Source documentation
The source coefficient q = c D(b) - b D(c).
```
def rigidityCoefficient (D : Derivation k A A) (b c : A) : A :=
…
```

theorem OAI.StableCoordinate.derivation_rigidityCoefficient line 68

Source documentation

The two identities in source equation rig:q in arbitrary commutative algebras.

theorem derivation_rigidityCoefficient (D : Derivation k A A)
    (a d b c : A) (hdet : a * c - b * d = 1)
    (ha : D a = 0) (hd : D d = 0) :
    D b = a * rigidityCoefficient D b c ∧ D c = d * rigidityCoefficient D b c := by
…

Mentions: OAI.StableCoordinate.rigidityCoefficient

theorem OAI.StableCoordinate.derivation_eq_zero_of_five_generators line 78

Source documentation

A derivation of the algebra generated by a,d,b,c,u vanishes once these five generators are invariant.

theorem derivation_eq_zero_of_five_generators (D : Derivation k A A)
    (a d b c u : A) (hgen : Algebra.adjoin k {a, d, b, c, u} = ⊤)
    (ha : D a = 0) (hd : D d = 0) (hb : D b = 0) (hc : D c = 0)
    (hu : D u = 0) : D = 0 := by
…

theorem OAI.StableCoordinate.rigidityCoefficient_ne_zero line 90

Source documentation

Under the exact generation condition used in §5, the source coefficient is nonzero whenever the derivation is nonzero.

theorem rigidityCoefficient_ne_zero (D : Derivation k A A)
    (a d b c u : A) (hdet : a * c - b * d = 1)
    (hgen : Algebra.adjoin k {a, d, b, c, u} = ⊤)
    (ha : D a = 0) (hd : D d = 0) (hu : D u = 0) (hD : D ≠ 0) :
    rigidityCoefficient D b c ≠ 0 := by
…

Mentions: OAI.StableCoordinate.rigidityCoefficient