OAI/AlgebraicGeometry/CommutingDerivations/ExtendedExtraPartials.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Ordinary partial derivatives in the unused variables agree with the corresponding localized coordinate derivatives and descend without a clearing factor.

  1. theorem OAI.AbhyankarSathaye.CommutingDerivations.pderiv_sumAlgEquiv_symm line 14
  2. theorem OAI.AbhyankarSathaye.CommutingDerivations.splitAmbient_extra_pderiv line 21
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedLocMap_extra_pderiv line 34
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv_extra_pderiv line 43
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.localized_extra_is_ordinary_partial line 58

    Source documentation

    The transported derivative indexed by an added coordinate agrees exactly with the ordinary partial derivative in the full original n-variable ring.

    theorem localized_extra_is_ordinary_partial {n : ℕ} (hn : 4 ≤ n)
    (i : Fin (n-4)) (p : MvPolynomial (Fin n) ℂ) :
    localizedPartial (extendedLocalizationEquiv hn) (blocksToOutput hn (Sum.inl i))
        (extendedLocMap hn p) =
      extendedLocMap hn (pderiv (blocksToAmbient hn (Sum.inl i)) p) := by
…

    Mentions: OAI.AbhyankarSathaye.p, OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial, OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv, OAI.AbhyankarSathaye.blocksToOutput, OAI.AbhyankarSathaye.CommutingDerivations.extendedLocMap, OAI.AbhyankarSathaye.blocksToAmbient