diff --git a/src/ring_theory/derivation.lean b/src/ring_theory/derivation.lean index 2d0bb2a9ec069..3f249a07dd6f6 100644 --- a/src/ring_theory/derivation.lean +++ b/src/ring_theory/derivation.lean @@ -7,6 +7,7 @@ Authors: Nicolò Cavalleri, Andrew Yang import ring_theory.adjoin.basic import algebra.lie.of_associative import ring_theory.tensor_product +import ring_theory.ideal.cotangent /-! # Derivations @@ -14,15 +15,25 @@ import ring_theory.tensor_product This file defines derivation. A derivation `D` from the `R`-algebra `A` to the `A`-module `M` is an `R`-linear map that satisfy the Leibniz rule `D (a * b) = a * D b + D a * b`. -## Notation - -The notation `⁅D1, D2⁆` is used for the commutator of two derivations. - -TODO: this file is just a stub to go on with some PRs in the geometry section. It only -implements the definition of derivations in commutative algebra. This will soon change: as soon -as bimodules will be there in mathlib I will change this file to take into account the -non-commutative case. Any development on the theory of derivations is discouraged until the -definitive definition of derivation will be implemented. +## Main results + +- `derivation`: The type of `R`-derivations from `A` to `M`. This has an `A`-module structure. +- `derivation.llcomp`: We may compose linear maps and derivations to obtain a derivation, + and the composition is bilinear. +- `derivation.lie_algebra`: The `R`-derivations from `A` to `A` form an lie algebra over `R`. +- `derivation_to_square_zero_equiv_lift`: The `R`-derivations from `A` into a square-zero ideal `I` + of `B` corresponds to the lifts `A →ₐ[R] B` of the map `A →ₐ[R] B ⧸ I`. +- `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)`. + +## Future project + +Generalize this into bimodules. -/ open algebra @@ -448,20 +459,20 @@ end end to_square_zero -section derivation_module +section kaehler_differential open_locale tensor_product variables (R S : Type*) [comm_ring R] [comm_ring S] [algebra R S] /-- The kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`. -/ -abbreviation derivation_module.ideal : ideal (S ⊗[R] S) := +abbreviation kaehler_differential.ideal : ideal (S ⊗[R] S) := ring_hom.ker (tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S) variable {S} -lemma derivation_module.one_smul_sub_smul_one_mem_ideal (a : S) : - (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ derivation_module.ideal R S := +lemma kaehler_differential.one_smul_sub_smul_one_mem_ideal (a : S) : + (1 : S) ⊗ₜ[R] a - a ⊗ₜ[R] (1 : S) ∈ kaehler_differential.ideal R S := by simp [ring_hom.mem_ker] variables {R} @@ -499,14 +510,14 @@ end variables (R S) /-- The kernel of `S ⊗[R] S →ₐ[R] S` is generated by `1 ⊗ s - s ⊗ 1` as a `S`-module. -/ -lemma derivation_module.submodule_span_range_eq_ideal : +lemma kaehler_differential.submodule_span_range_eq_ideal : submodule.span S (set.range $ λ s : S, (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) = - (derivation_module.ideal R S).restrict_scalars S := + (kaehler_differential.ideal R S).restrict_scalars S := begin apply le_antisymm, { rw submodule.span_le, rintros _ ⟨s, rfl⟩, - exact derivation_module.one_smul_sub_smul_one_mem_ideal _ _ }, + exact kaehler_differential.one_smul_sub_smul_one_mem_ideal _ _ }, { rintros x (hx : _ = _), have : x - (tensor_product.lmul' R x) ⊗ₜ[R] (1 : S) = x, { rw [hx, tensor_product.zero_tmul, sub_zero] }, @@ -526,18 +537,188 @@ begin exact add_mem hx hy } } end -lemma derivation_module.span_range_eq_ideal : +lemma kaehler_differential.span_range_eq_ideal : ideal.span (set.range $ λ s : S, (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) = - derivation_module.ideal R S := + kaehler_differential.ideal R S := begin apply le_antisymm, { rw ideal.span_le, rintros _ ⟨s, rfl⟩, - exact derivation_module.one_smul_sub_smul_one_mem_ideal _ _ }, - { change (derivation_module.ideal R S).restrict_scalars S ≤ (ideal.span _).restrict_scalars S, - rw [← derivation_module.submodule_span_range_eq_ideal, ideal.span], + exact kaehler_differential.one_smul_sub_smul_one_mem_ideal _ _ }, + { change (kaehler_differential.ideal R S).restrict_scalars S ≤ (ideal.span _).restrict_scalars S, + rw [← kaehler_differential.submodule_span_range_eq_ideal, ideal.span], conv_rhs { rw ← submodule.span_span_of_tower S }, exact submodule.subset_span } end -end derivation_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 +`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`. +-/ +@[derive [add_comm_group, module R, module S, module (S ⊗[R] S)]] +def kaehler_differential : Type* := (kaehler_differential.ideal R S).cotangent + +notation `Ω[ `:100 S ` ⁄ `:0 R ` ]`:0 := kaehler_differential R S + +instance : nonempty Ω[S⁄R] := ⟨0⟩ + +instance : is_scalar_tower S (S ⊗[R] S) Ω[S⁄R] := +ideal.cotangent.is_scalar_tower _ + +instance kaehler_differential.is_scalar_tower' : is_scalar_tower R S Ω[S⁄R] := +begin + haveI : is_scalar_tower R S (kaehler_differential.ideal R S), + { constructor, intros x y z, ext1, exact smul_assoc x y z.1 }, + exact submodule.quotient.is_scalar_tower _ _ +end + +/-- (Implementation) The underlying linear map of the derivation into `Ω[S⁄R]`. -/ +def kaehler_differential.D_linear_map : S →ₗ[R] Ω[S⁄R] := +((kaehler_differential.ideal R S).to_cotangent.restrict_scalars R).comp + ((tensor_product.include_right.to_linear_map - tensor_product.include_left.to_linear_map : + S →ₗ[R] S ⊗[R] S).cod_restrict ((kaehler_differential.ideal R S).restrict_scalars R) + (kaehler_differential.one_smul_sub_smul_one_mem_ideal R) : _ →ₗ[R] _) + +lemma kaehler_differential.D_linear_map_apply (s : S) : + kaehler_differential.D_linear_map R S s = (kaehler_differential.ideal R S).to_cotangent + ⟨1 ⊗ₜ s - s ⊗ₜ 1, kaehler_differential.one_smul_sub_smul_one_mem_ideal R s⟩ := +rfl + +/-- The universal derivation into `Ω[S⁄R]`. -/ +def kaehler_differential.D : derivation R S Ω[S⁄R] := +{ map_one_eq_zero' := begin + dsimp [kaehler_differential.D_linear_map_apply], + rw [ideal.to_cotangent_eq_zero, subtype.coe_mk, sub_self], + exact zero_mem _ + end, + leibniz' := λ a b, begin + dsimp [kaehler_differential.D_linear_map_apply], + rw [← linear_map.map_smul_of_tower, ← linear_map.map_smul_of_tower, ← map_add, + ideal.to_cotangent_eq, pow_two], + convert submodule.mul_mem_mul (kaehler_differential.one_smul_sub_smul_one_mem_ideal R a : _) + (kaehler_differential.one_smul_sub_smul_one_mem_ideal R b : _) using 1, + simp only [add_subgroup_class.coe_sub, submodule.coe_add, submodule.coe_mk, + tensor_product.tmul_mul_tmul, mul_sub, sub_mul, mul_comm b, + submodule.coe_smul_of_tower, smul_sub, tensor_product.smul_tmul', smul_eq_mul, mul_one], + ring_nf, + end, + ..(kaehler_differential.D_linear_map R S) } + +lemma kaehler_differential.D_apply (s : S) : + kaehler_differential.D R S s = (kaehler_differential.ideal R S).to_cotangent + ⟨1 ⊗ₜ s - s ⊗ₜ 1, kaehler_differential.one_smul_sub_smul_one_mem_ideal R s⟩ := +rfl + +lemma kaehler_differential.span_range_derivation : + submodule.span S (set.range $ kaehler_differential.D R S) = ⊤ := +begin + rw _root_.eq_top_iff, + rintros x -, + obtain ⟨⟨x, hx⟩, rfl⟩ := ideal.to_cotangent_surjective _ x, + have : x ∈ (kaehler_differential.ideal R S).restrict_scalars S := hx, + rw ← kaehler_differential.submodule_span_range_eq_ideal at this, + suffices : ∃ hx, (kaehler_differential.ideal R S).to_cotangent ⟨x, hx⟩ ∈ + submodule.span S (set.range $ kaehler_differential.D R S), + { exact this.some_spec }, + apply submodule.span_induction this, + { rintros _ ⟨x, rfl⟩, + refine ⟨kaehler_differential.one_smul_sub_smul_one_mem_ideal R x, _⟩, + apply submodule.subset_span, + exact ⟨x, kaehler_differential.D_linear_map_apply R S x⟩ }, + { exact ⟨zero_mem _, zero_mem _⟩ }, + { rintros x y ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩, exact ⟨add_mem hx₁ hy₁, add_mem hx₂ hy₂⟩ }, + { rintros r x ⟨hx₁, hx₂⟩, exact ⟨((kaehler_differential.ideal R S).restrict_scalars S).smul_mem + r hx₁, submodule.smul_mem _ r hx₂⟩ } +end + +variables {R S} + +/-- The linear map from `Ω[S⁄R]`, associated with a derivation. -/ +def derivation.lift_kaehler_differential (D : derivation R S M) : Ω[S⁄R] →ₗ[S] M := +begin + refine ((kaehler_differential.ideal R S • ⊤ : + submodule (S ⊗[R] S) (kaehler_differential.ideal R S)).restrict_scalars S).liftq _ _, + { exact D.tensor_product_to.comp ((kaehler_differential.ideal R S).subtype.restrict_scalars S) }, + { intros x hx, + change _ = _, + apply submodule.smul_induction_on hx; clear hx x, + { rintros x (hx : _ = _) ⟨y, hy : _ = _⟩ -, + dsimp, + rw [derivation.tensor_product_to_mul, hx, hy, zero_smul, zero_smul, zero_add] }, + { intros x y ex ey, rw [map_add, ex, ey, zero_add] } } +end + +lemma derivation.lift_kaehler_differential_apply (D : derivation R S M) (x) : + D.lift_kaehler_differential + ((kaehler_differential.ideal R S).to_cotangent x) = D.tensor_product_to x := +rfl + +lemma derivation.lift_kaehler_differential_comp (D : derivation R S M) : + D.lift_kaehler_differential.comp_der (kaehler_differential.D R S) = D := +begin + ext a, + dsimp [kaehler_differential.D_apply], + refine (D.lift_kaehler_differential_apply _).trans _, + rw [subtype.coe_mk, map_sub, derivation.tensor_product_to_tmul, + derivation.tensor_product_to_tmul, one_smul, D.map_one_eq_zero, smul_zero, sub_zero], +end + +@[ext] +lemma derivation.lift_kaehler_differential_unique + (f f' : Ω[S⁄R] →ₗ[S] M) + (hf : f.comp_der (kaehler_differential.D R S) = + f'.comp_der (kaehler_differential.D R S)) : + f = f' := +begin + apply linear_map.ext, + intro x, + have : x ∈ submodule.span S (set.range $ kaehler_differential.D R S), + { rw kaehler_differential.span_range_derivation, trivial }, + apply submodule.span_induction this, + { rintros _ ⟨x, rfl⟩, exact congr_arg (λ D : derivation R S M, D x) hf }, + { rw [map_zero, map_zero] }, + { intros x y hx hy, rw [map_add, map_add, hx, hy] }, + { intros a x e, rw [map_smul, map_smul, e] } +end + +variables (R S) + +lemma derivation.lift_kaehler_differential_D : + (kaehler_differential.D R S).lift_kaehler_differential = linear_map.id := +derivation.lift_kaehler_differential_unique _ _ + (kaehler_differential.D R S).lift_kaehler_differential_comp + +variables {R S} + +lemma kaehler_differential.D_tensor_product_to (x : kaehler_differential.ideal R S) : + (kaehler_differential.D R S).tensor_product_to x = + (kaehler_differential.ideal R S).to_cotangent x := +begin + rw [← derivation.lift_kaehler_differential_apply, derivation.lift_kaehler_differential_D], + refl, +end + +variables (R S) + +lemma kaehler_differential.tensor_product_to_surjective : + function.surjective (kaehler_differential.D R S).tensor_product_to := +begin + intro x, obtain ⟨x, rfl⟩ := (kaehler_differential.ideal R S).to_cotangent_surjective x, + exact ⟨x, kaehler_differential.D_tensor_product_to x⟩ +end + +/-- The `S`-linear maps from `Ω[S⁄R]` to `M` are (`S`-linearly) equivalent to `R`-derivations +from `S` to `M`. -/ +def kaehler_differential.linear_map_equiv_derivation : (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] derivation R S M := +{ inv_fun := derivation.lift_kaehler_differential, + left_inv := λ f, derivation.lift_kaehler_differential_unique _ _ + (derivation.lift_kaehler_differential_comp _), + right_inv := derivation.lift_kaehler_differential_comp, + ..(derivation.llcomp.flip $ kaehler_differential.D R S) } + +end kaehler_differential