OAI/Algebra/AffineCancellation/DeterminantRigidity.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexCancellation.Determinant.δP line 15
  2. def OAI.ComplexCancellation.Determinant.ηP line 16
  3. lemma OAI.ComplexCancellation.Determinant.δP_relation line 18
  4. lemma OAI.ComplexCancellation.Determinant.ηP_relation line 21
  5. def OAI.ComplexCancellation.Determinant.δ line 25
  6. def OAI.ComplexCancellation.Determinant.η line 27
  7. def OAI.ComplexCancellation.Determinant.Euler line 29
  8. lemma OAI.ComplexCancellation.Determinant.δ_π line 31
  9. lemma OAI.ComplexCancellation.Determinant.η_π line 32
  10. lemma OAI.ComplexCancellation.Determinant.δ_a line 33
  11. lemma OAI.ComplexCancellation.Determinant.δ_d line 34
  12. lemma OAI.ComplexCancellation.Determinant.δ_b line 35
  13. lemma OAI.ComplexCancellation.Determinant.δ_c line 36
  14. lemma OAI.ComplexCancellation.Determinant.δ_u line 37
  15. lemma OAI.ComplexCancellation.Determinant.η_a line 38
  16. lemma OAI.ComplexCancellation.Determinant.η_d line 39
  17. lemma OAI.ComplexCancellation.Determinant.η_b line 40
  18. lemma OAI.ComplexCancellation.Determinant.η_c line 41
  19. lemma OAI.ComplexCancellation.Determinant.η_u line 42
  20. lemma OAI.ComplexCancellation.Determinant.Euler_a line 43
  21. lemma OAI.ComplexCancellation.Determinant.Euler_d line 44
  22. lemma OAI.ComplexCancellation.Determinant.Euler_b line 45
  23. lemma OAI.ComplexCancellation.Determinant.Euler_c line 46
  24. lemma OAI.ComplexCancellation.Determinant.Euler_u line 47
  25. lemma OAI.ComplexCancellation.Determinant.derivation_ext line 49
  26. lemma OAI.ComplexCancellation.Determinant.η_locallyNilpotent line 60
  27. lemma OAI.ComplexCancellation.Determinant.Euler_η line 67
  28. def OAI.ComplexCancellation.Determinant.FiberShift line 80

    Source documentation

    Exact infinitesimal formulation of a fixed fiber-weight shift.

    def FiberShift (E : Derivation ℂ T T) (e : ℤ) : Prop :=
…

    Mentions: OAI.ComplexCancellation.Determinant.T

  29. lemma OAI.ComplexCancellation.Determinant.fixed_coefficients_contradiction line 83
  30. def OAI.ComplexCancellation.Determinant.auxWeight line 135
  31. abbrev OAI.ComplexCancellation.Determinant.auxPoly line 136
  32. abbrev OAI.ComplexCancellation.Determinant.aux line 137
  33. lemma OAI.ComplexCancellation.Determinant.relation_aux line 139
  34. lemma OAI.ComplexCancellation.Determinant.aux_ker line 150
  35. instance OAI.ComplexCancellation.Determinant.auxGrading line 159
  36. lemma OAI.ComplexCancellation.Determinant.aux_X line 162
  37. lemma OAI.ComplexCancellation.Determinant.aux_a line 164
  38. lemma OAI.ComplexCancellation.Determinant.aux_d line 165
  39. lemma OAI.ComplexCancellation.Determinant.aux_b line 166
  40. lemma OAI.ComplexCancellation.Determinant.aux_c line 167
  41. lemma OAI.ComplexCancellation.Determinant.aux_u line 168
  42. lemma OAI.ComplexCancellation.Determinant.aux_N line 169
  43. lemma OAI.ComplexCancellation.Determinant.aux_a3b line 176
  44. lemma OAI.ComplexCancellation.Determinant.Euler_aux line 182
  45. lemma OAI.ComplexCancellation.Determinant.Euler_proj line 202
  46. lemma OAI.ComplexCancellation.Determinant.component_fiberShift line 214
  47. lemma OAI.ComplexCancellation.Determinant.nonzero_base_X line 225
  48. lemma OAI.ComplexCancellation.Determinant.a_ne_zero line 228
  49. lemma OAI.ComplexCancellation.Determinant.d_ne_zero line 229
  50. lemma OAI.ComplexCancellation.Determinant.u_ne_zero line 230
  51. lemma OAI.ComplexCancellation.Determinant.N_ne_zero line 231
  52. lemma OAI.ComplexCancellation.Determinant.nonsquare_u line 240
  53. theorem OAI.ComplexCancellation.Determinant.rigidity line 251

    Source documentation

    Rigidity for the determinant algebra with its fiber Euler operator.

    theorem rigidity (E : Derivation ℂ T T) (hln : LND.LocallyNilpotent E)
    (e : ℤ) (he : e ≤ 0) (hshift : FiberShift E e) (hv : E (E v) = 0) : E = 0 := by
…

    Mentions: OAI.ComplexCancellation.Determinant.T, OAI.ComplexCancellation.LND.LocallyNilpotent, OAI.ComplexCancellation.Determinant.FiberShift, OAI.ComplexCancellation.Determinant.v