feat(ring_theory/derivation): Endomorphisms of the Kähler differential module (#15854)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/algebra/module/submodule/basic.lean

@@ -167,6 +167,12 @@ instance [has_smul S R] [has_smul S M] [is_scalar_tower S R M] :
 instance [has_smul S R] [has_smul S M] [is_scalar_tower S R M] : is_scalar_tower S R p :=
 p.to_sub_mul_action.is_scalar_tower
 
+instance is_scalar_tower' {S' : Type*}
+  [has_smul S R] [has_smul S M] [has_smul S' R] [has_smul S' M] [has_smul S S']
+  [is_scalar_tower S' R M] [is_scalar_tower S S' M] [is_scalar_tower S R M] :
+  is_scalar_tower S S' p :=
+p.to_sub_mul_action.is_scalar_tower'
+
 instance
   [has_smul S R] [has_smul S M] [is_scalar_tower S R M]
   [has_smul Sᵐᵒᵖ R] [has_smul Sᵐᵒᵖ M] [is_scalar_tower Sᵐᵒᵖ R M]

src/group_theory/group_action/sub_mul_action.lean

@@ -117,6 +117,11 @@ instance has_smul' : has_smul S p :=
 instance : is_scalar_tower S R p :=
 { smul_assoc := λ s r x, subtype.ext $ smul_assoc s r ↑x }
 
+instance is_scalar_tower' {S' : Type*} [has_smul S' R] [has_smul S' S]
+  [has_smul S' M] [is_scalar_tower S' R M] [is_scalar_tower S' S M] :
+  is_scalar_tower S' S p :=
+{ smul_assoc := λ s r x, subtype.ext $ smul_assoc s r ↑x }
+
 @[simp, norm_cast] lemma coe_smul_of_tower (s : S) (x : p) : ((s • x : p) : M) = s • ↑x := rfl
 
 @[simp] lemma smul_mem_iff' {G} [group G] [has_smul G R] [mul_action G M]

src/ring_theory/derivation.lean

@@ -6,6 +6,7 @@ Authors: Nicolò Cavalleri, Andrew Yang
 
 import ring_theory.adjoin.basic
 import algebra.lie.of_associative
+import ring_theory.ideal.cotangent
 import ring_theory.tensor_product
 import ring_theory.ideal.cotangent
 
@@ -211,7 +212,7 @@ section push_forward
 
 variables {N : Type*} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M]
   [is_scalar_tower R A N]
-variables (f : M →ₗ[A] N)
+variables (f : M →ₗ[A] N) (e : M ≃ₗ[A] N)
 
 /-- We can push forward derivations using linear maps, i.e., the composition of a derivation with a
 linear map is a derivation. Furthermore, this operation is linear on the spaces of derivations. -/
@@ -233,11 +234,20 @@ rfl
 rfl
 
 /-- The composition of a derivation with a linear map as a bilinear map -/
+@[simps]
 def llcomp : (M →ₗ[A] N) →ₗ[A] derivation R A M →ₗ[R] derivation R A N :=
 { to_fun := λ f, f.comp_der,
   map_add' := λ f₁ f₂, by { ext, refl },
   map_smul' := λ r D, by { ext, refl } }
 
+/-- Pushing a derivation foward through a linear equivalence is an equivalence. -/
+def _root_.linear_equiv.comp_der : derivation R A M ≃ₗ[R] derivation R A N :=
+{ inv_fun := e.symm.to_linear_map.comp_der,
+  left_inv := λ D, by { ext a, exact e.symm_apply_apply (D a) },
+  right_inv := λ D, by { ext a, exact e.apply_symm_apply (D a) },
+  ..e.to_linear_map.comp_der }
+
+
 end push_forward
 
 end
@@ -356,7 +366,7 @@ section to_square_zero
 
 universes u v w
 
-variables {R : Type u} {A : Type u} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B]
+variables {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B]
 variables [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ⊥)
 
 /-- If `f₁ f₂ : A →ₐ[R] B` are two lifts of the same `A →ₐ[R] B ⧸ I`,
@@ -721,4 +731,81 @@ def kaehler_differential.linear_map_equiv_derivation : (Ω[S⁄R] →ₗ[S] M) 
   right_inv := derivation.lift_kaehler_differential_comp,
   ..(derivation.llcomp.flip $ kaehler_differential.D R S) }
 
