Slow elaboration - algebra

Stream: general

[María Inés de Frutos Fernández]

I wrote a definition of adic completion of a ring at an ideal, but I am having trouble working with it because of slow elaboration. For instance, in the code below, elaboration of ring.adic_completion.algebra takes 11.3 seconds on my laptop (however, if I use the commented version instead, it takes virtually no time). Does anyone know what could be causing this to be so slow?

import ring_theory.ideal.operations

variables {R : Type*} [comm_ring R] (I : ideal R)

/-- The completion of a ring with respect to an ideal. -/
def ring.adic_completion :
subring (Π n : ℕ, (I ^ n • ⊤ : ideal R).quotient) :=
{ carrier  := { f | ∀ {m n} (h : m ≤ n), ideal.quotient.lift ( I ^ n • ⊤ : ideal R)
    (ideal.quotient.mk _)
    (by { intros a ha,
          rw [← ring_hom.mem_ker, ideal.mk_ker],
          rw [algebra.id.smul_eq_mul, ideal.mul_top]at ha ⊢,
          apply ideal.pow_le_pow h,
          exact ha }) (f n) = f m },
  one_mem'  := λ m n hmn, by { rw [pi.one_apply, pi.one_apply, ring_hom.map_one] },
  mul_mem'  := λ f g hf hg m n hmn, by rw [pi.mul_apply, pi.mul_apply, ring_hom.map_mul,
    hf hmn, hg hmn],
  zero_mem' := λ m n hmn, by rw [pi.zero_apply, pi.zero_apply, ring_hom.map_zero],
  add_mem'  := λ f g hf hg m n hmn, by rw [pi.add_apply, pi.add_apply,
    ring_hom.map_add, hf hmn, hg hmn],
  neg_mem'  := λ f hf m n hmn, by {rw [pi.neg_apply, pi.neg_apply, ring_hom.map_neg, hf hmn] }}

instance : comm_ring (ring.adic_completion I) := infer_instance

/-- The canonical ring map to the completion. -/
def ring.adic_completion.of : R →+* (ring.adic_completion I) :=
{ to_fun := λ x, ⟨λ (n : ℕ), (ideal.quotient.mk (I ^ n • ⊤ : ideal R) x), λ m n hmn, rfl⟩,
  map_one' := rfl,
  map_mul' := λ x y, rfl,
  map_zero' := rfl,
  map_add' := λ x y, rfl, }

set_option profiler true
instance : algebra R (ring.adic_completion I) :=
ring_hom.to_algebra (ring.adic_completion.of I)

/- instance : algebra R (ring.adic_completion I):=
{ smul := λ r x, (ring.adic_completion.of I r) * x,
  commutes' := λ r x, by {rw mul_comm},
  smul_def' := λ r x, rfl,
  ..(ring.adic_completion.of I) } -/

[María Inés de Frutos Fernández]

@Kevin Buzzard wrote a related example which is also taking quite long:

import ring_theory.ideal.operations

variables {ι : Type} (A : ι → Type) [∀ i, comm_ring (A i)]

def foo : subring (Π i, A i) := ⊤

def bar : ℤ →+* foo A := algebra_map ℤ ↥(foo A)

set_option profiler true
instance : algebra ℤ (foo A) :=
ring_hom.to_algebra (bar A)
/-
elaboration of foo.algebra took 4.99s
-/

[Kevin Buzzard]

This is bizarre because bar / ring.adic_completion.of is having no problem finding the ring instances. Maybe it's not the type class inference system which is taking so long?

[Kevin Buzzard]

ring_hom.to_algebra takes 14 seconds on my system in Maria's example, and it's a really innocuous def.

[Patrick Massot]

Why do you need this when we already have the algebraic story in docs#adic_completion and the topological one in https://leanprover-community.github.io/mathlib_docs/topology/algebra/nonarchimedean/adic_topology.html?

[Kevin Buzzard]

The adic completion of a ring is a ring, we don't seem to have this

[Kevin Buzzard]

(unless we missed it)

[Kevin Buzzard]

I mean, we _do_ have it now, because Maria's code above gives it us, but she's having real trouble using it and I have no idea what's going on

[María Inés de Frutos Fernández]

Right, I found adic_completion for modules but I couldn't find a ring version, so my plan was to use my definition of ring.adic_completion and put the adic topology on it using https://leanprover-community.github.io/mathlib_docs/topology/algebra/nonarchimedean/adic_topology.html.

[Johan Commelin]

Should the adic completion of R as a ring be defeq to its adic completion as R-module over itself? I assume this might come in handy at times?

[Johan Commelin]

On the other hand, we probably want to be able to say that ℤ_[p] is the adic completion of ℤ as ideal.span {p}, but that certainly won't be by definition. So maybe we need a predicte is_adic_completion?

[Johan Commelin]

On the other hand, we will need a construction anyway. It would be nice if it could reuse the construction for modules.

[Eric Wieser]

(deleted)

[Patrick Massot]

Kevin Buzzard said:

The adic completion of a ring is a ring, we don't seem to have this

We certainly have it for the topological story.

[Eric Wieser]

Why not make it a subalgebra rather than a subring?

def ring.adic_completion :
subalgebra R (Π n : ℕ, (I ^ n • ⊤ : ideal R).quotient) :=
{ carrier  := { f | ∀ {m n} (h : m ≤ n), ideal.quotient.lift ( I ^ n • ⊤ : ideal R)
    (ideal.quotient.mk _)
    (by { intros a ha,
          rw [← ring_hom.mem_ker, ideal.mk_ker],
          rw [algebra.id.smul_eq_mul, ideal.mul_top]at ha ⊢,
          apply ideal.pow_le_pow h,
          exact ha }) (f n) = f m },
  mul_mem'  := λ f g hf hg m n hmn, by rw [pi.mul_apply, pi.mul_apply, ring_hom.map_mul,
    hf hmn, hg hmn],
  add_mem'  := λ f g hf hg m n hmn, by rw [pi.add_apply, pi.add_apply,
    ring_hom.map_add, hf hmn, hg hmn],
  algebra_map_mem' := λ r m n h, rfl }

