[Merged by Bors] - feat(ring_theory/derivations): stab on derivations

[Nicknamen]

---

Temporary stab on derivations. I will write myself the definitive definition as soon as bimodules will be there.

[Vierkantor]

Thank you for the PR!

I would have preferred it if you submitted three different PRs, one for cancel_monoid, one for compat_semimodule and one for derivation. Together they are still small enough, so I can review them.

[Vierkantor]

Sorry for noticing it later on: could you move ring_theory/derivations.lean to ring_theory/derivation.lean? Files generally don't use a plural.

[ocfnash]

I'm delighted to see this work taking shape but I wonder if bundling derivations into a structure is the best approach. I came here to comment that, mathematically, what is really being proved in derivation.commutator is that the derivations form a Lie subalgebra of the linear endomorphisms of the algebra A. But when I tried to drop in a proof of this I realised that because derivations are bundled I couldn't even state this fact!

Unfortunately I am running late for an appointment so I haven't time to finish this but here's another approach that might be worth considering:

-- Test this out by dropping it in at the end of your final section.

def is_derivation (D : A →ₗ[R] M) := ∀ ⦃a b⦄, D (a * b) = (a • D b) + (b • D a)

lemma is_derivation.eq (D : A →ₗ[R] M) (h : is_derivation D) :
  ∀ {a b}, D (a * b) = (a • D b) + (b • D a) := h

def submodule : submodule R (module.End R A) :=
{ carrier   := is_derivation,
  zero_mem' := λ a b, by simp,
  add_mem'  := λ a b ha hb, by sorry,
  smul_mem' := λ c a ha, by sorry, }

def lie_subalgebra : lie_subalgebra R (module.End R A) :=
{ lie_mem := λ D₁ D₂ h₁ h₂ a b, by { -- Awful proof but haven't time to fix.
    simp only [lie_ring.of_associative_ring_bracket,
      id.smul_eq_mul, linear_map.mul_app, linear_map.sub_apply],
    rw [h₁, h₂],
    simp only [id.smul_eq_mul, linear_map.map_add],
    rw [h₁, h₂, h₁, h₂],
    simp only [id.smul_eq_mul],
    ring, },
  ..submodule }

You should have a bit less work to do this way because module and Lie algebra structures will be automatically induced and I expect it will be very useful later to know not just that the derivations form a module / Lie algebra but actually submodule / Lie subalgebra.

[Nicknamen]

Hi Oliver, thanks for commenting! I am perfectly aware of this problem (I was also when I did define derivations) and it actually arose before in the topology and geometry sections of the library with continuous and smooth bundled maps, where it is not possible to treat eg continuous maps valued in a group as a subgroup of all maps (see #3446). However, in order to define the Lie algebra of a Lie group I defined vector fields as derivations over the algebra of smooth maps valued in the field (next PR), and for consistency in that section of the library and for it to properly work the only possible implementation of vector fields is as structures (regardless of how the structure is defined I believe it needs to be a structure: is_vector_field would not fit very well in my opinion). This having been said I totally see your point and I agree that for the purpose itself of the algebra section of the library this is not a good way to implement it. What we can do, if you agree it could be a good idea, is to have both implementations existing and working, as it happens in many other parts of the library (such as linear maps, continuous maps, smooth maps). If you prefer, I can write in the introductory part of the documentation to implement is_derivation as TODO and encourage to use is_derivation instead of derivation for the algebra section. Note that one year ago, Kenny Lau also implemented derivations as a structure so I imagine he possibly also had in mind a double implementation like this.

Maybe there is a way to do state things for bundled derivations in the algebra section as well though (https://leanprover.zulipchat.com/login/#narrow/stream/113488-general/topic/Making.20a.20type.20a.20.22subtype.22.20of.20another might be relevant for the case of continuous functions: could we do something in the same style?)

[ocfnash]

Thanks for such a comprehensive reply @Nicknamen I now understand that you had already carefully considered the bundled vs. unbundled approach.

I like the approach of defining the bracket on vector fields by identifying them with the derivations as a Lie subalgebra of the linear endomorphisms of the smooth functions (I guess this uses Hadamard's Lemma?). I am a little surprised that you find an unbundled approach to derivations would not work well there but I confess I have not seen that work or thought much about it.

It may well be that we need both the bundled and unbundled approaches (together with the machinery to plumb these together). If this turns out to be the case then I would advocate defining the module and Lie algebra structures on derivations via their submodule and Lie subalgebra structures using the unbundled definitions. Still, I appreciate I'm not in the weeds here so I am more than happy to leave this up to you.

I mostly just wanted to make sure these ideas were being considered and I now know they are. Thanks again for doing all this excellent work.

[Nicknamen]

Ok I believe this is pretty much ready on my side. I replaced compatible_semimodule with is_scalar_tower.

[Nicknamen]

The last commit I pushed will not compile but is there just to illustrate a refactor I could include with this PR. Everything there compiles up to the file ring_theory.algebra. Some of the lemmas that were proved for restrict_scalars are true for the general case of a scalar tower. What I did was to write an instance of is_scalar_tower for the restrict_scalars case and delete some lemmas of restrict_scalars to use only the is_scalar_tower version. However now Lean cannot resolve type class inference well as before, and in order to find the correct instances one now needs to specify the arguments of lemmas. It will not anymore be sufficient to write rw lemma_name but one will have to write rw lemma_name a b c. Should I go on with this refactor? Do we want this or is it better to keep both versions of lemmas there?

[Nicknamen]

Also, there are three pending changes that I did not apply because I would like to discuss them further!

[Nicknamen]

The last commit I pushed will not compile but is there just to illustrate a refactor I could include with this PR. Everything there compiles up to the file ring_theory.algebra. Some of the lemmas that were proved for restrict_scalars are true for the general case of a scalar tower. What I did was to write an instance of is_scalar_tower for the restrict_scalars case and delete some lemmas of restrict_scalars to use only the is_scalar_tower version. However now Lean cannot resolve type class inference well as before, and in order to find the correct instances one now needs to specify the arguments of lemmas. It will not anymore be sufficient to write rw lemma_name but one will have to write rw lemma_name a b c. Should I go on with this refactor? Do we want this or is it better to keep both versions of lemmas there?

Well this seems to happen just for the lemma semimodule.restrict_scalars_smul_def. I believe a good compromise could be to include this lemma only. In any case I believe the best thing is to remove semimodule.restrict_scalars from mathlib and substitute it with is_scalar_tower: in abstract lemmas it should be no problem to require these two additional instances and in practical examples, it should be always possible to define such instances. Should I propose this in Zulip?

[Vierkantor]

Refactoring restrict_scalars (i.e. deleting them) sounds like a good idea to me! Let's make a new PR for that and focus on derivations in this one, so we can merge it soon. I have some time now to do a review if you are ready for it.

[Nicknamen]

A review of derivations? Yeah sure I'd merge this first so that I can go on with the other PRs I have in cue! I am not sure it is best to review this before mathlib build succeeds, but if you don't mind go ahead! In any case we could start by resolving the three points from the previous review that are still open!

[Nicknamen]

Ok mathlib built so feel free to go on with the next review!

[Vierkantor]

Just one extra comment, apart from those comments everything looks good to me!

[Vierkantor]

Thanks for the fixes!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests