OAI/AlgebraicGeometry/CommutingDerivations/LocalizedPartials.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transport the actual coordinate partials through a specified, proved algebra equivalence. Coefficients in the whole relative coefficient algebra are fixed, even when the derivations are viewed over a smaller ground ring.

  1. def OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial line 15
  2. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial_apply line 18
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial_locallyNilpotent line 21
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartials_commute line 25
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial_fixes_relative line 30
  6. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial_coordinate line 34
  7. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartial_kernel line 39
  8. theorem OAI.AbhyankarSathaye.CommutingDerivations.localizedPartials_common_kernel line 48