mathlib

mathlib copied to clipboard

We define the finite adèle ring of a Dedekind domain and show that it is a commutative ring.

---

@riccardobrasca is right and that we should be using the algebra typeclass more here. Even before we get to the adèles I think there are various little gaps to fill.

The job of algebra is to make it convenient to work with canonical ring morphisms and we have lots of these here. For example, I claim what is currently called inj_adic_completion_integers should really be instance : algebra R $ v.adic_completion_integers K.

Indeed, denoting the completion by $K_v$ and its integers by $R_v$, we have the commutative square:

R    ⟶ K
↓        ↓
R_v ⟶ K_v

and from this there are five algebra classes (the fifth one corresponding to the diagonal map). Of course algebra R K is part of the input but I think the other four are missing and I think should probably be added.

There will also be two is_scalar_tower instances and I guess also no_zero_smul_divisors instance(s) for the injectivity.

Hmm, even the following seems to be missing:

import topology.algebra.uniform_ring
import algebra.algebra.basic

noncomputable theory

variables (A : Type*) [comm_ring A] [uniform_space A] [uniform_add_group A]
variables [topological_ring A] [uniform_add_group A]

local notation `A_hat` := uniform_space.completion A

instance ring_completion.algebra : algebra A A_hat :=
(uniform_space.completion.coe_ring_hom : A →+* A_hat).to_algebra

@[simp] lemma ring_completion.algebra_smul_eq (a : A) (x : A_hat) :
  a • x = (a : A_hat) * x :=
rfl

variables (R : Type*) [comm_ring R] [algebra R A]

instance ring_completion.algebra' : algebra R A_hat :=
((uniform_space.completion.coe_ring_hom : A →+* A_hat).comp (algebra_map R A)).to_algebra

@[simp] lemma ring_completion.algebra'_smul_eq (r : R) (x : A_hat) :
  r • x = (algebra_map R A r : A_hat) * x :=
rfl

instance ring_completion.is_scalar_tower : is_scalar_tower R A A_hat :=
⟨λ r k x,
begin
  simp only [←mul_assoc, algebra.smul_def, map_mul],
  congr,
end⟩

I'll look at this again first thing tomorrow and see if I can PR the missing general results.

I'll look at this again first thing tomorrow and see if I can PR the missing general results.

Did you end up PRing this? I have been away at a conference, but now that I'm back I'll start working on your suggestions and Riccardo's.

Did you end up PRing this?

Not yet (though I was hoping to get to it today). However if you can do it, then that would be even better.

Not yet (though I was hoping to get to it today). However if you can do it, then that would be even better.

I can do it (but I don't know if I'll get to it today).

Is it ready to be merged now?

@eric-wieser, could you review the last changes? I think I replied to all of your comments.

Just in case you missed it, I also responded to an earlier comment at https://github.com/leanprover-community/mathlib/pull/14249#discussion_r1114263296

:v: mariainesdff can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests