Generalizing Derivation module

Stream: mathlib4

[Reklle]

Hello everyone! While studying the Derivation module, I noticed opportunities for some natural generalizations.

The current structure limitations:

1. Restricted to commutative algebras
2. The 2020 TODO about bimodules remains unresolved
3. Lacks support for graded derivations
4. There are no inner derivations and related theory

Would this be valuable for mathlib? What other ideas and suggestions will there be?

I'm a third-year physics student and this seems like an ideal summer project for me. I am ready to take on the implementation.

Best regards,
Kirill Ferediakin

[Eric Wieser]

I attempted point 2 back in !3#18936, in case that's of interest

[Eric Wieser]

I don't think we can make progress on that without #7152

[Eric Wieser]

I think maybe the first step here is to add op_nsmul and op_zsmul fields to additive monoids and additive groups?

[张守信(Shouxin Zhang)]

In the process of formalizing DifferentialGradedAlgebra, we encountered a situation where the standard definition of a derivation, which implicitly assumes commutativity for the product rule, was insufficient. This is because multiplication in exterior algebra is non-commutative (specifically, anti-commutative).

I'm wondering if there's some easy way in the short term to define a non-commutative derivative so that the definition we need doesn't fail due to commutativity. :face_with_spiral_eyes:

[Kenny Lau]

@张守信(Shouxin Zhang) What's the mathematical definition?

[Robin Carlier]

How about defining differential graded (A-)algebras as algebra objects in the monoidal category of chain complexes of A-modules? I guess there will need a lot of unfolding to do to get the operations, but here the anticommutativity is "baked in" the sign rules for the tensor product of chain complexes.

[Kenny Lau]

What is the mathematical definition?

[Robin Carlier]

What I wrote above is a mathematical definition. Or perhaps you're unhappy with the term "Algebra object"? To me, this is synonym to "Monoid object internal to a monoidal category".

[Robin Carlier]

(The point of view of monoids in the category of chain complexes is also more suited to study the homotopy theory of (commutative) dg-algebras, i.e the localization of this category at the class of weak equivalences given by morphisms that induce a quasi-isomorphism of the underlying chain complexes)

[张守信(Shouxin Zhang)]

Kenny Lau said:

张守信(Shouxin Zhang) What's the mathematical definition?

Our def of math is as follow
image.png

The lean code is

import Mathlib

section DGA

