coercions in finite adele ring file

Stream: mathlib4

[Kevin Buzzard]

I'm trying to make sense of the coercions in file#Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing and it's exposing my ignorance.

In that file, R_hat R K is notation for FiniteIntegralAdeles R Kand by line 54 of the file we know this is a ring (all rings are commutative in this question). Also K_hat R K is notation for ProdAdicCompletions R K and by line 87 we know this is a ring too. A coercion (of types) is defined between them on line 99, an AddMonoidHom is defined between them on line 107, a RingHom on line 120 (no notation is used for some reason), K_hat is made into an algebra over R_hat on line 157, and it turns out that they're both R-algebras and an R-algebra hom is defined on line 172. Are all these needed?

[Filippo A. E. Nuccio]

Well, I would say that

• the ring structures are needed to even define the RingHom
• the different algebra structures are needed so that it is easy to walk around ScalarTowers: suppose you are in a field extension $L/K$ and you want to go from the finite integral adeles of $K$ to the adeles of $L$, so you have two ways. Having all these instances explicit makes it easy to show that the two "natural" paths are the same.
• The AddMonoidHom could be packed inside the RingHom, but I think it is better to unpack them, since you help class instances when looking for things that are already true at AddMonoid level (like $0\mapsto 0$) avoiding a long type class search.

[Kevin Buzzard]

But do we really need to define a coercion and also an algebra structure? Is that how it works?

[Filippo A. E. Nuccio]

Well, I think that the whole point is that there are three gadgets, the docs#algebraMap, then the external multiplication that is linked to the previous by docs#Algebra.algebraMap_eq_smul_one and (sometimes) a coercion that is the first field of the algebra map. Defining a coercion is only reasonable when the algebra map is injective, whereas the smul part is independent, so I think you cannot hope to get rid of the algebra map; and, on the other hand, in your setting you really want a coercion. So I am tempted to answer "yes" but I might be mathlib-biased.

[Kevin Buzzard]

I can get a coercion from an Algebra structure with open scoped algebraMap right? And I will probably want to open scoped algebraMap because there are many other rings and coercions involved. Will this lead to a diamond? Right now we have

noncomputable instance : Coe (R_hat R K) (K_hat R K) where coe x v := x v

(this is really { coe := fun x v ↦ ↑(x v) } and the up-arrow is Subtype.val, so it's a product of Subtype.vals), and also

instance ProdAdicCompletions.algebraCompletions : Algebra (R_hat R K) (K_hat R K) :=
  (FiniteIntegralAdeles.Coe.ringHom R K).toAlgebra

and after open scoped algebraMap we will have

scoped instance coeHTCT (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
    CoeHTCT R A :=
  ⟨Algebra.cast⟩

I have no understanding of all this coeHTCT business.

[Kevin Buzzard]

I guess one approach is that I can just soldier on and see what if anything breaks when I open the scope (which I will have to do for unrelated reasons).

[Filippo A. E. Nuccio]

I think you're safe:

example (x : R_hat R K) : (@Coe.coe (R_hat R K) (K_hat R K) _) x = (@CoeHTCT.coe (R_hat R K) (K_hat R K) _) x := by rfl

[Kevin Buzzard]

In Lean 3 I would be happy with that argument but

example (x : R_hat R K) : (@Coe.coe (R_hat R K) (K_hat R K) _) x =
  (@CoeHTCT.coe (R_hat R K) (K_hat R K) _) x := by with_reducible rfl -- fails

[Filippo A. E. Nuccio]

forget it...

[Filippo A. E. Nuccio]

(deleted)

[Christian Merten]

But

example (x : R_hat R K) : (@Coe.coe (R_hat R K) (K_hat R K) _) x =
  (@CoeHTCT.coe (R_hat R K) (K_hat R K) _) x := by with_reducible_and_instances rfl -- succeeds

works. Don't ask me what the difference is, but I believe someone mentioned here on Zulip at somepoint that this is sufficient.

[Filippo A. E. Nuccio]

Oh, and whenever "someone" finds the "somepoint", please post it here! I am very curious... :smile: :point:

[Filippo A. E. Nuccio]

OK, some updates after playing around a little bit: I have changed instance Coe to def Coe and the effect (after some fixing) is that

1. I can find

#synth Algebra (R_hat R K) (K_hat R K) --ProdAdicCompletions.algebraCompletions R K

#synth CoeHTCT (R_hat R K) (K_hat R K) -- failed to synthetize
#synth Coe (R_hat R K) (K_hat R K) -- failed to synthetize

which are both reasonable, as I have not open scoped algebraMap

2. If I open scoped it, I get

#synth Algebra (R_hat R K) (K_hat R K)

open scoped algebraMap

#synth CoeHTCT (R_hat R K) (K_hat R K) -- algebraMap.coeHTCT (R_hat R K) (K_hat R K)
#synth Coe (R_hat R K) (K_hat R K) -- failed to synthetize

showing that the two are not "really really" equal.

3. This CoeHTCT is really the algebraCast, and this works

open scoped algebraMap

example (x : R_hat R K) (hx : x= 0) : (↑x : (K_hat R K))= 0 := by
  rw [hx]
  rfl

4. Changing rfl to both with_reducible rfl or with_reducible_and_instances_rfl fails:

open scoped algebraMap

example (x : R_hat R K) (hx : x= 0) : (↑x : (K_hat R K))= 0 := by
  rw [hx]
  with_reducible rfl -- The rfl tactic failed.

example (x : R_hat R K) (hx : x= 0) : (↑x : (K_hat R K))= 0 := by
  rw [hx]
  with_reducible_and_instances rfl -- The rfl tactic failed.

[Filippo A. E. Nuccio]

The reason why I tested all this was because I wanted to try to get rid of the Coe instance, using only the algebra map and then benefitting of the CoeHTCT. The upshot is that @Kevin Buzzard is not alone in having no understanding of all this coeHTCT business.

[Kevin Buzzard]

I have just decided to plough on and see what happens.

My next question is: if I have four commutative rings in a commutative square (with all the arrows being Algebra maps), say A -> B -> D and A -> C -> D, and if I have some subring D' of D containing the image of B and C, and I promote D' to a type, and I define [Algebra B D'] and [Algebra C D'] then should I also make IsScalarTower X Y Z for (X,Y,Z) in (A,B,D'),(A,D',D),(B,D',D),(A,C,D'),(C,D',D)? Again I'm just experimenting and seeing what I'll need. Here A=R, B=K, C=R-hat, D=prod_v K_v and D' is the finite adeles.

[Filippo A. E. Nuccio]

The second, third and fourth should follow from docs#IsScalarTower.subalgebra'

[Filippo A. E. Nuccio]

But I confess I am not writing down the diagrams, so something could be the wrong way around.

[Kevin Buzzard]

They don't because finite adeles are a definition and it's not reducible because of all the trouble we had when we tried that with integer rings.

I don't object to adding them! I just don't know if I need them. I was going to find out by only adding them when I need them, but I've proved them all.