[Merged by Bors] - feat(RingTheory/Derivation): define `Differential` and `DifferentialAlgebra` typeclasses by Command-Master · Pull Request #14699 · leanprover-community/mathlib4

Command-Master · 2024-07-13T04:46:35Z

Define a typeclass Differential of CommRings with a chosen Derivation, a notation for that derivation, and a DifferentialAlgebra for Algerbas on differential rings whose algebraMap commutes with the derivation.

github-actions · 2024-07-13T04:47:14Z

PR summary 487dac828a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Derivation.DifferentialRing`	965

Declarations diff

+ Differential
+ Differential.ContainConstants
+ Differential.equiv
+ DifferentialAlgebra
+ DifferentialAlgebra.equiv
+ algebraMap.coe_deriv
+ delabDeriv
+ instance (A : Type*) [CommRing A] [Differential A] : Differential.ContainConstants A A
+ instance (A : Type*) [CommRing A] [Differential A] : DifferentialAlgebra A A
+ mem_range_of_deriv_eq_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for `script/declarations_diff.sh` contains some details about this script.

Command-Master · 2024-07-13T04:54:53Z

Is there a problem with the instance I add?

erdOne · 2024-07-14T02:44:55Z

Do you plan to add more results about this? Please move it into a new file in that case.

Command-Master · 2024-07-14T03:53:12Z

Do you plan to add more results about this? Please move it into a new file in that case.

A few more, proving that AlgHoms commute with the derivative in some cases. What's a good name for this file?

erdOne · 2024-07-14T04:09:55Z

RingTheory/Derivation/DifferentialRing or RingTheory/DifferentialRing both makes sense IMO.

Mathlib/Topology/ContinuousFunction/UniqueCFC.lean

erdOne · 2024-07-14T15:32:55Z

Mathlib/RingTheory/Derivation/DifferentialRing.lean

+/--
+A `CommRing` with a bundled `Derivation` to itself.
+-/
+class CommDifferentialRing (R : Type*) extends CommRing R where


Are there any non-commutative CommDifferentialRings?

I'm not aware of any, the existing definition of Derivation requires commutativity, and Wikipedia defines it with commutativity, but I don't know differential algebra well enough to tell for sure.

Would you ever want to consider multiple differential-ring structures on the same ring (maybe multiple partial derivatives)? If so, I would suggest class DifferentialRing (R : Type*) [CommRing R] where instead.

You could have multiple (d1 d2 : DifferentialRing R) lying around, like how mathlib deals with multiple topologies on a type. Also you wouldn't be able to declare differential fields with this bundled approach.

I would (and do, in #14860), they just extend both CommDifferentialRing and Field

I tried to change it, what do you think? It's nicer in some ways, but it also requires writing more typeclass assumptions

Mathlib/RingTheory/Derivation/DifferentialRing.lean

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/RingTheory/Derivation/DifferentialRing.lean

erdOne · 2024-07-18T07:06:10Z

Mathlib/RingTheory/Derivation/DifferentialRing.lean

+/--
+A `CommRing` with a bundled `Derivation` to itself.
+-/
+class CommDifferentialRing (R : Type*) extends CommRing R where


Would you ever want to consider multiple differential-ring structures on the same ring (maybe multiple partial derivatives)? If so, I would suggest class DifferentialRing (R : Type*) [CommRing R] where instead.

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Command-Master · 2024-07-18T07:17:56Z

How would class DifferentialRing (R : Type*) [CommRing R] where help for having multiple derivatives?

Mathlib/RingTheory/Derivation/DifferentialRing.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

jcommelin

My apologies for the delay in reviewing. Holiday season etc...

I think this looks good now.

bors merge

…lgebra` typeclasses (#14699) Define a typeclass `Differential` of `CommRing`s with a chosen `Derivation`, a notation for that derivation, and a `DifferentialAlgebra` for `Algerba`s on differential rings whose `algebraMap` commutes with the derivation. Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

mathlib-bors · 2024-08-23T04:06:38Z

Pull request successfully merged into master.

Build succeeded:

…lgebra` typeclasses (#14699) Define a typeclass `Differential` of `CommRing`s with a chosen `Derivation`, a notation for that derivation, and a `DifferentialAlgebra` for `Algerba`s on differential rings whose `algebraMap` commutes with the derivation. Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

Add bundled differential rings and algberas

f5ecd0d

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 13, 2024

Command-Master added the t-algebra Algebra (groups, rings, fields, etc) label Jul 13, 2024

increase synth instance time

7d35fb3

Export deriv_algebraMap

fd308f9

Command-Master added 2 commits July 14, 2024 07:31

Move file

71f6141

golf

6e65f24

Command-Master changed the title ~~feat(RingTheory/Derivation/Basic): define bundled CommDifferentialRing and DifferentialAlgebra~~ feat(RingTheory/Derivation): define bundled CommDifferentialRing and DifferentialAlgebra Jul 14, 2024

erdOne reviewed Jul 14, 2024

View reviewed changes

Command-Master and others added 2 commits July 14, 2024 19:38

Apply suggestions from code review

80919b1

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Test

4147685

Command-Master requested a review from erdOne July 16, 2024 09:20

Command-Master added 3 commits July 18, 2024 09:05

Add SharedConstants

85522ea

Merge branch 'master' into CommandMaster_diffring

6ef60d5

SharedConstants rfl

d64315a

Command-Master mentioned this pull request Jul 18, 2024

[Merged by Bors] - feat(Mathlib/FieldTheory): define differential fields #14860

Closed

2 tasks

erdOne reviewed Jul 18, 2024

View reviewed changes

Update Mathlib/RingTheory/Derivation/DifferentialRing.lean

a121966

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Command-Master added 3 commits July 18, 2024 10:19

Apply suggestions from code review

0090899

Rename

32aea5d

Merge branch 'master' into CommandMaster_diffring

7e5d284

Command-Master mentioned this pull request Jul 21, 2024

[Merged by Bors] - feat(RingTheory/Derivation/MapCoeffs): define mapCoeffs on a differential ring #14967

Closed

4 tasks

Change

03e1cda

Command-Master requested a review from erdOne July 23, 2024 03:15

Command-Master added 2 commits July 23, 2024 06:50

Fix

7628b7d

style

1dbf7c7

Command-Master changed the title ~~feat(RingTheory/Derivation): define bundled CommDifferentialRing and DifferentialAlgebra~~ feat(RingTheory/Derivation): define Differential and DifferentialAlgebra typeclasses Jul 26, 2024

jcommelin reviewed Jul 29, 2024

View reviewed changes

Mathlib/RingTheory/Derivation/DifferentialRing.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Derivation/DifferentialRing.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Derivation/DifferentialRing.lean Outdated Show resolved Hide resolved

Command-Master and others added 2 commits July 29, 2024 11:35

Apply suggestions from code review

2e161f6

Co-authored-by: Johan Commelin <johan@commelin.net>

Update DifferentialRing.lean

487dac8

jcommelin reviewed Aug 23, 2024

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Aug 23, 2024

mathlib-bors bot changed the title ~~feat(RingTheory/Derivation): define Differential and DifferentialAlgebra typeclasses~~ [Merged by Bors] - feat(RingTheory/Derivation): define Differential and DifferentialAlgebra typeclasses Aug 23, 2024

mathlib-bors bot closed this Aug 23, 2024

mathlib-bors bot deleted the CommandMaster_diffring branch August 23, 2024 04:06

Conversation

Command-Master commented Jul 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 487dac828a

Import changes for modified files

Declarations diff

Uh oh!

Command-Master commented Jul 13, 2024

Uh oh!

erdOne commented Jul 14, 2024

Uh oh!

Command-Master commented Jul 14, 2024

Uh oh!

erdOne commented Jul 14, 2024

Uh oh!

Uh oh!

erdOne Jul 14, 2024

Choose a reason for hiding this comment

Uh oh!

Command-Master Jul 14, 2024

Choose a reason for hiding this comment

Uh oh!

erdOne Jul 18, 2024

Choose a reason for hiding this comment

Uh oh!

erdOne Jul 21, 2024

Choose a reason for hiding this comment

Uh oh!

Command-Master Jul 21, 2024

Choose a reason for hiding this comment

Uh oh!

Command-Master Jul 23, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

erdOne Jul 18, 2024

Choose a reason for hiding this comment

Uh oh!

Command-Master commented Jul 18, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Aug 23, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Command-Master commented Jul 13, 2024 •

edited

Loading

github-actions bot commented Jul 13, 2024 •

edited

Loading