The module of kaehler differentials #
Main results #
KaehlerDifferential
: The module of kaehler differentials. For anR
-algebraS
, we provide the notationΩ[S⁄R]
forKaehlerDifferential R S
. Note that the slash is\textfractionsolidus
.KaehlerDifferential.D
: The derivation into the module of kaehler differentials.KaehlerDifferential.span_range_derivation
: The image ofD
spansΩ[S⁄R]
as anS
-module.KaehlerDifferential.linearMapEquivDerivation
: The isomorphismHom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M)
.KaehlerDifferential.quotKerTotalEquiv
: An alternative description ofΩ[S⁄R]
asS
copies ofS
with kernel (KaehlerDifferential.kerTotal
) generated by the relations:dx + dy = d(x + y)
x dy + y dx = d(x * y)
dr = 0
forr ∈ R
KaehlerDifferential.map
: Given a map between the arrowsR →+* A
andS →+* B
, we have anA
-linear mapΩ[A⁄R] → Ω[B⁄S]
.KaehlerDifferential.map_surjective
: The sequenceΩ[B⁄R] → Ω[B⁄A] → 0
is exact.KaehlerDifferential.exact_mapBaseChange_map
: The sequenceB ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A]
is exact.KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange
: IfA → B
is surjective with kernelI
, then the sequenceI/I² → B ⊗[A] Ω[A⁄R] → Ω[B⁄R]
is exact.KaehlerDifferential.mapBaseChange_surjective
: IfA → B
is surjective, then the sequenceB ⊗[A] Ω[A⁄R] → Ω[B⁄R] → 0
is exact.
Future project #
- Define the
IsKaehlerDifferential
predicate.
The kernel of the multiplication map S ⊗[R] S →ₐ[R] S
.
Equations
Instances For
For a R
-derivation S → M
, this is the map S ⊗[R] S →ₗ[S] M
sending s ⊗ₜ t ↦ s • D t
.
Equations
- D.tensorProductTo = TensorProduct.AlgebraTensorModule.lift ((LinearMap.lsmul S (S →ₗ[R] M)).flip ↑D)
Instances For
The kernel of S ⊗[R] S →ₐ[R] S
is generated by 1 ⊗ s - s ⊗ 1
as a S
-module.
The module of Kähler differentials (Kahler differentials, Kaehler differentials).
This is implemented as I / I ^ 2
with I
the kernel of the multiplication map S ⊗[R] S →ₐ[R] S
.
To view elements as a linear combination of the form s • D s'
, use
KaehlerDifferential.tensorProductTo_surjective
and Derivation.tensorProductTo_tmul
.
We also provide the notation Ω[S⁄R]
for KaehlerDifferential R S
.
Note that the slash is \textfractionsolidus
.
Equations
- Ω[S⁄R] = (KaehlerDifferential.ideal R S).Cotangent
Instances For
Equations
- instAddCommGroupKaehlerDifferential R S = inferInstanceAs (AddCommGroup (KaehlerDifferential.ideal R S).Cotangent)
The module of Kähler differentials (Kahler differentials, Kaehler differentials).
This is implemented as I / I ^ 2
with I
the kernel of the multiplication map S ⊗[R] S →ₐ[R] S
.
To view elements as a linear combination of the form s • D s'
, use
KaehlerDifferential.tensorProductTo_surjective
and Derivation.tensorProductTo_tmul
.
We also provide the notation Ω[S⁄R]
for KaehlerDifferential R S
.
Note that the slash is \textfractionsolidus
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The quotient map I → Ω[S⁄R]
with I
being the kernel of S ⊗[R] S → S
.
Equations
- KaehlerDifferential.fromIdeal R S = (KaehlerDifferential.ideal R S).toCotangent
Instances For
The universal derivation into Ω[S⁄R]
.
Equations
- KaehlerDifferential.D R S = { toLinearMap := KaehlerDifferential.DLinearMap R S, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
Instances For
Ω[S⁄R]
is trivial if R → S
is surjective.
Also see Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential
.
The linear map from Ω[S⁄R]
, associated with a derivation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The S
-linear maps from Ω[S⁄R]
to M
are (S
-linearly) equivalent to R
-derivations
from S
to M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient ring of S ⊗ S ⧸ J ^ 2
by Ω[S⁄R]
is isomorphic to S
.
Equations
- KaehlerDifferential.quotientCotangentIdealRingEquiv R S = (KaehlerDifferential.ideal R S).quotCotangent.trans ((Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfRightInverse ⋯))
Instances For
The quotient ring of S ⊗ S ⧸ J ^ 2
by Ω[S⁄R]
is isomorphic to S
as an S
-algebra.
Equations
- KaehlerDifferential.quotientCotangentIdeal R S = { toEquiv := (KaehlerDifferential.quotientCotangentIdealRingEquiv R S).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- smul_SSmod_SSmod R S = Mul.toSMul (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- ⋯ = ⋯
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- ⋯ = ⋯
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- ⋯ = ⋯
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- instS R S = Submodule.module' (KaehlerDifferential.ideal R S).cotangentIdeal
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- instR R S = Submodule.module' (KaehlerDifferential.ideal R S).cotangentIdeal
Instances For
A shortcut instance to prevent timing out. Hopefully to be removed in the future.
Equations
- instSS R S = Submodule.module' (KaehlerDifferential.ideal R S).cotangentIdeal
Instances For
Derivations into Ω[S⁄R]
is equivalent to derivations
into (KaehlerDifferential.ideal R S).cotangentIdeal
.
Equations
- KaehlerDifferential.endEquivDerivation' R S = (LinearEquiv.restrictScalars S (KaehlerDifferential.ideal R S).cotangentEquivIdeal).compDer
Instances For
(Implementation) An Equiv
version of KaehlerDifferential.End_equiv_aux
.
Used in KaehlerDifferential.endEquiv
.
Equations
- KaehlerDifferential.endEquivAuxEquiv R S = (Equiv.refl (S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2)).subtypeEquiv ⋯
Instances For
The endomorphisms of Ω[S⁄R]
corresponds to sections of the surjection S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S
,
with J
being the kernel of the multiplication map S ⊗[R] S →ₐ[R] S
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The S
-submodule of S →₀ S
(the direct sum of copies of S
indexed by S
) generated by
the relations:
dx + dy = d(x + y)
x dy + y dx = d(x * y)
dr = 0
forr ∈ R
wheredb
is the unit in the copy ofS
with indexb
.
This is the kernel of the surjection
Finsupp.linearCombination S Ω[S⁄R] S (KaehlerDifferential.D R S)
.
See KaehlerDifferential.kerTotal_eq
and KaehlerDifferential.linearCombination_surjective
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The (universal) derivation into (S →₀ S) ⧸ KaehlerDifferential.kerTotal R S
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination
.
Ω[S⁄R]
is isomorphic to S
copies of S
with kernel KaehlerDifferential.kerTotal
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given the commutative diagram
A --→ B
↑ ↑
| |
R --→ S
The kernel of the presentation ⊕ₓ B dx ↠ Ω_{B/S}
is spanned by the image of the
kernel of ⊕ₓ A dx ↠ Ω_{A/R}
and all ds
with s : S
.
See kerTotal_map'
for the special case where R = S
.
This is a special case of kerTotal_map
where R = S
.
The kernel of the presentation ⊕ₓ B dx ↠ Ω_{B/R}
is spanned by the image of the
kernel of ⊕ₓ A dx ↠ Ω_{A/R}
and all da
with a : A
.
The map Ω[A⁄R] →ₗ[A] Ω[B⁄S]
given a square
A --→ B
↑ ↑
| |
R --→ S
Equations
- KaehlerDifferential.map R S A B = (Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B))).liftKaehlerDifferential
Instances For
The lift of the map Ω[A⁄R] →ₗ[A] Ω[B⁄R]
to the base change along A → B
.
This is the first map in the exact sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0
.
Equations
- KaehlerDifferential.mapBaseChange R A B = ⋯.lift (KaehlerDifferential.map R R A B)
Instances For
The sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0
is exact.
Also see KaehlerDifferential.map_surjective
.
The map I → B ⊗[A] B ⊗[A] Ω[A⁄R]
where I = ker(A → B)
.
Equations
- KaehlerDifferential.kerToTensor R A B = { toFun := fun (x : ↥(RingHom.ker (algebraMap A B))) => 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The map I/I² → B ⊗[A] B ⊗[A] Ω[A⁄R]
where I = ker(A → B)
.
Equations
- KaehlerDifferential.kerCotangentToTensor R A B = (RingHom.ker (algebraMap A B) • ⊤).liftQ (KaehlerDifferential.kerToTensor R A B) ⋯