variable {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (𝓐 : ℤ → Submodule R A)

class DifferentialGradedAlgebra [GradedAlgebra 𝓐] where
  deriv : Derivation R A A
  deriv_isHomogeneous {n : ℤ} (a : 𝓐 n) : deriv a ∈ 𝓐 (n - 1)

end DGA

variable {R : Type u} [CommRing R] {L : Type v} [AddCommGroup L] [Module R L]

variable (R) (L) in
def exteriorIntGrading : ℤ → Submodule R (ExteriorAlgebra R L) := fun i =>
  match i with
  | Int.ofNat i => ⋀[R]^i L
  | Int.negSucc _ => 0

instance : GradedAlgebra (fun i : ℕ ↦ ⋀[R]^i L) := ExteriorAlgebra.gradedAlgebra R L

instance : SetLike.GradedMonoid (exteriorIntGrading R L) where
  one_mem := by simp [exteriorIntGrading]
  mul_mem := by
    unfold exteriorIntGrading
    intro i j gi gj hgi hgj
    cases i with
    | ofNat i =>
      cases j with
      | ofNat j =>
        simp only at hgi hgj
        exact SetLike.mul_mem_graded hgi hgj
      | negSucc j => simp_all
    | negSucc i => simp_all

instance : GradedAlgebra (exteriorIntGrading R L) := by
  apply GradedAlgebra.ofAlgHom _ ?_ ?_ ?_
  . apply AlgHom.comp ?_ (GradedAlgebra.liftι R L)
    refine DirectSum.toAlgebra _ _ (fun i => ?_) ?_ ?_
    . exact (DirectSum.lof R ℤ (fun i => ↥(exteriorIntGrading R L i)) (Int.ofNat i)).comp <|
        Submodule.inclusion (by rfl)
    . simp only [Int.ofNat_eq_coe, Int.cast_ofNat_Int, LinearMap.coe_comp, Function.comp_apply]
      rfl
    . intro i j ai aj
      dsimp only [Int.ofNat_eq_coe, Int.natCast_add, LinearMap.coe_comp, Function.comp_apply]
      sorry
  .
    sorry
  .
    sorry

-- instance (f : L →ₗ[R] R) : DifferentialGradedAlgebra (R := R) (A := (ExteriorAlgebra R L)) (exteriorIntGrading R L):= by sorry

Here, in the final part, we need R is CommRing.

[Reklle]

@张守信(Shouxin Zhang) If there are no other options, perhaps it is worth writing a temporary module for

$$d : A \to A$$

[Kevin Buzzard]

Our def of math is as follow

What is an algebra over a non-commutative ring? (re "a graded algebra A over R")

[Kenny Lau]

Kevin Buzzard said:

Our def of math is as follow

What is an algebra over a non-commutative ring? (re "a graded algebra A over R")

I believe they might have meant a non-commutative algebra over a commutative ring

[张守信(Shouxin Zhang)]

Robin Carlier said:

What I wrote above is a mathematical definition. Or perhaps you're unhappy with the term "Algebra object"? To me, this is synonym to "Monoid object internal to a monoidal category".

I'm very sorry, but we do indeed need to work on a concrete definition at the moment. Therefore, the best solution for now might be to temporarily create a generalized version of a derivation as a substitute.

[张守信(Shouxin Zhang)]

Robin Carlier said:

How about defining differential graded (A-)algebras as algebra objects in the monoidal category of chain complexes of A-modules? I guess there will need a lot of unfolding to do to get the operations, but here the anticommutativity is "baked in" the sign rules for the tensor product of chain complexes.

To be honest, I don't know much about category theory. Previously, other students used a categorical API to prove that the derivative d of the Koszul complex satisfies d^2 = 0. I was responsible for porting this into a proof based on concrete definitions, under the guidance of other more experienced students. Therefore, I may not be able to answer your question. >_<

[Yongle Hu]

Kenny Lau 发言道：

Kevin Buzzard said:

Our def of math is as follow

What is an algebra over a non-commutative ring? (re "a graded algebra A over R")

I believe they might have meant a non-commutative algebra over a commutative ring

Yes, it is a non-commutative algebra over a commutative ring. Therefore, we only need to change the definition of docs#Derivation from

import Mathlib.Algebra.Polynomial.AlgebraMap

structure Derivation (R A M : Type*) [CommSemiring R] [CommSemiring A]
    [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M]
    extends A →ₗ[R] M where
  protected map_one_eq_zero' : toLinearMap 1 = 0
  protected leibniz' (a b : A) : toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a

to

import Mathlib.Algebra.Polynomial.AlgebraMap

structure Derivation (R A M : Type*) [CommSemiring R] [Semiring A]
    [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M]
    extends A →ₗ[R] M where
  protected map_one_eq_zero' : toLinearMap 1 = 0
  protected leibniz' (a b : A) : toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a

I think this will have little negative impact.

[Robin Carlier]

张守信(Shouxin Zhang) said:

Robin Carlier said:

How about defining differential graded (A-)algebras as algebra objects in the monoidal category of chain complexes of A-modules? I guess there will need a lot of unfolding to do to get the operations, but here the anticommutativity is "baked in" the sign rules for the tensor product of chain complexes.

To be honest, I don't know much about category theory. Previously, other students used a categorical API to prove that the derivative d of the Koszul complex satisfies d^2 = 0. I was responsible for porting this into a proof based on concrete definitions, under the guidance of other more experienced students. Therefore, I may not be able to answer your question. >_<

Both point of views (concrete & abstract categorical) are probably useful to have anyway (just like Mathlib has both algebras in unbundled form, and the equivalence between AlgCat A and Mon_ (ModuleCat A)). Since so far monoids in monoidal categories are bundled (I recall seeing a PR trying to have a type-class based version), this will also not play nice with your "defining everything as a class approach anyway"

I was asking about the abstract categorical definition because of what I wrote after in parenthesis, where the equivalent definition really pays off when one wants to look at the homotopy theory of cdgas (and hopefully, Mathlib will want some derived algebraic geometry, of which one flavor of is heavily using this homotopy theory, when the time will be ripe).

I also felt that it would be interesting to "get the formulas" out of the purely categorical definitions, which is most certainly possible, but I also looked a bit at it and Mathlib still needs a lot more infrastructure on its monoidal categories side to make this work anyways.

[Eric Wieser]

@Yongle Hu, that definition is not correct, you need to reverse the second multiplication. Please look at the in !3#18936 I linked for the correct version

[Eric Wieser]

In general, generalizing a definition requires more thought than just making the code compile

[Kevin Buzzard]

The nuclear approach is to refactor groups once again (giving monoids this opposite action of Nat) but I wonder whether this would give me easier access to the right module structure on a tensor product of modules? I'm finding that It's very convenient to just switch it on occasionally in API development.

[Eric Wieser]

I think we should do that nuclear approach

[Kevin Buzzard]

Before or after or at the same time as adding the PNat_smul field?

[Eric Wieser]

It's already justified elsewhere as without it we can't talk about TrivSqZeroExt Nat M for some additive monoids M.

[Eric Wieser]

And the more we generalize to two-sided actions, the less will work for Nat / int

[Matthew Ballard]

Other than duplication what was the thought process on LSMul and RSMul

[Eric Wieser]

That still needs the new field in AddMonoid, right?

[Eric Wieser]

I think ultimately that question is orthogonal to derivations, in that context it is at best a bikeshed about notation that we can revisit once we have a shed to paint.

[Matthew Ballard]

I think it depends on how set it up. I would imagine (with limited forethought) that central actions would get abstracted out as something that extends both with some compatibilities.

[Eric Wieser]

We already have central actions, docs#IsCentralScalar

[Eric Wieser]

But even if things are central, the right action has to come from somewhere, and you can't build it from the left action without creating a diamond.

[Matthew Ballard]

I agree. I think you will need some propositional compatibilities with each piece of data you add. But it would nice if it was one package that feeds directly into the existing typeclasses rather than having to retrofit each time.

It seems like [SMul M N] [SMul Mᵐᵒᵖ N] then trying to use the fact that "M and Mᵐᵒᵖ are the same" sets you up for trouble.

[Eric Wieser]

[SMul M N] [SMul Mᵐᵒᵖ N] [IsCentralScalar M N] works just fine today, the problem is that it is not currently satisfied by Algebra M N, or for M := Nat by AddMonoid N, or for M := Int by AddGroup N,

[Eric Wieser]

(It's satisfied mathematically, but we can't teach lean this is so without introducing new data fields)

[Eric Wieser]

I think you will need some propositional compatibilities with each piece of data you add.

Indeed, we need one of these in each of AddMonoid, AddGroup, and Algebra

[Matthew Ballard]

And [LeftSMul Nat A] [RightSMul Nat A] [IsCentralBiSMul Nat A] fails even worse for AddMonoid A since it is hallucinated and then isn't supported assuming some indulgence.

Perhaps I am the outlier but it this situation and in others it seems more natural to the human thought process to split the SMul typeclass than to continue with op-fication.

[Kevin Buzzard]

Yay let's have luMS M R, I think that's much more sensible than SMul R^{mop} M (apart from the silly name, that's obviously a bit less sensible but hopefully indicates what it's supposed to represent)

[Notification Bot]

30 messages were moved from this topic to #mathlib4 > Right actions on tensor products (again) by Eric Wieser.