How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Universal Kähler differential module
Definition
Let be a homomorphism of commutative rings and let be the derivation functor of Derivation of an algebra. A Kähler differential module for is a pair consisting of a -module and an -derivation such that for every -module the assignment
is a bijection, and such that these bijections are natural in : for every -linear map the square
commutes. In other words, represents the covariant functor on -modules, and is the universal -derivation of over ; the element is the image of under it. Whether such a pair exists for a given is not part of the definition; when it does, the pair is uniquely determined up to a unique compatible isomorphism, as the next paragraph records.
Uniqueness. If and are both Kähler differential modules for the same ring map , the universal property of the first applied to the derivation produces a unique -linear with , and the property of the second applied to produces a unique -linear with . Then and , while the identity maps of and have the same property; the injectivity clause of the universal property applied twice gives and . So is an isomorphism with inverse , and is the only -linear map from to compatible with the two universal derivations. In particular is determined by the ring map up to canonical isomorphism, which is what justifies writing it as without further qualification.
Functoriality in ring maps. Given a commutative square of ring maps , , and , and universal pairs for its two horizontal maps, regard as a -module through . The composite is an -derivation: it is additive, satisfies Leibniz with this module action, and kills since the square commutes. Universality gives a unique -linear map sending to . For identity squares this is the identity; for composable squares the composite has the prescribed values on and so equals the map of the composite square by uniqueness. This proves functoriality in ring maps separately from naturality in the target module .
Depends on
Used by
Dependency tree · two levels
3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Stacks Algebra 10.131.2–3 (standard reference, not scraped)
- Vakil §22.2.17, p.582 (standard reference, not scraped)