chore(RingTheory/AdicCompletion): manual instances (#14534)

Instead of inferring `AddCommGroup`, `Module`, etc. instances for `AdicCompletion I M` from being a submodule, we explicitly spell out the definitions to improve performance.

Also marks some definitions as `noncomputable` to save time spent on compilation.

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Adic.20completion.20is.20slow.

Author: chrisflav

Mathlib/LinearAlgebra/SModEq.lean

@@ -92,11 +92,31 @@ theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] :=
   simp_rw [Quotient.mk_smul, hxy]
 #align smodeq.smul SModEq.smul
 
+lemma nsmul (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U] := by
+  rw [SModEq.def] at hxy ⊢
+  simp_rw [Quotient.mk_smul, hxy]
+
+lemma zsmul (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U] := by
+  rw [SModEq.def] at hxy ⊢
+  simp_rw [Quotient.mk_smul, hxy]
+
 theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I])
     (hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I] := by
   simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
   rw [hxy₁, hxy₂]
 
+lemma pow {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
+    x ^ n ≡ y ^ n [SMOD I] := by
+  simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
+  rw [hxy]
+
+lemma neg (hxy : x ≡ y [SMOD U]) : - x ≡ - y [SMOD U] := by
+  simpa only [SModEq.def, Quotient.mk_neg, neg_inj]
+
+lemma sub (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U] := by
+  rw [SModEq.def] at hxy₁ hxy₂ ⊢
+  simp_rw [Quotient.mk_sub, hxy₁, hxy₂]
+
 theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
 #align smodeq.zero SModEq.zero
 

Mathlib/RingTheory/AdicCompletion/Algebra.lean

@@ -21,6 +21,8 @@ providing as much API as possible.
 
 -/
 
+suppress_compilation
+
 open Submodule
 
 variable {R : Type*} [CommRing R] (I : Ideal R)
@@ -45,6 +47,11 @@ theorem transitionMap_map_mul {m n : ℕ} (hmn : m ≤ n) (x y : R ⧸ (I ^ n 
     transitionMap I R hmn (x * y) = transitionMap I R hmn x * transitionMap I R hmn y :=
   Quotient.inductionOn₂' x y (fun _ _ ↦ rfl)
 
+@[local simp]
+theorem transitionMap_map_pow {m n a : ℕ} (hmn : m ≤ n) (x : R ⧸ (I ^ n • ⊤ : Ideal R)) :
+    transitionMap I R hmn (x ^ a) = transitionMap I R hmn x ^ a :=
+  Quotient.inductionOn' x (fun _ ↦ rfl)
+
 /-- `AdicCompletion.transitionMap` as an algebra homomorphism. -/
 def transitionMapₐ {m n : ℕ} (hmn : m ≤ n) :
     R ⧸ (I ^ n • ⊤ : Ideal R) →ₐ[R] R ⧸ (I ^ m • ⊤ : Ideal R) :=
@@ -59,11 +66,35 @@ def subalgebra : Subalgebra R (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) :=
 def subring : Subring (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) :=
   Subalgebra.toSubring (subalgebra I)
 
-instance : CommRing (AdicCompletion I R) :=
-  inferInstanceAs <| CommRing (subring I)
+instance : Mul (AdicCompletion I R) where
+  mul x y := ⟨x.val * y.val, by simp [x.property, y.property]⟩
 
-instance : Algebra R (AdicCompletion I R) :=
-  inferInstanceAs <| Algebra R (subalgebra I)
+instance : One (AdicCompletion I R) where
+  one := ⟨1, by simp⟩
+
+instance : NatCast (AdicCompletion I R) where
+  natCast n := ⟨n, fun _ ↦ rfl⟩
+
+instance : IntCast (AdicCompletion I R) where
+  intCast n := ⟨n, fun _ ↦ rfl⟩
+
+instance : Pow (AdicCompletion I R) ℕ where
+  pow x n := ⟨x.val ^ n, fun _ ↦ by simp [x.property]⟩
+
+instance : CommRing (AdicCompletion I R) :=
+  let f : AdicCompletion I R → ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R) := Subtype.val
+  Subtype.val_injective.commRing f rfl rfl
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
+
+instance : Algebra R (AdicCompletion I R) where
+  toFun r := ⟨algebraMap R (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) r, by simp⟩
+  map_one' := Subtype.ext <| map_one _
+  map_mul' x y := Subtype.ext <| map_mul _ x y
+  map_zero' := Subtype.ext <| map_zero _
+  map_add' x y := Subtype.ext <| map_add _ x y
+  commutes' r x := Subtype.ext <| Algebra.commutes' r x.val
+  smul_def' r x := Subtype.ext <| Algebra.smul_def' r x.val
 
 @[simp]
 theorem val_one (n : ℕ) : (1 : AdicCompletion I R).val n = 1 :=
@@ -100,11 +131,35 @@ def AdicCauchySequence.subalgebra : Subalgebra R (ℕ → R) :=
 def AdicCauchySequence.subring : Subring (ℕ → R) :=
   Subalgebra.toSubring (AdicCauchySequence.subalgebra I)
 
-instance : CommRing (AdicCauchySequence I R) :=
-  inferInstanceAs <| CommRing (AdicCauchySequence.subring I)
+instance : Mul (AdicCauchySequence I R) where
+  mul x y := ⟨x.val * y.val, fun hmn ↦ SModEq.mul (x.property hmn) (y.property hmn)⟩
+
+instance : One (AdicCauchySequence I R) where
+  one := ⟨1, fun _ ↦ rfl⟩
+
+instance : NatCast (AdicCauchySequence I R) where
+  natCast n := ⟨n, fun _ ↦ rfl⟩
 
-instance : Algebra R (AdicCauchySequence I R) :=
-  inferInstanceAs <| Algebra R (AdicCauchySequence.subalgebra I)
+instance : IntCast (AdicCauchySequence I R) where
+  intCast n := ⟨n, fun _ ↦ rfl⟩
+
+instance : Pow (AdicCauchySequence I R) ℕ where
+  pow x n := ⟨x.val ^ n, fun hmn ↦ SModEq.pow n (x.property hmn)⟩
+
+instance : CommRing (AdicCauchySequence I R) :=
+  let f : AdicCauchySequence I R → (ℕ → R) := Subtype.val
+  Subtype.val_injective.commRing f rfl rfl
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
+
+instance : Algebra R (AdicCauchySequence I R) where
+  toFun r := ⟨algebraMap R (∀ _, R) r, fun _ ↦ rfl⟩
+  map_one' := Subtype.ext <| map_one _
+  map_mul' x y := Subtype.ext <| map_mul _ x y
+  map_zero' := Subtype.ext <| map_zero _
+  map_add' x y := Subtype.ext <| map_add _ x y
+  commutes' r x := Subtype.ext <| Algebra.commutes' r x.val
+  smul_def' r x := Subtype.ext <| Algebra.smul_def' r x.val
 
 @[simp]
 theorem one_apply (n : ℕ) : (1 : AdicCauchySequence I R) n = 1 :=

Mathlib/RingTheory/AdicCompletion/Basic.lean

@@ -27,6 +27,7 @@ with respect to an ideal `I`:
 
 -/
 
+suppress_compilation
 
 open Submodule
 
@@ -213,11 +214,43 @@ def submodule : Submodule R (∀ n : ℕ, M ⧸ (I ^ n • ⊤ : Submodule R M))
     rw [Pi.add_apply, Pi.add_apply, LinearMap.map_add, hf hmn, hg hmn]
   smul_mem' c f hf m n hmn := by rw [Pi.smul_apply, Pi.smul_apply, LinearMap.map_smul, hf hmn]
 
+instance : Zero (AdicCompletion I M) where
+  zero := ⟨0, by simp⟩
+
+instance : Add (AdicCompletion I M) where
+  add x y := ⟨x.val + y.val, by simp [x.property, y.property]⟩
+
+instance : Neg (AdicCompletion I M) where
+  neg x := ⟨- x.val, by simp [x.property]⟩
+
+instance : Sub (AdicCompletion I M) where
+  sub x y := ⟨x.val - y.val, by simp [x.property, y.property]⟩
+
+instance : SMul ℕ (AdicCompletion I M) where
+  smul n x := ⟨n • x.val, by simp [x.property]⟩
+
+instance : SMul ℤ (AdicCompletion I M) where
+  smul n x := ⟨n • x.val, by simp [x.property]⟩
+
 instance : AddCommGroup (AdicCompletion I M) :=
-  inferInstanceAs <| AddCommGroup (submodule I M)
+  let f : AdicCompletion I M → ∀ n, M ⧸ (I ^ n • ⊤ : Submodule R M) := Subtype.val
+  Subtype.val_injective.addCommGroup f rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+
+instance : SMul R (AdicCompletion I M) where
+  smul r x := ⟨r • x.val, by simp [x.property]⟩
 
 instance : Module R (AdicCompletion I M) :=
-  inferInstanceAs <| Module R (submodule I M)
+  let f : AdicCompletion I M →+ ∀ n, M ⧸ (I ^ n • ⊤ : Submodule R M) :=
+    { toFun := Subtype.val, map_zero' := rfl, map_add' := fun _ _ ↦ rfl }
+  Subtype.val_injective.module R f (fun _ _ ↦ rfl)
+
+/-- The canonical inclusion from the completion to the product. -/
+@[simps]
+def incl : AdicCompletion I M →ₗ[R] (∀ n, M ⧸ (I ^ n • ⊤ : Submodule R M)) where
+  toFun x := x.val
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 /-- The canonical linear map to the completion. -/
 def of : M →ₗ[R] AdicCompletion I M where
@@ -279,6 +312,11 @@ theorem val_add (n : ℕ) (f g : AdicCompletion I M) : (f + g).val n = f.val n +
 theorem val_sub (n : ℕ) (f g : AdicCompletion I M) : (f - g).val n = f.val n - g.val n :=
   rfl
 
+@[simp]
+theorem val_sum {α : Type*} (s : Finset α) (f : α → AdicCompletion I M) (n : ℕ) :
+    (Finset.sum s f).val n = Finset.sum s (fun a ↦ (f a).val n) := by
+  simp_rw [← incl_apply, map_sum, Finset.sum_apply]
+
 /- No `simp` attribute, since it causes `simp` unification timeouts when considering
 the `AdicCompletion I R` module instance on `AdicCompletion I M` (see `AdicCompletion/Algebra`). -/
 theorem val_smul (n : ℕ) (r : R) (f : AdicCompletion I M) : (r • f).val n = r • f.val n :=
@@ -361,14 +399,39 @@ def submodule : Submodule R (ℕ → M) where
     intro r f hf m n hmn
     exact SModEq.smul (hf hmn) r
 
-instance : CoeFun (AdicCauchySequence I M) (fun _ ↦ ℕ → M) where
-  coe f := f.val
+instance : Zero (AdicCauchySequence I M) where
+  zero := ⟨0, fun _ ↦ rfl⟩
+
+instance : Add (AdicCauchySequence I M) where
+  add x y := ⟨x.val + y.val, fun hmn ↦ SModEq.add (x.property hmn) (y.property hmn)⟩
+
+instance : Neg (AdicCauchySequence I M) where
+  neg x := ⟨- x.val, fun hmn ↦ SModEq.neg (x.property hmn)⟩
+
+instance : Sub (AdicCauchySequence I M) where
+  sub x y := ⟨x.val - y.val, fun hmn ↦ SModEq.sub (x.property hmn) (y.property hmn)⟩
 
-instance : AddCommGroup (AdicCauchySequence I M) :=
-  inferInstanceAs <| AddCommGroup (AdicCauchySequence.submodule I M)
+instance : SMul ℕ (AdicCauchySequence I M) where
+  smul n x := ⟨n • x.val, fun hmn ↦ SModEq.nsmul (x.property hmn) n⟩
+
+instance : SMul ℤ (AdicCauchySequence I M) where
+  smul n x := ⟨n • x.val, fun hmn ↦ SModEq.zsmul (x.property hmn) n⟩
+
+instance : AddCommGroup (AdicCauchySequence I M) := by
+  let f : AdicCauchySequence I M → (ℕ → M) := Subtype.val
+  apply Subtype.val_injective.addCommGroup f rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+
+instance : SMul R (AdicCauchySequence I M) where
+  smul r x := ⟨r • x.val, fun hmn ↦ SModEq.smul (x.property hmn) r⟩
 
 instance : Module R (AdicCauchySequence I M) :=
-  inferInstanceAs <| Module R (AdicCauchySequence.submodule I M)
+  let f : AdicCauchySequence I M →+ (ℕ → M) :=
+    { toFun := Subtype.val, map_zero' := rfl, map_add' := fun _ _ ↦ rfl }
+  Subtype.val_injective.module R f (fun _ _ ↦ rfl)
+
+instance : CoeFun (AdicCauchySequence I M) (fun _ ↦ ℕ → M) where
+  coe f := f.val
 
 @[simp]
 theorem zero_apply (n : ℕ) : (0 : AdicCauchySequence I M) n = 0 :=

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

@@ -24,6 +24,8 @@ In this file we establish functorial properties of the adic completion.
 
 -/
 
+suppress_compilation
+
 variable {R : Type*} [CommRing R] (I : Ideal R)
 variable {M : Type*} [AddCommGroup M] [Module R M]
 variable {N : Type*} [AddCommGroup N] [Module R N]
@@ -191,12 +193,6 @@ theorem map_zero : map I (0 : M →ₗ[R] N) = 0 := by
   ext
   simp
 
-@[simp]
-theorem val_sum {α : Type*} (s : Finset α) (f : α → AdicCompletion I M) (n : ℕ) :
-    (Finset.sum s f).val n = Finset.sum s (fun a ↦ (f a).val n) := by
-  change (Submodule.subtype (AdicCompletion.submodule I M) _) n = _
-  rw [map_sum, Finset.sum_apply, Submodule.coeSubtype]
-
 /-- A linear equiv induces a linear equiv on adic completions. -/
 def congr (f : M ≃ₗ[R] N) :
     AdicCompletion I M ≃ₗ[AdicCompletion I R] AdicCompletion I N :=