[Merged by Bors] - feat: relative differentials as a presheaf of modules #14014

joelriou · 2024-06-21T11:12:01Z

In this PR, we define the type M.Derivation φ of derivations with values in a presheaf of R-modules M relative to
a morphism of φ : S ⟶ F.op ⋙ R of presheaves of commutative rings over categories C and D that are related by a functor F : C ⥤ D. In the particular case F is the identity functor, we construct the universal derivation.

depends on: [Merged by Bors] - feat: differentials as an object in ModuleCat #14030

This is a refactor of #11570

github-actions · 2024-06-21T11:12:38Z

PR summary ec03e2a468

Import changes

No significant changes to the import graph

Declarations diff

+ Derivation
+ HasDifferentials
+ Universal
+ Universal.mk
+ app
+ app_apply
+ congr_d
+ d_app
+ d_one
+ derivation'
+ instance : HasDifferentials (F := 𝟭 D) φ' := ⟨_, _, ⟨isUniversal' φ'⟩⟩
+ instance : Subsingleton d.Universal
+ isUniversal'
+ mk
+ mk_app
+ postcomp
+ relativeDifferentials'
+ relativeDifferentials'BundledCore
+ relativeDifferentials'_map_apply
+ relativeDifferentials'_map_d
+ relativeDifferentials'_obj

You can run this locally as follows

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

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

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…om:leanprover-community/mathlib4 into presheaf-of-modules-relative-differentials

…nto presheaf-of-modules-relative-differentials

leanprover-community-mathlib4-bot · 2024-06-24T14:20:20Z

This PR/issue depends on:

~~[Merged by Bors] - feat: differentials as an object in ModuleCat #14030~~
By Dependent Issues (🤖). Happy coding!

…ve-differentials

Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

erdOne · 2024-06-25T12:20:24Z

Thanks!
maintainer merge

github-actions · 2024-06-25T12:20:36Z

🚀 Pull request has been placed on the maintainer queue by erdOne.

jcommelin · 2024-06-25T14:40:11Z

Thanks 🎉

bors merge

In this PR, we define the type `M.Derivation φ` of derivations with values in a presheaf of `R`-modules `M` relative to a morphism of `φ : S ⟶ F.op ⋙ R` of presheaves of commutative rings over categories `C` and `D` that are related by a functor `F : C ⥤ D`. In the particular case `F` is the identity functor, we construct the universal derivation. Co-authored-by: Joël Riou <[email protected]>

kbuzzard

All the lean looks fine to me but I would like to be able to understand the module docstring better :-)

kbuzzard · 2024-06-25T14:44:50Z

Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

+with values in a presheaf of `R`-modules `M` relative to
+a morphism of `φ : S ⟶ F.op ⋙ R` of presheaves of commutative rings
+over categories `C` and `D` that are related by a functor `F : C ⥤ D`.
+We formalize the notion of universal derivation.


Trying to read this first paragraph, I found myself not knowing what S was, and actually I'm still confused mathematically. If F : C => D then F.op >>> R is a presheaf of rings on D,and I'm guessing that S is a scheme because that's what it is in the next paragraph, and now I don't know what kind of object phi is supposed to be. Please feel free to add explanations so that I understand the first paragraph :-)

kbuzzard · 2024-06-25T14:45:08Z

Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

+
+Geometrically, if `f : X ⟶ S` is a morphisms of schemes (or more generally
+a morphism of commutative ringed spaces), we would like to apply
+these definitions in the case where `F` is the pullback functors from


Suggested change

these definitions in the case where `F` is the pullback functors from

these definitions in the case where `F` is the pullback functor from

kbuzzard · 2024-06-25T14:45:44Z

Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

+rings `φ' : S' ⟶ R`, we construct a derivation
+`DifferentialsConstruction.derivation'` which is universal.
+Then, the general case (TODO) shall be obtained by observing that
+derivations for `S ⟶ F.op ⋙ R` identify to derivations


Suggested change

derivations for `S ⟶ F.op ⋙ R` identify to derivations

derivations for `S ⟶ F.op ⋙ R` identify with derivations

mathlib-bors · 2024-06-25T14:51:17Z

Pull request successfully merged into master.

Build succeeded:

In this PR, we define the type `M.Derivation φ` of derivations with values in a presheaf of `R`-modules `M` relative to a morphism of `φ : S ⟶ F.op ⋙ R` of presheaves of commutative rings over categories `C` and `D` that are related by a functor `F : C ⥤ D`. In the particular case `F` is the identity functor, we construct the universal derivation. Co-authored-by: Joël Riou <[email protected]>

feat: relative differentials of a presheaf of modules

1deb982

wip

295e945

