OAI/Algebra/AffineCancellation/HomogeneousExtraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ComplexCancellation.AffineModification.euler_factor line 16
2. lemma OAI.ComplexCancellation.AffineModification.fixed_τ_of_fixed_v line 32
3. lemma OAI.ComplexCancellation.AffineModification.coefficient_order line 43
4. lemma OAI.ComplexCancellation.AffineModification.order_monomial_fixed_V line 54
5. theorem OAI.ComplexCancellation.AffineModification.extract line 63

   Source documentation

   Extraction of a coefficient derivation without assuming invariance of the coefficient ring.

   theorem extract (H : Derivation k R R) (hH : H v=2*v)
       (D : Derivation k (T R v) (T R v)) (hD : LND.LocallyNilpotent D) (hDn : D ≠ 0)
       (j : ℤ) (hshift : ∀ e r, r ∈ pieces R v e → D r ∈ pieces R v (e+j))
       (hcomm : ∀ z, euler v H hH (D z)=D (euler v H hH z))
       (hV : D (V R v)=0) :
       ∃ (E : Derivation k R R) (n : ℕ), E ≠ 0 ∧ LND.LocallyNilpotent E ∧
         (∀ r, H (E r)-E (H r)=-(n • E r)) ∧ E (E v)=0 := by
   …

   Mentions: OAI.ComplexCancellation.H, OAI.ComplexCancellation.AffineModification.T, OAI.ComplexCancellation.LND.LocallyNilpotent, OAI.ComplexCancellation.AffineModification.pieces, OAI.ComplexCancellation.AffineModification.euler, OAI.ComplexCancellation.AffineModification.V

6. lemma OAI.ComplexCancellation.AffineModification.fixed_V_of_positive_invariant line 117