chore(RingTheory/AdicCompletion): make AdicCompletion.map linear on linear maps

Mathlib/RingTheory/AdicCompletion/Basic.lean

@@ -596,6 +596,19 @@ lemma eval_lift_apply (f : ∀ (n : ℕ), M →ₗ[R] N ⧸ (I ^ n • ⊤ : Sub
     (n : ℕ) (x : M) : (lift I f h x).val n = f n x :=
   rfl
 
+lemma lift_add (f g : ∀ (n : ℕ), M →ₗ[R] N ⧸ (I ^ n • ⊤ : Submodule R N))
+    (hf : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m)
+    (hg : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ g n = g m) :
+    lift I (f + g) (fun h ↦ by simp [LinearMap.comp_add, hf h, hg h]) =
+      lift I f hf + lift I g hg := by
+  ext; simp
+
+theorem lift_smul (c : R) (f : ∀ n, M →ₗ[R] N ⧸ (I ^ n • ⊤ : Submodule R N))
+    (hf : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m) :
+    lift I (c • f) (fun h ↦ by simp [LinearMap.comp_smul, hf h]) =
+      c • (lift I f hf) := by
+  ext; simp [val_smul]
+
 section Bijective
 
 variable {I}

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

@@ -40,14 +40,20 @@ variable {T : Type*} [AddCommGroup T] [Module (AdicCompletion I R) T]
 namespace LinearMap
 
 /-- The induced linear map on the quotients mod `I • ⊤`. -/
-def reduceModIdeal (f : M →ₗ[R] N) :
-    M ⧸ (I • ⊤ : Submodule R M) →ₗ[R ⧸ I] N ⧸ (I • ⊤ : Submodule R N) :=
-  LinearMap.extendScalarsOfSurjective Ideal.Quotient.mk_surjective <|
+def reduceModIdeal :
+    (M →ₗ[R] N) →ₗ[R] M ⧸ (I • ⊤ : Submodule R M) →ₗ[R ⧸ I] N ⧸ (I • ⊤ : Submodule R N) where
+  toFun f := LinearMap.extendScalarsOfSurjective Ideal.Quotient.mk_surjective <|
     Submodule.mapQ (I • ⊤ : Submodule R M) (I • ⊤ : Submodule R N) f
       (fun x hx ↦ by
         refine Submodule.smul_induction_on hx (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)
         · simp [Submodule.smul_mem_smul hr Submodule.mem_top]
         · simp [Submodule.add_mem _ hx hy])
+  map_add' f g := LinearMap.ext fun x ↦ by
+    rcases Submodule.Quotient.mk_surjective _ x with ⟨x, rfl⟩
+    simp
+  map_smul' r f := LinearMap.ext fun x ↦ by
+    rcases Submodule.Quotient.mk_surjective _ x with ⟨x, rfl⟩
+    simp
 
 @[simp]
 theorem reduceModIdeal_apply (f : M →ₗ[R] N) (x : M) :
@@ -101,15 +107,22 @@ theorem map_zero : map I (0 : M →ₗ[R] N) = 0 :=
 end AdicCauchySequence
 
 /-- A linear map induces a map on adic completions. -/
-def map (f : M →ₗ[R] N) :
-    AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I N where
-  __ := AdicCompletion.lift I (fun n ↦ reduceModIdeal (I ^ n) f ∘ₗ AdicCompletion.eval I M n)
-    (fun {m n} hmn ↦ by rw [← comp_assoc, AdicCompletion.transitionMap_comp_reduceModIdeal,
-        comp_assoc, transitionMap_comp_eval])
-  map_smul' r x := by
-    ext
-    dsimp
-    rw [val_smul_eq_evalₐ_smul, val_smul_eq_evalₐ_smul, map_smul]
+def map : (M →ₗ[R] N) →ₗ[R] (AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I N) where
+  toFun f :=
+    { __ := AdicCompletion.lift I (fun n ↦ reduceModIdeal (I ^ n) f ∘ₗ AdicCompletion.eval I M n)
+        (fun {m n} hmn ↦ by rw [← comp_assoc, AdicCompletion.transitionMap_comp_reduceModIdeal,
+          comp_assoc, transitionMap_comp_eval])
+      map_smul' r x := by
+        ext
+        dsimp
+        rw [val_smul_eq_evalₐ_smul, val_smul_eq_evalₐ_smul, map_smul] }
+  map_add' f g := LinearMap.ext fun _ ↦ by
+    simp only [map_add, restrictScalars_add, add_comp, ← Pi.add_def, coe_mk, coe_toAddHom,
+      add_apply]
+    rw [← LinearMap.add_apply, ← lift_add]
+  map_smul' c f := LinearMap.ext fun _ ↦ by
+    simp only [map_smul, restrictScalars_smul, coe_mk, coe_toAddHom, RingHom.id_apply, smul_apply]
+    simp_rw [← LinearMap.smul_apply, ← lift_smul, Pi.smul_def, LinearMap.smul_comp]
 
 @[simp]
 theorem map_val_apply (f : M →ₗ[R] N) {n : ℕ} (x : AdicCompletion I M) :