KaehlerDifferential.submodule_span_range_eq_ideal
theorem KaehlerDifferential.submodule_span_range_eq_ideal :
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) =
Submodule.restrictScalars S (KaehlerDifferential.ideal R S)
This theorem states that for any types `R` and `S`, with `R` being a commutative ring, `S` being a ring, and `S` being an `R`-algebra, the submodule of `S` spanned by the range of the function that maps each element `s` to `1 ⊗ s - s ⊗ 1` is equal to the restriction of scalars of the Kähler differential ideal of `R` and `S` to `S`. In other words, the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S` is generated by the elements of the form `1 ⊗ s - s ⊗ 1` in the `S`-module.
More concisely: The submodule of an `R`-algebra `S` spanned by elements `1 ⊗ s - s ⊗ 1` is equal to the restriction of scalars of the Kähler differential ideal of `R` and `S` to `S`, and is the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.
|
Derivation.liftKaehlerDifferential_comp
theorem Derivation.liftKaehlerDifferential_comp :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
(D : Derivation R S M), D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D
The theorem `Derivation.liftKaehlerDifferential_comp` states that for any given types `R`, `S`, and `M` where `R` and `S` are commutative rings, `S` is an `R`-algebra, and `M` is both an `R`-module and `S`-module forming a scalar tower, if `D` is a derivation from `R` to `S` with values in `M`, then composing `D` with the function `Derivation.liftKaehlerDifferential` and the Kähler differential `KaehlerDifferential.D` from `S` to the Kähler differentials `Ω[S/R]` gives back `D`. In other words, the Kähler differential is universal with respect to `D`, demonstrating its fundamental role in differential geometry and algebra.
More concisely: Given derivations D from a commutative ring R to an R-algebra S over an R-module M, the composition of D with Derivation.liftKaehlerDifferential and KaehlerDifferential.D equals D.
|