joelriou changed the title ~~feat: relative differentials of a presheaf of modules~~ feat: relative differentials as a presheaf of modules Jun 21, 2024

joelriou mentioned this pull request Jun 21, 2024

feat: absolute differentials of a presheaf of rings #11570

Closed

1 task

joelriou added 2 commits June 21, 2024 14:21

wip

61104fd

wip

2c46459

github-actions bot reviewed Jun 21, 2024

View reviewed changes

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean Outdated Show resolved Hide resolved

joelriou and others added 5 commits June 21, 2024 17:06

fixing the build

3852398

Update Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

6e8e935

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

cleaning up

53ef31a

new file ModuleCat/Differentials/Basic.lean

d2d73b6

moved lemmas

71e7326

joelriou added t-category-theory Category theory t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry awaiting-review labels Jun 21, 2024

fixed comment

d1acf43

joelriou added WIP Work in progress and removed awaiting-review labels Jun 22, 2024

joelriou added 4 commits June 22, 2024 14:34

universal property

9735afd

Merge branch 'presheaf-of-modules-relative-differentials' of github.c…

673b878

…om:leanprover-community/mathlib4 into presheaf-of-modules-relative-differentials

cleaning up

d60a13e

feat: differentials as an object in ModuleCat

0adb1f0

joelriou removed the WIP Work in progress label Jun 22, 2024

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 22, 2024

joelriou and others added 4 commits June 22, 2024 15:26

added docstring

dc489ba

added docstring

b62888a

Update Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean

1632ed1

Merge remote-tracking branch 'origin/modulecat-differentials-basic' i…

e8447ac

…nto presheaf-of-modules-relative-differentials

joelriou added 2 commits June 24, 2024 09:31

fix

22a9b26

Merge remote-tracking branch 'origin/modulecat-differentials-basic' i…

18a9e66

…nto presheaf-of-modules-relative-differentials

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 24, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 24, 2024

Merge remote-tracking branch 'origin' into presheaf-of-modules-relati…

7f19518

…ve-differentials

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 24, 2024

joelriou added the awaiting-review label Jun 24, 2024

erdOne reviewed Jun 25, 2024

View reviewed changes

erdOne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 25, 2024

added Subsingleton instance and more API for Derivation'

ec03e2a

joelriou added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 25, 2024

github-actions bot removed the awaiting-CI label Jun 25, 2024

github-actions bot added the maintainer-merge label Jun 25, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 25, 2024

kbuzzard approved these changes Jun 25, 2024

View reviewed changes

mathlib-bors bot changed the title ~~feat: relative differentials as a presheaf of modules~~ [Merged by Bors] - feat: relative differentials as a presheaf of modules Jun 25, 2024

mathlib-bors bot closed this Jun 25, 2024

mathlib-bors bot deleted the presheaf-of-modules-relative-differentials branch June 25, 2024 14:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: relative differentials as a presheaf of modules #14014

[Merged by Bors] - feat: relative differentials as a presheaf of modules #14014

joelriou commented Jun 21, 2024 •

edited

Loading

github-actions bot commented Jun 21, 2024 •

edited

Loading

Declarations diff

leanprover-community-mathlib4-bot commented Jun 24, 2024

erdOne commented Jun 25, 2024

github-actions bot commented Jun 25, 2024

jcommelin commented Jun 25, 2024

kbuzzard left a comment

kbuzzard Jun 25, 2024

kbuzzard Jun 25, 2024

kbuzzard Jun 25, 2024

mathlib-bors bot commented Jun 25, 2024

	these definitions in the case where `F` is the pullback functors from
	these definitions in the case where `F` is the pullback functor from

	derivations for `S ⟶ F.op ⋙ R` identify to derivations
	derivations for `S ⟶ F.op ⋙ R` identify with derivations

[Merged by Bors] - feat: relative differentials as a presheaf of modules #14014

[Merged by Bors] - feat: relative differentials as a presheaf of modules #14014

Conversation

joelriou commented Jun 21, 2024 • edited Loading

github-actions bot commented Jun 21, 2024 • edited Loading

PR summary ec03e2a468

Import changes

Declarations diff

leanprover-community-mathlib4-bot commented Jun 24, 2024

erdOne commented Jun 25, 2024

github-actions bot commented Jun 25, 2024

jcommelin commented Jun 25, 2024

kbuzzard left a comment

Choose a reason for hiding this comment

kbuzzard Jun 25, 2024

Choose a reason for hiding this comment

kbuzzard Jun 25, 2024

Choose a reason for hiding this comment

kbuzzard Jun 25, 2024

Choose a reason for hiding this comment

mathlib-bors bot commented Jun 25, 2024

joelriou commented Jun 21, 2024 •

edited

Loading

github-actions bot commented Jun 21, 2024 •

edited

Loading