# mathlib3documentation

ring_theory.kaehler

# The module of kaehler differentials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main results #

• kaehler_differential: The module of kaehler differentials. For an R-algebra S, we provide the notation Ω[S⁄R] for kaehler_differential R S. Note that the slash is \textfractionsolidus.
• kaehler_differential.D: The derivation into the module of kaehler differentials.
• kaehler_differential.span_range_derivation: The image of D spans Ω[S⁄R] as an S-module.
• kaehler_differential.linear_map_equiv_derivation: The isomorphism Hom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M).
• kaehler_differential.quot_ker_total_equiv: An alternative description of Ω[S⁄R] as S copies of S with kernel (kaehler_differential.ker_total) generated by the relations:
1. dx + dy = d(x + y)
2. x dy + y dx = d(x * y)
3. dr = 0 for r ∈ R
• kaehler_differential.map: Given a map between the arrows R → A and S → B, we have an A-linear map Ω[A⁄R] → Ω[B⁄S].

## Future project #

• Define a is_kaehler_differential predicate.
@[reducible]
def kaehler_differential.ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
ideal S S)

The kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

theorem kaehler_differential.one_smul_sub_smul_one_mem_ideal (R : Type u_1) {S : Type u_2} [comm_ring R] [comm_ring S] [ S] (a : S) :
1 ⊗ₜ[R] a - a ⊗ₜ[R] 1
def derivation.tensor_product_to {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) :
S →ₗ[S] M

For a R-derivation S → M, this is the map S ⊗[R] S →ₗ[S] M sending s ⊗ₜ t ↦ s • D t.

Equations
theorem derivation.tensor_product_to_tmul {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) (s t : S) :
theorem derivation.tensor_product_to_mul {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) (x y : S) :
theorem kaehler_differential.submodule_span_range_eq_ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
(set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) =

The kernel of S ⊗[R] S →ₐ[R] S is generated by 1 ⊗ s - s ⊗ 1 as a S-module.