+/-- The quotient ring of `S ⊗ S ⧸ J ^ 2` by `Ω[S⁄R]` is isomorphic to `S`. -/
+def kaehler_differential.quotient_cotangent_ideal_ring_equiv :
+  (S ⊗ S ⧸ kaehler_differential.ideal R S ^ 2) ⧸
+    (kaehler_differential.ideal R S).cotangent_ideal ≃+* S :=
+begin
+  have : function.right_inverse tensor_product.include_left
+    (↑(tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S) : S ⊗[R] S →+* S),
+  { intro x, rw [alg_hom.coe_to_ring_hom, ← alg_hom.comp_apply,
+      tensor_product.lmul'_comp_include_left], refl },
+  refine (ideal.quot_cotangent _).trans _,
+  refine (ideal.quot_equiv_of_eq _).trans (ring_hom.quotient_ker_equiv_of_right_inverse this),
+  ext, refl,
+end
+
+/-- The quotient ring of `S ⊗ S ⧸ J ^ 2` by `Ω[S⁄R]` is isomorphic to `S` as an `S`-algebra. -/
+def kaehler_differential.quotient_cotangent_ideal :
+  ((S ⊗ S ⧸ kaehler_differential.ideal R S ^ 2) ⧸
+    (kaehler_differential.ideal R S).cotangent_ideal) ≃ₐ[S] S :=
+{ commutes' := (kaehler_differential.quotient_cotangent_ideal_ring_equiv R S).apply_symm_apply,
+  ..kaehler_differential.quotient_cotangent_ideal_ring_equiv R S }
+
+lemma kaehler_differential.End_equiv_aux (f : S →ₐ[R] S ⊗ S ⧸ kaehler_differential.ideal R S ^ 2) :
+  (ideal.quotient.mkₐ R (kaehler_differential.ideal R S).cotangent_ideal).comp f =
+    is_scalar_tower.to_alg_hom R S _ ↔
+  (tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S).ker_square_lift.comp f = alg_hom.id R S :=
+begin
+  rw [alg_hom.ext_iff, alg_hom.ext_iff],
+  apply forall_congr,
+  intro x,
+  have e₁ : (tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S).ker_square_lift (f x) =
+    kaehler_differential.quotient_cotangent_ideal_ring_equiv R S
+      (ideal.quotient.mk (kaehler_differential.ideal R S).cotangent_ideal $ f x),
+  { generalize : f x = y, obtain ⟨y, rfl⟩ := ideal.quotient.mk_surjective y, refl },
+  have e₂ : x = kaehler_differential.quotient_cotangent_ideal_ring_equiv
+    R S (is_scalar_tower.to_alg_hom R S _ x),
+  { exact ((tensor_product.lmul'_apply_tmul x 1).trans (mul_one x)).symm },
+  split,
+  { intro e,
+    exact (e₁.trans (@ring_equiv.congr_arg _ _ _ _ _ _
+      (kaehler_differential.quotient_cotangent_ideal_ring_equiv R S) _ _ e)).trans e₂.symm },
+  { intro e, apply (kaehler_differential.quotient_cotangent_ideal_ring_equiv R S).injective,
+    exact e₁.symm.trans (e.trans e₂) }
+end
+
+/-- Derivations into `Ω[S⁄R]` is equivalent to derivations
+into `(kaehler_differential.ideal R S).cotangent_ideal` -/
+-- This has type
+-- `derivation R S Ω[ S / R ] ≃ₗ[R] derivation R S (kaehler_differential.ideal R S).cotangent_ideal`
+-- But lean times-out if this is given explicitly.
+noncomputable
+def kaehler_differential.End_equiv_derivation' :=
+@linear_equiv.comp_der R _ _ _ _ Ω[S⁄R] _ _ _ _ _ _ _ _ _
+  ((kaehler_differential.ideal R S).cotangent_equiv_ideal.restrict_scalars S)
+
+/-- (Implementation) An `equiv` version of `kaehler_differential.End_equiv_aux`.
+Used in `kaehler_differential.End_equiv`. -/
+def kaehler_differential.End_equiv_aux_equiv :
+  {f // (ideal.quotient.mkₐ R (kaehler_differential.ideal R S).cotangent_ideal).comp f =
+    is_scalar_tower.to_alg_hom R S _ } ≃
+  { f // (tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S).ker_square_lift.comp f = alg_hom.id R S } :=
+(equiv.refl _).subtype_equiv (kaehler_differential.End_equiv_aux R S)
+
+/--
+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`.
+-/
+noncomputable
+def kaehler_differential.End_equiv :
+  module.End S Ω[S⁄R] ≃
+    { f // (tensor_product.lmul' R : S ⊗[R] S →ₐ[R] S).ker_square_lift.comp f = alg_hom.id R S } :=
+(kaehler_differential.linear_map_equiv_derivation R S).to_equiv.trans $
+  (kaehler_differential.End_equiv_derivation' R S).to_equiv.trans $
+  (derivation_to_square_zero_equiv_lift
+  (kaehler_differential.ideal R S).cotangent_ideal
+  (kaehler_differential.ideal R S).cotangent_ideal_square).trans $
+  kaehler_differential.End_equiv_aux_equiv R S
+
 end kaehler_differential

src/ring_theory/ideal/cotangent.lean

@@ -179,6 +179,14 @@ begin
   { rintros _ ⟨x, hx, rfl⟩, exact hx }
 end
 
+/-- The quotient ring of `I ⧸ I ^ 2` is `R ⧸ I`. -/
+def quot_cotangent : ((R ⧸ I ^ 2) ⧸ I.cotangent_ideal) ≃+* R ⧸ I :=
+begin
+  refine (ideal.quot_equiv_of_eq (ideal.map_eq_submodule_map _ _).symm).trans _,
+  refine (double_quot.quot_quot_equiv_quot_sup _ _).trans _,
+  exact (ideal.quot_equiv_of_eq (sup_eq_right.mpr $ ideal.pow_le_self two_ne_zero)),
+end
+
 end ideal
 
 namespace local_ring

src/ring_theory/ideal/operations.lean

@@ -1206,6 +1206,12 @@ lemma mem_map_iff_of_surjective {I : ideal R} {y} :
 lemma le_map_of_comap_le_of_surjective : comap f K ≤ I → K ≤ map f I :=
 λ h, (map_comap_of_surjective f hf K) ▸ map_mono h
 
+omit hf
+
+lemma map_eq_submodule_map (f : R →+* S) [h : ring_hom_surjective f] (I : ideal R) :
+  I.map f = submodule.map f.to_semilinear_map I :=
+submodule.ext (λ x, mem_map_iff_of_surjective f h.1)
+
 end surjective
 
 section injective

src/ring_theory/ideal/quotient.lean

@@ -121,6 +121,8 @@ instance : unique (R ⧸ (⊤ : ideal R)) :=
 lemma mk_surjective : function.surjective (mk I) :=
 λ y, quotient.induction_on' y (λ x, exists.intro x rfl)
 
+instance : ring_hom_surjective (mk I) := ⟨mk_surjective⟩
+
 /-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
 `s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`. -/
 lemma quotient_ring_saturate (I : ideal R) (s : set R) :