Zulip Chat Archive

Is there a (commutative) ring with derivation? Here derivation means an operator D: R \to R satisfying Leibniz rule D(ab) = (Da)b + a(Db) and additive D(a+b) = Da + Db. While I was trying to add Wronskian for polynomials in mathlib4, I realized that Wronskian W(a,b) = a(Db) - (Da)b can be defined any ring with derivation and still satisfy nice properties, such as W(a, b) = W(b, c) when a + b + c = 0. cc. @Jineon Baek

Kevin Buzzard (Jun 27 2024 at 07:22):

There are many ways to search mathlib for things. Asking here is one way, but there are other ways which are sometimes far more efficient! For example if you go to the mathlib docs page https://leanprover-community.github.io/mathlib4_docs/index.html and type derivation into the search box, you will see about 20 functions all called Derivation.something . I'm sure you can take it from there :-) An alternative is using moogle which will also give you plenty of leads if you type derivation into the search box.

Let me know if I misunderstood your question.

Daniel Weber (Jun 27 2024 at 14:34):

I'm working on this right now, as part of a proof of Liouville's theorem, but I'm not sure if it's quite ready for Mathlib yet.
I'm using

class CommDifferentialRing (R : Type*) extends CommRing R where
  deriv : Derivation ℕ R R

postfix:max "′" => CommDifferentialRing.deriv

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.DFunLike.coe]
def delabDeriv : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity' ``DFunLike.coe 6
  guard <| (e.getArg!' 4).isAppOf' ``CommDifferentialRing.deriv
  let arg ← withAppArg delab
  `($arg′)

if it helps

Seewoo Lee (Jun 27 2024 at 14:44):

@Kevin Buzzard Thank you for pointing this out! I searched documentation first but I simply missed Derivation there for no reason..

Seewoo Lee (Jun 27 2024 at 14:45):

Also thanks @Daniel Weber for letting me know!

Seewoo Lee (Jun 27 2024 at 14:48):

Based on the current status, I think one way I can try to make a new file Wronskian.lean in RingTheory/Derivation directory and prove some properties there. This might be better than defining only for polynomial derivations (which is enough for our purpose though)

Seewoo Lee (Jun 28 2024 at 18:37):

We realized that the above property I mentioned (a + b + c = 0 => W(a, b) = W(b, c) actually holds for any anti-symmetric bilinear form, but I couldn't find the thing in from documentation or moogle. We tried to search with antisymm, anticomm, symplectic, ..., but couldn't locate any. Nothing under the directory BilinearForm too.