theorem kaehler_differential.span_range_eq_ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
ideal.span (set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) =
def kaehler_differential (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
Type u_2

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 kaehler_differential.tensor_product_to_surjective and derivation.tensor_product_to_tmul.

We also provide the notation Ω[S⁄R] for kaehler_differential R S. Note that the slash is \textfractionsolidus.

Equations
Instances for kaehler_differential
@[protected, instance]
def kaehler_differential.module (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[protected, instance]
def kaehler_differential.add_comm_group (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[protected, instance]
def kaehler_differential.nonempty (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[protected, instance]
def kaehler_differential.module' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {R' : Type u_3} [comm_ring R'] [algebra R' S] [ R' S] :
Equations
@[protected, instance]
def kaehler_differential.is_scalar_tower (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S S) Ω[SR]
@[protected, instance]
def kaehler_differential.is_scalar_tower_of_tower (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {R₁ : Type u_3} {R₂ : Type u_4} [comm_ring R₁] [comm_ring R₂] [algebra R₁ S] [algebra R₂ S] [has_smul R₁ R₂] [ R₁ S] [ R₂ S] [ R₂ S] :
R₂ Ω[SR]
@[protected, instance]
def kaehler_differential.is_scalar_tower' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S S) Ω[SR]
def kaehler_differential.from_ideal (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :

The quotient map I → Ω[S⁄R] with I being the kernel of S ⊗[R] S → S.

Equations
def kaehler_differential.D_linear_map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :

(Implementation) The underlying linear map of the derivation into Ω[S⁄R].

Equations
theorem kaehler_differential.D_linear_map_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (s : S) :
= 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
def kaehler_differential.D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S Ω[SR]

The universal derivation into Ω[S⁄R].

Equations
theorem kaehler_differential.D_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (s : S) :
s = 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
theorem kaehler_differential.span_range_derivation (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
def derivation.lift_kaehler_differential {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) :

The linear map from Ω[S⁄R], associated with a derivation.

Equations
theorem derivation.lift_kaehler_differential_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) (x : ) :
theorem derivation.lift_kaehler_differential_comp {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D : S M) :
@[simp]
theorem derivation.lift_kaehler_differential_comp_D {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (D' : S M) (x : S) :
@[ext]
theorem derivation.lift_kaehler_differential_unique {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] (f f' : Ω[SR] →ₗ[S] M) (hf : (f.comp_der) = (f'.comp_der) ) :
f = f'
theorem derivation.lift_kaehler_differential_D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
theorem kaehler_differential.D_tensor_product_to {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] (x : ) :
= x
def kaehler_differential.linear_map_equiv_derivation (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] {M : Type u_3} [ M] [ M] [ M] :

The S-linear maps from Ω[S⁄R] to M are (S-linearly) equivalent to R-derivations from S to M.

Equations

The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S.

Equations

The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S as an S-algebra.

Equations
theorem kaehler_differential.End_equiv_aux (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (f : S →ₐ[R] S ) :
= S S
noncomputable def kaehler_differential.End_equiv_derivation' (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S Ω[SR] ≃ₗ[R] S

Derivations into Ω[S⁄R] is equivalent to derivations into (kaehler_differential.ideal R S).cotangent_ideal

Equations
def kaehler_differential.End_equiv_aux_equiv (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
{f // = S S {f //

(Implementation) An equiv version of kaehler_differential.End_equiv_aux. Used in kaehler_differential.End_equiv.

Equations
noncomputable def kaehler_differential.End_equiv (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
Ω[SR] {f //

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
noncomputable def kaehler_differential.ker_total (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
(S →₀ S)

The S-submodule of S →₀ S (the direct sum of copies of S indexed by S) generated by the relations:

1. dx + dy = d(x + y)
2. x dy + y dx = d(x * y)
3. dr = 0 for r ∈ R where db is the unit in the copy of S with index b.

This is the kernel of the surjection finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S). See kaehler_differential.ker_total_eq and kaehler_differential.total_surjective.

Equations
theorem kaehler_differential.ker_total_mkq_single_add (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x y z : S) :
.mkq) (finsupp.single (x + y) z) = .mkq) z) + .mkq) z)
theorem kaehler_differential.ker_total_mkq_single_mul (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x y z : S) :
.mkq) (finsupp.single (x * y) z) = .mkq) (z * x)) + .mkq) (z * y))
theorem kaehler_differential.ker_total_mkq_single_algebra_map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x : R) (y : S) :
.mkq) (finsupp.single ( S) x) y) = 0
theorem kaehler_differential.ker_total_mkq_single_algebra_map_one (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x : S) :
.mkq) x) = 0
theorem kaehler_differential.ker_total_mkq_single_smul (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (r : R) (x y : S) :
.mkq) (finsupp.single (r x) y) = r .mkq) y)
noncomputable def kaehler_differential.derivation_quot_ker_total (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
S ((S →₀ S)

The (universal) derivation into (S →₀ S) ⧸ kaehler_differential.ker_total R S.

Equations
theorem kaehler_differential.derivation_quot_ker_total_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (x : S) :
= .mkq) 1)
theorem kaehler_differential.ker_total_eq (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :
@[simp]
theorem kaehler_differential.quot_ker_total_equiv_symm_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (ᾰ : Ω[SR]) :
@[simp]
theorem kaehler_differential.quot_ker_total_equiv_apply (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (ᾰ : (S →₀ S) ) :
= Ω[SR] S S)) _).to_fun
noncomputable def kaehler_differential.quot_ker_total_equiv (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] :

Ω[S⁄R] is isomorphic to S copies of S with kernel kaehler_differential.ker_total.

Equations
theorem kaehler_differential.ker_total_map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] (h : function.surjective B)) :
submodule.map B))) (set.range (λ (x : S), finsupp.single ( B) x) 1)) =
def derivation.comp_algebra_map {R : Type u_1} [comm_ring R] {M : Type u_3} [ M] (A : Type u_4) {B : Type u_5} [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ M] [ M] [ M] (d : B M) :
A M

For a tower R → A → B and an R-derivation B → M, we may compose with A → B to obtain an R-derivation A → M.

Equations
def kaehler_differential.map (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] [ B] :

The map Ω[A⁄R] →ₗ[A] Ω[B⁄R] given a square A --→ B ↑ ↑ | | R --→ S

Equations
theorem kaehler_differential.map_comp_der (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] [ B] :
A B).comp_der) =
theorem kaehler_differential.map_D (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] [ B] (x : A) :
A B) ( x) = ( B) x)
theorem kaehler_differential.map_surjective_of_surjective (R : Type u_1) (S : Type u_2) [comm_ring R] [comm_ring S] [ S] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] [ B] [ B] [ B] (h : function.surjective B)) :
noncomputable def kaehler_differential.map_base_change (R : Type u_1) [comm_ring R] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] :

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
@[simp]
theorem kaehler_differential.map_base_change_tmul (R : Type u_1) [comm_ring R] (A : Type u_4) (B : Type u_5) [comm_ring A] [comm_ring B] [ A] [ B] [ B] [ B] (x : B) (y : Ω[AR]) :
(x ⊗ₜ[A] y) = x A B) y