chore(ring_theory/kaehler): cleanup instances (#19234)

eric-wieser · eric-wieser · commit 4b92a463033b · 2023-07-24T07:47:40.000Z
The previous module instance has the wrong defeqs, and was more work to construct.
The new one remains propositionally equal to the old one.
diff --git a/src/ring_theory/ideal/cotangent.lean b/src/ring_theory/ideal/cotangent.lean
@@ -38,16 +38,10 @@ instance cotangent.module_of_tower : module S I.cotangent :=
 submodule.quotient.module' _
 
 instance : is_scalar_tower S S' I.cotangent :=
-begin
-  delta cotangent,
-  constructor,
-  intros s s' x,
-  rw [← @is_scalar_tower.algebra_map_smul S' R, ← @is_scalar_tower.algebra_map_smul S' R,
-    ← smul_assoc, ← is_scalar_tower.to_alg_hom_apply S S' R, map_smul],
-  refl
-end
+submodule.quotient.is_scalar_tower _ _
 
-instance [is_noetherian R I] : is_noetherian R I.cotangent := by { delta cotangent, apply_instance }
+instance [is_noetherian R I] : is_noetherian R I.cotangent :=
+submodule.quotient.is_noetherian _
 
 /-- The quotient map from `I` to `I ⧸ I ^ 2`. -/
 @[simps apply (lemmas_only)]
diff --git a/src/ring_theory/kaehler.lean b/src/ring_theory/kaehler.lean
@@ -145,31 +145,23 @@ notation `Ω[`:100 S `⁄`:0 R `]`:0 := kaehler_differential R S
 
 instance : nonempty Ω[S⁄R] := ⟨0⟩
 
-instance kaehler_differential.module' {R' : Type*} [comm_ring R'] [algebra R' S] :
+instance kaehler_differential.module' {R' : Type*} [comm_ring R'] [algebra R' S]
+  [smul_comm_class R R' S] :
   module R' Ω[S⁄R] :=
-(module.comp_hom (kaehler_differential.ideal R S).cotangent (algebra_map R' S) : _)
+submodule.quotient.module' _
 
 instance : is_scalar_tower S (S ⊗[R] S) Ω[S⁄R] :=
 ideal.cotangent.is_scalar_tower _
 
 instance kaehler_differential.is_scalar_tower_of_tower {R₁ R₂ : Type*} [comm_ring R₁] [comm_ring R₂]
-  [algebra R₁ S] [algebra R₂ S] [algebra R₁ R₂] [is_scalar_tower R₁ R₂ S] :
+  [algebra R₁ S] [algebra R₂ S] [has_smul R₁ R₂]
+  [smul_comm_class R R₁ S] [smul_comm_class R R₂ S] [is_scalar_tower R₁ R₂ S] :
   is_scalar_tower R₁ R₂ Ω[S⁄R] :=
-begin
-  convert restrict_scalars.is_scalar_tower R₁ R₂ Ω[S⁄R] using 1,
-  ext x m,
-  show algebra_map R₁ S x • m = algebra_map R₂ S (algebra_map R₁ R₂ x) • m,
-  rw ← is_scalar_tower.algebra_map_apply,
-end
+submodule.quotient.is_scalar_tower _ _
 
 instance kaehler_differential.is_scalar_tower' :
   is_scalar_tower R (S ⊗[R] S) Ω[S⁄R] :=
-begin
-  convert restrict_scalars.is_scalar_tower R (S ⊗[R] S) Ω[S⁄R] using 1,
-  ext x m,
-  show algebra_map R S x • m = algebra_map R (S ⊗[R] S) x • m,
-  simp_rw [is_scalar_tower.algebra_map_apply R S (S ⊗[R] S), is_scalar_tower.algebra_map_smul]
-end
+submodule.quotient.is_scalar_tower _ _
 
 /-- The quotient map `I → Ω[S⁄R]` with `I` being the kernel of `S ⊗[R] S → S`. -/
 def kaehler_differential.from_ideal : kaehler_differential.ideal R S →ₗ[S ⊗[R] S] Ω[S⁄R] :=
@@ -190,13 +182,14 @@ 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],
+    dsimp only [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,
+    dsimp only [kaehler_differential.D_linear_map_apply],
+    rw [← linear_map.map_smul_of_tower ((kaehler_differential.ideal R S).to_cotangent) a,
+      ← linear_map.map_smul_of_tower ((kaehler_differential.ideal R S).to_cotangent) b, ← 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,
@@ -205,7 +198,7 @@ def kaehler_differential.D : derivation R S Ω[S⁄R] :=
       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) }
+  to_linear_map := 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
@@ -373,9 +366,9 @@ into `(kaehler_differential.ideal R S).cotangent_ideal` -/
 -- `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)
+def kaehler_differential.End_equiv_derivation' :
+  derivation R S Ω[S⁄R] ≃ₗ[R] derivation R S _ :=
+linear_equiv.comp_der ((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`. -/
@@ -538,7 +531,7 @@ variables (A B : Type*) [comm_ring A] [comm_ring B] [algebra R A] [algebra S B]
 variables [algebra A B] [is_scalar_tower R S B] [is_scalar_tower R A B]
 
 -- The map `(A →₀ A) →ₗ[A] (B →₀ B)`
-local notation `finsupp_map` := ((finsupp.map_range.linear_map (algebra.of_id A B).to_linear_map)
+local notation `finsupp_map` := ((finsupp.map_range.linear_map (algebra.linear_map A B))
   .comp (finsupp.lmap_domain A A (algebra_map A B)))
 
 lemma kaehler_differential.ker_total_map (h : function.surjective (algebra_map A B)) :
@@ -552,7 +545,7 @@ begin
     set.image_univ, map_sub, map_add],
   simp only [linear_map.comp_apply, finsupp.map_range.linear_map_apply, finsupp.map_range_single,
     finsupp.lmap_domain_apply, finsupp.map_domain_single, alg_hom.to_linear_map_apply,
-    algebra.of_id_apply, ← is_scalar_tower.algebra_map_apply, map_one, map_add, map_mul],
+    algebra.linear_map_apply, ← is_scalar_tower.algebra_map_apply, map_one, map_add, map_mul],
   simp_rw [sup_assoc, ← (h.prod_map h).range_comp],
   congr' 3,
   rw [sup_eq_right],
@@ -565,8 +558,6 @@ end presentation
 
 section exact_sequence
 
-local attribute [irreducible] kaehler_differential
-
 /- We have the commutative diagram
 A --→ B
 ↑     ↑
@@ -585,7 +576,7 @@ def derivation.comp_algebra_map [module A M] [module B M] [is_scalar_tower A B M
   leibniz' := λ a b, by simp,
   to_linear_map := d.to_linear_map.comp (is_scalar_tower.to_alg_hom R A B).to_linear_map }
 
-variables (R B)
+variables (R B) [smul_comm_class S A B]
 
 /-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄R]` given a square
 A --→ B
