[Merged by Bors] - feat(ring_theory/derivation): A presentation of the Kähler differential module #17011
Conversation
erdOne
added
awaiting-review
There was a problem hiding this comment.
Can you please add some docstring? Also, it would be nice to have a final theorem, saying that the Kähler differential module is isomorphic to S →₀ S / ker_total. The best way to state this would be to prove that it satisfies the universal property, but I am not sure we have it. In any case, the final result should be added as a "main result" at the beginning of the file.
There was a problem hiding this comment.
I think you can add a TODO saying that we want a characteristic predicate is_kaehler_differential (the universal property) and the fact that the two (isomorphic) modules satisfy it. I am afraid we will suffer if we do things for a particular definition.
Also, can you please add a description of the PR?
src/ring_theory/derivation.lean
Outdated
| ← linear_map.map_smul_of_tower, finsupp.smul_single, mul_comm, algebra.smul_def], | ||
| end | ||
|
|
||
| /-- (Implementation) An auxiliary definition for `kaehler_differential.ker_total_eq`. -/ |
There was a problem hiding this comment.
I don't think this is an implementation detail: it is the universal derivation after all (if this were the definition of Kaehler differential)
There was a problem hiding this comment.
This is because the intended way to use this result is to treat Ω[S⁄R] as the quotient (using total_surjective and ker_total) instead of reasoning with the quotient module and then transferring the result using an equivalence; not least because the "transferring" part is math-trivial but (usually) lean-tedious.
That said, there is an argument to be made that we (being a library) should provide all things we could, and let the user decide how they would like to use them.
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
…al module (#17011) We add an alternative description of `Ω[S⁄R]`, presenting it as `S` copies of `S` with kernel generated by the relations: 1. `dx + dy = d(x + y)` 2. `x dy + y dx = d(x * y)` 3. `dr = 0` for `r ∈ R` Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
We add an alternative description of
Ω[S⁄R], presenting it asScopies ofSwith kernel generated by the relations:dx + dy = d(x + y)x dy + y dx = d(x * y)dr = 0forr ∈ R