Chapter 9. Derivations
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 13 definitions, 22 theorems, 2 lemmas, 3 examples, 1 counterexample, 4 constructions, 1 criterion and 2 other statements.
Of the 48 statements checked against Lean, 13 are formalized somewhere and 35 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 35 | 73% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 13 | 27% | Mathlib states and proves it. |
| checked in total | 48 |
- Canonical source block: FC13 Matsumura Chapter 9,
FC13-C09-U001–FC13-C09-U048, §§25–27, in canonical source-ID order from Foundational corpus units FC13 Matsumura. All 48 IDs are retrieved throughagent-memory, asserted once/in-order, and assigned exactly one route. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280. No project-owned derivation/Kähler/separability wrapper closes a C09 source unit more completely than pinned Mathlib, so C09 has noproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native C09 coverage is concentrated in derivations, trivial square-zero extensions, Kähler differentials and cotangent/Jacobi–Zariski sequences, formal smooth/unramified/étale maps, separable algebraic field extensions, linear disjointness, relative perfect closure, and the generic differential-basis universal property. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493(Lean 4.34.0-rc2). Targeted current/open searches for p-bases, differential ideals/Harper/Kimura–Niitsuma, and Hasse–Schmidt/iterative higher derivations found no compatible completed owner. GitHub-wide Lean-code searches likewise found no reusable source-level interfaces. - Strict bundle semantics were enforced. U002 is not credited from the Lie bracket without D^p being a derivation; U015 is not credited from
IsGeometricallyReducedbecause its own pinned TODO records missing arbitrary field-extension stability; U016 is not downgraded from arbitrary finite-dimensional algebras to finite field extensions; and the partial equivalence program inSeparablyGenerated.leandoes not earn U018–U021/U024. - The Kähler exact-sequence rows U009–U010 are native assemblies, not textual-name matches: pinned Jacobi–Zariski/conormal exactness plus formal-smooth H₁-vanishing and projectivity supply the stated injectivity and splitting clauses. For U010,
h1CotangentEquivCotangentidentifies the quotient cotangent module with H₁(B/A). U011 uses the presentation-level cotangent complex whose matrix entries are the evaluated partial derivatives. The U006 generator-spanning, U009/U010 injectivity, and U023 perfect-closure minimality assemblies were compile-checked against P in isolated Lean files before promotion. - Route totals for C09:
mathlib13,project-existing0,package-import0,reference-port0,unmatched35.
Definition: derivations and k-derivations
For an A-module M, Der(A,M) consists of additive maps D:A→M satisfying Leibniz. For a k-algebra A, Der_k(A,M) is the A-submodule of derivations vanishing on k; Der_k(A)=Der_k(A,A).
Formalized. Mathlib/RingTheory/Derivation/Basic.lean::Derivation, leibniz, map_algebraMap — Mathlib Derivation R A M is an R-linear additive map satisfying Leibniz; map_algebraMap is the vanishing-on-base condition, exactly Matsumura’s Der_k(A,M).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction: Lie bracket and p-th powers of derivations
Der_k(A) is a Lie algebra under [D,D′]=DD′−D′D. In characteristic p, D(a^p)=0 for every derivation and D^p is again a derivation.
Not formalized. Derivation/Lie.lean gives the commutator Lie algebra and leibniz_pow gives D(a^p)=0 in characteristic p, but no checked pinned/current/open declaration makes D^p an ordinary derivation or packages the whole characteristic-p row.
Definition: square-zero and trivial extensions
If N⊲B has N²=0 and A=B/N, then B is an extension of the k-algebra A by the A-module N. It is split when A→B admits a k-algebra section; the canonical trivial extension A*N has underlying module A⊕N and product (a,x)(a′,x′)=(aa′,ax′+a′x).
Formalized. Mathlib/Algebra/TrivSqZeroExt/Basic.lean::TrivSqZeroExt, fstHom, inlAlgHom, inr_mul_inr — TrivSqZeroExt A N is A⊕N with the source multiplication, projection, canonical section, and square-zero N-summand.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: difference of liftings is a derivation
For a square-zero extension B→A and two k-algebra liftings h,h′ of the same map C→A, h−h′ is a k-derivation C→N=ker(B→A); conversely h+D is another lifting for every such derivation.
Formalized. Mathlib/RingTheory/Derivation/ToSquareZero.lean::diffToIdealOfQuotientCompEq, derivationToSquareZeroOfLift, liftOfDerivationToSquareZero, derivationToSquareZeroEquivLift — derivationToSquareZeroEquivLift identifies derivations into the square-zero kernel with lifts of a fixed quotient map; its forward/backward maps are exactly h-h′ and h+D.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction: Kähler differentials and universal derivation
For a k-algebra A, with I=ker(A⊗kA→A), define Ω{A/k}=I/I² and d(a)=1⊗a−a⊗1 mod I². Then d is universal: Der_k(A,M)≅Hom_A(Ω_{A/k},M) naturally in M.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential, D, linearMapEquivDerivation — Pinned Mathlib defines Ω as the cotangent quotient of ker(S⊗_R S→S), defines the universal derivation D, and represents derivations by S-linear maps out of Ω.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example: differentials of generated and polynomial algebras
If A is generated over k by U then Ω_{A/k} is generated by {du:u∈U}. For A=k[X_1,…,X_n], Ω_{A/k} is free with basis dX_1,…,dX_n, and d f=Σ_i(∂f/∂X_i)dX_i.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::span_range_derivation, finite; Mathlib/RingTheory/Kaehler/Polynomial.lean::mvPolynomialBasis, mvPolynomialBasis_repr_apply, polynomial_D_apply — mvPolynomialBasis gives the free basis dX_i and mvPolynomialBasis_repr_apply identifies coefficients with partial derivatives. The generic spanning proof for Kähler differentials uses adjoin induction on algebra generators, exactly the source generator argument.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: 0-smooth, 0-unramified and 0-etale
A k-algebra A is 0-smooth if maps A→C/N lift across every square-zero ideal N; it is 0-unramified if such liftings are unique, and 0-etale if both existence and uniqueness hold. 0-unramified is equivalent to Ω_{A/k}=0.
Formalized. Mathlib/RingTheory/Smooth/Basic.lean::FormallySmooth, iff_comp_surjective; Mathlib/RingTheory/Unramified/Basic.lean::FormallyUnramified, iff_comp_injective, subsingleton_kaehlerDifferential; Mathlib/RingTheory/Etale/Basic.lean::FormallyEtale, iff_comp_bijective, iff_formallyUnramified_and_formallySmooth — The three pinned classes are exactly the square-zero existence, uniqueness, and bijective lifting conditions; formal unramifiedness is represented by Ω=0, matching Matsumura’s 0-terminology.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example: localisations are 0-etale
For any ring A and multiplicative set S, A_S is 0-etale over A.
Formalized. Mathlib/RingTheory/Etale/Basic.lean::FormallyEtale.of_isLocalization — Algebra.FormallyEtale.of_isLocalization proves every localization is formally étale over the source ring, exactly the row.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 25.1 (first fundamental exact sequence)
For k→A→B there is an exact sequence Ω_{A/k}⊗A B→Ω{B/k}→Ω_{B/A}→0. If B is 0-smooth over A, adding 0 on the left gives a split exact sequence.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::exact_mapBaseChange_map, map_surjective; Mathlib/RingTheory/Kaehler/JacobiZariski.lean::H1Cotangent.exact_map_δ, H1Cotangent.exact_δ_mapBaseChange; Mathlib/RingTheory/Smooth/Basic.lean::projective_kaehlerDifferential, subsingleton_h1Cotangent — The pinned Jacobi–Zariski sequence is Ω_A/k⊗_A B→Ω_B/k→Ω_B/A→0. If B/A is formally smooth, H₁(B/A)=0 makes the left map injective and projectivity of Ω_B/A splits the right surjection, giving the source split exact sequence.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 25.2 (second fundamental exact sequence)
For k→A→B=A/m, there is an exact sequence m/m²→Ω_{A/k}⊗A B→Ω{B/k}→0. If B is 0-smooth over k, the sequence is split exact.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::kerCotangentToTensor, exact_kerCotangentToTensor_mapBaseChange, mapBaseChange_surjective; Mathlib/RingTheory/Kaehler/JacobiZariski.lean::H1Cotangent.exact_map_δ, H1Cotangent.exact_δ_mapBaseChange; Mathlib/RingTheory/Extension/ExtendScalars.lean::h1CotangentEquivCotangent, cotangentComplex_comp_h1CotangentEquivCotangent; Mathlib/RingTheory/Smooth/Basic.lean::projective_kaehlerDifferential, subsingleton_h1Cotangent — For a quotient A→B=A/m, h1CotangentEquivCotangent identifies H₁(B/A) with m/m² and intertwines its Jacobi–Zariski connecting map with the conormal map. Formal smoothness of B/k kills H₁(B/k), so exactness makes the conormal map injective; projectivity of Ω_B/k splits the right surjection. This assembly was compile-checked against P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example: Jacobian presentation of Ω for quotient algebras
If B=k[X_1,…,X_n]/(f_1,…,f_m), then Ω_{B/k} is the quotient of the free B-module on dX_j by the submodule generated by df_i=Σ_j(∂f_i/∂X_j)dX_j.
Formalized. Mathlib/RingTheory/Extension/Cotangent/Basic.lean::exact_cotangentComplex_toKaehler, cotangentSpaceBasis, cotangentRestrict_mk — For a polynomial presentation, exact_cotangentComplex_toKaehler is the relations→free differentials→Ω sequence; cotangentRestrict_mk identifies the matrix entries with evaluated partial derivatives, exactly the Jacobian presentation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 25.3
If L/K is separable algebraic, then L is 0-etale over K. For any subfield k⊆K, Ω_{L/k}≅Ω_{K/k}⊗_K L.
Formalized. Mathlib/RingTheory/Etale/Field.lean::FormallyEtale.of_isSeparable; Mathlib/RingTheory/Etale/Kaehler.lean::tensorKaehlerEquivOfFormallyEtale — A separable algebraic field extension is formally étale at P, and the canonical tensor-Kähler equivalence gives Ω_{L/k}≃L⊗KΩ{K/k}, exactly Theorem 25.3.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 25.4
For a field K of characteristic p and nonzero D∈Der(K), the operators 1,D,…,D^{p−1} are K-linearly independent; a K-linear combination of them can be a derivation only with zero constant and all coefficients except that of D equal to zero.
Not formalized. Pinned/current/open searches found ordinary derivations and their Lie bracket but no source-shaped theorem for the linear independence of 1,D,…,D^{p-1} or Hochschild’s (aD)^p formula.
Theorem: Theorem 25.5 (Hochschild formula)
In characteristic p, for a∈A and D∈Der(A), (aD)p=apDp+(aD){p−1}(a)D.
Not formalized. Pinned/current/open searches found ordinary derivations and their Lie bracket but no source-shaped theorem for the linear independence of 1,D,…,D^{p-1} or Hochschild’s (aD)^p formula.
Definition: separable k-algebra
A k-algebra A is separable over the field k if A⊗_k k′ is reduced for every field extension k′/k. The property passes to subalgebras, is finitely generated-local on A, and is stable under field extension.
Not formalized. Algebra.IsGeometricallyReduced matches the source definition over a field and supports subalgebras/finitely-generated detection, but its pinned file explicitly lists arbitrary field-extension stability as TODO. The source row includes that clause, so strict bundle semantics leaves it unmatched.
Criterion: discriminant criterion for finite separable algebras
For finite-dimensional A/k, the discriminant det(tr_{A/k}(ω_iω_j)) is nonzero iff A is separable over k; vanishing/nonvanishing is independent of the chosen basis.
Not formalized. Pinned trace/discriminant theorems characterize separability for finite field extensions. Matsumura’s row is for an arbitrary finite-dimensional k-algebra under the geometrically-reduced notion; no checked route provides that full criterion.
Comparison: classical separable algebraic extensions are separable algebras
An algebraic field extension K/k that is separable in the usual polynomial-theoretic sense is separable as a k-algebra in the tensor-product sense of §26.
Not formalized. Pinned Mathlib formalizes classical algebraic separability and formal étaleness, but no checked declaration identifies arbitrary separable algebraic field extensions with IsGeometricallyReduced in the source sense; the needed arbitrary scalar-extension reducedness is not exported as a complete route.
Definition: separably generated extension
A field extension K/k is separably generated if it has a transcendence basis T such that K/k(T) is separable algebraic; T is then a separating transcendence basis.
Not formalized. SeparablyGenerated.lean proves existence statements involving separating transcendence bases but does not define the source predicate as a reusable interface; the row is therefore not mapped to a complete declaration.
Theorem: Theorem 26.1
Every separably generated field extension is separable.
Not formalized. SeparablyGenerated.lean explicitly describes the desired equivalences but does not prove this implication as a completed theorem.
Theorem: Theorem 26.2
For a finitely generated extension K/k in characteristic p, the following are equivalent: K/k is separable; K⊗_k k^{1/p} is reduced; K/k is separably generated.
Not formalized. The pinned SeparablyGenerated.lean header lists the source equivalences (separably generated, p-power linear independence, reduced tensor with k^{1/p}, geometrically reduced, linear disjointness), but states only one implication as its main result and leaves the iff as TODO.
Theorem: Theorem 26.3
If k is perfect, every field extension K/k is separable, and a k-algebra is separable iff it is reduced.
Not formalized. Pinned Mathlib proves finite-type extensions over perfect fields admit separating transcendence bases, but no checked theorem states that every extension is geometrically reduced or that every k-algebra is geometrically reduced iff reduced.
Definition: linear disjointness
Subfields K,K′ of a common field are linearly disjoint over k iff a k-linearly independent family in one remains independent over the other; equivalently K⊗_kK′→K[K′] is an isomorphism.
Formalized. Mathlib/FieldTheory/LinearDisjoint.lean::IntermediateField.LinearDisjoint, linearDisjoint_iff', linearIndependent_left; Mathlib/RingTheory/LinearDisjoint.lean::linearDisjoint_iff_injective, mulMap — Pinned linear-disjointness is defined by injectivity of the tensor-product multiplication map and is equivalent to preservation of linear independence, exactly the source definitions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction: p-power root towers and perfect closure
For characteristic p, k{p{-n}}={α:α{pn}∈k} inside a fixed algebraic closure; their union is the smallest perfect field containing k.
Formalized. Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean::perfectClosure, mem_perfectClosure_iff_pow_mem, perfectClosure.perfectField; Mathlib/FieldTheory/Perfect.lean::bijective_iterateFrobenius — Inside a perfect ambient field (in particular an algebraic closure), perfectClosure k E consists exactly of elements whose p^n-th power lies in k and is itself perfect. Frobenius bijectivity in every perfect intermediate field proves this relative perfect closure is contained in every perfect field containing k, giving the source minimality statement; this assembly was compile-checked against P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 26.4 (MacLane)
For K/k in characteristic p: if K/k is separable then K and k{p{-n}} are linearly disjoint over k for every n; conversely, linear disjointness from k^{1/p} already implies separability.
Not formalized. Pinned Mathlib proves separable subfields are linearly disjoint from purely inseparable extensions, but no checked theorem gives Matsumura’s converse from k^{1/p}, nor the whole every-n criterion under the source geometric separability notion.
Definition: differential basis
A subset B⊆K is a differential basis of K/k when {db:b∈B} is a K-basis of Ω_{K/k}; equivalently arbitrary prescribed values on B extend uniquely to a k-derivation K→K.
Not formalized. Pinned Mathlib has the universal derivation D, ordinary Basis, and linearMapEquivDerivation, so the source definition can be reconstructed. But no DifferentialBasis/equivalent source-level interface is exported; consistent with strict definition mapping elsewhere in FC13, derivability alone does not earn a native route.
Definition: p-independence and p-basis
In characteristic p, B⊆K is p-independent over k when its p-monomials are linearly independent over K^p(k); it is a p-basis of K/k when additionally K=K^p(k,B). Any p-independent set extends to a p-basis.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 26.5
Differential bases are exactly transcendence bases in characteristic zero and exactly p-bases in characteristic p.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 26.6
For a field extension K/k, separability is equivalent to injectivity of Ω_{k/k′}⊗kK→Ω{K/k′} for every subfield k′⊆k; equivalently differential bases of k/k′ extend to K/k′, equivalently Ω_k⊗_kK→Ω_K is injective, equivalently every derivation of k to a K-module extends to K.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Definition: absolute p-basis
In characteristic p, a p-basis over the prime subfield is called an absolute p-basis. It is unchanged if the prime subfield is replaced by any perfect subfield contained in k.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 26.7
For K/k in characteristic p, K is 0-etale over k iff an absolute p-basis of k is also an absolute p-basis of K.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 26.8
If K/k is separable of characteristic p and B is a p-basis of K/k, then B is algebraically independent over k and K is 0-etale over k(B).
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Counterexample: a p-basis need not make the extension algebraic
Even when K/k is separable and B is a p-basis, K need not be algebraic over k(B); the source gives K=k(x,x{p{-1}},x{p{-2}},…) with B empty.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 26.9
A field extension K/k is separable iff K is 0-smooth over k.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Definition: imperfection module
For k→A→B, the imperfection module Γ_{B/A/k} is the kernel of Ω_{A/k}⊗A B→Ω{B/k}; for the prime field k is omitted from the notation.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Lemma: imperfection-module exact sequence
For field maps k→K→L→L′ there is a natural exact sequence relating Γ_{L/K/k}, Γ_{L′/K/k}, Ω_{L/K}, Ω_{L′/K}, and Ω_{L′/L}.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 26.10 (Cartier equality)
If k is perfect, K/k arbitrary and L/K finitely generated, then dim_L Ω_{L/K}=trdeg_K L+dim_L Γ_{L/K/k}.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Definition: differential ideals and differentiably simple rings
An ideal is differential if every derivation preserves it. A ring is differentiably simple if it has no nontrivial differential ideals.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Harper theorem
A Noetherian ring of characteristic p is differentiably simple iff it is isomorphic to k[T_1,…,T_n]/(T_1p,…,T_np) for a field k of characteristic p.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Kimura-Niitsuma / Kunz-conjecture theorem
Let R be regular local of characteristic p and S⊆R a local subring containing R^p, with R finite over S. Then R has a p-basis over S iff S is regular.
Not formalized. Pinned/current/open Mathlib has Frobenius, perfect closure, linear disjointness, Kähler differentials, and ordinary derivations, but no reusable p-basis/p-independence interface or the source theorem package required for this unit. Targeted open-PR and indexed Lean-code searches were negative.
Definition: higher derivation of finite or infinite length
For k→A→B, a higher derivation of length m is a sequence (D_0,…,D_m) of k-linear maps with D_0 the structure map and D_i(xy)=Σ_{r+s=i}D_r(x)D_s(y). Equivalently ΣD_i(x)t^i defines a k-algebra homomorphism A→B[t]/(t^{m+1}); HS_k(A,m) denotes the set in the endomorphism case. It is trivial on a∈A when D_i(a)=0 for all i>0.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Construction: group law on higher derivations
Identifying a higher derivation with an automorphism of A[t]/(t^{m+1}) congruent to the identity mod t gives HS_k(A,m) a generally nonabelian group structure; components compose by convolution D_iD′=Σ_{r+s=i}D_rD′_s.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: localisation of higher derivations
A higher derivation A→B extends uniquely to compatible localisations A_S→B_T whenever the structure map sends S into T.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 27.1
If A is 0-smooth over k, every finite-length higher k-derivation from A to an A-algebra B extends to a higher derivation of infinite length.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Definition: iterative higher derivation
A higher derivation D is iterative when D_iD_j=binom(i+j,i)D_{i+j}; equivalently its associated homomorphisms satisfy the additive formal-group composition law.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Comparison: iterative higher derivations in characteristic zero and p
Over a Q-algebra, an iterative higher derivation is determined by D_1 with D_n=D_1^n/n!, and conversely every derivation integrates this way. In characteristic p one still has D_i=D_1^i/i! for i<p and necessarily D_1^p=0.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 27.2
If k→A→B and B is 0-etale over A, every higher derivation of A with values in B extends uniquely to a higher derivation of B; an iterative higher derivation extends iteratively.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 27.3
In characteristic p, if D∈Der(A), Dx=1 and D^p=0, then A is free over A_0=ker D with basis 1,x,…,x^{p−1}. If K/k is separable and 0≠D∈Der_k(K) with D^p=0, one can choose x with Dx=1 and a p-basis B={x}∪B_0 for K/k with B_0⊆ker D.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.
Theorem: Theorem 27.4
For a separable field extension K/k of characteristic p, D∈Der_k(K) extends to an iterative higher k-derivation iff D^p=0.
Not formalized. Pinned/current/open Mathlib has polynomial Hasse derivatives but no Hasse–Schmidt higher derivation object, convolution group law, iterative condition, localization/étale extension, or Matsumura’s characteristic-p integration theorems. Targeted open-PR and indexed Lean-code searches were negative.