OAI/Algebra/AffineCancellation/PositiveObstruction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComplexCancellation.Determinant.Euler_v line 9
2. abbrev OAI.ComplexCancellation.Bundle.valuationPieces line 16
3. instance OAI.ComplexCancellation.Bundle.valuationGrading line 18
4. def OAI.ComplexCancellation.Bundle.fiberEuler line 20
5. theorem OAI.ComplexCancellation.Bundle.no_positive_invariant line 22

   Source documentation

   The positive-invariant obstruction on the pullback ring.

   theorem no_positive_invariant
       (D : Derivation ℂ B B) (hD : LND.LocallyNilpotent D) (hDn : D ≠ 0)
       (j : ℤ) (hshift : ∀ e r, r ∈ valuationPieces e → D r ∈ valuationPieces (e+j))
       (hcomm : ∀ z, fiberEuler (D z)=D (fiberEuler z))
       (w : B) (hw : w ≠ 0) (e : ℤ) (he : 0 < e)
       (hwg : w ∈ valuationPieces e) (hDw : D w=0) : False := by
   …

   Mentions: OAI.ComplexCancellation.Bundle.B, OAI.ComplexCancellation.LND.LocallyNilpotent, OAI.ComplexCancellation.Bundle.j, OAI.ComplexCancellation.Bundle.valuationPieces, OAI.ComplexCancellation.Bundle.fiberEuler