[Eric Wieser]

Then the instance you want already exists

[Patrick Massot]

docs#uniform_space.completion.comm_ring

[Patrick Massot]

Johan Commelin said:

Should the adic completion of R as a ring be defeq to its adic completion as R-module over itself? I assume this might come in handy at times?

In the topological story I took great care to ensure this. See https://github.com/leanprover-community/mathlib/blob/d6fd5f5fc4d020d0cec5af2106c7bafee45108ab/src/topology/algebra/nonarchimedean/adic_topology.lean#L36-L39

[Kevin Buzzard]

Aah I see -- so we topologise R with the adic topology and then complete the corresponding topological ring

[María Inés de Frutos Fernández]

Patrick Massot said:

docs#uniform_space.completion.comm_ring

Thanks!

[Kevin Buzzard]

None of this explains why it takes 5 seconds to elaborate

import ring_theory.ideal.operations

variables {ι : Type} (A : ι → Type) [∀ i, comm_ring (A i)]

def foo : subring (Π i, A i) := ⊤

def bar : ℤ →+* foo A := algebra_map ℤ ↥(foo A)

set_option profiler true
instance : algebra ℤ (foo A) :=
ring_hom.to_algebra (bar A)
/-
elaboration of foo.algebra took 4.99s
-/

which to me still remains incomprehensible

[Eric Wieser]

It takes 48s for me on gitpod

[Johan Commelin]

I agree that this elaboration issue is bad.

[Johan Commelin]

import ring_theory.ideal.operations

variables {ι : Type} (A : ι → Type) [∀ i, comm_semiring (A i)]

def foo : subsemiring (Π i, A i) := ⊤

def bar : ℕ →+* foo A := algebra_map ℕ ↥(foo A)

set_option profiler true
instance : algebra ℕ (foo A) :=
ring_hom.to_algebra (bar A)
/-
elaboration of foo.algebra took 4.99s
-/

is takes only 33% of the time, compared to Kevin's MWE, on my box.

[Johan Commelin]

The difference between ring and semiring shouldn't have such an impact...