diamond in adele set-up

Stream: FLT

[Kevin Buzzard]

When reviewing FLT#682 I ran into a diamond in FLT.

Mathematically the issue is this. If $K$ is a number field then there's a ring $\mathbb{A}_K$ called the adeles of $K$, which is a product of two other rings called the finite adeles of $K$ and the infinite adeles of $K$. All of these constructions are functorial; if $L$ is another number field and $L$ is a $K$-algebra then the adeles of $L$ are naturally an algebra for the adeles of $K$ etc.

Right now in FLT this fact (if $L$ is a $K$-algebra then $\mathbb{A}_L$ is an $\mathbb{A}_K$-algebra) is an instance, constructed in FLT.NumberField.AdeleRing using docs#RingHom.toAlgebra and the ring homomorphism $\mathbb{A}_K\to\mathbb{A}_L$ constructed using docs#RingHom.prod and docs#RingHom.fst and docs#RingHom.snd (recall that the adeles are a product of the finite adeles and the infinite adeles).

So now when $L=K$ we have the following diamond:

import FLT.NumberField.AdeleRing

open NumberField AdeleRing

variable (K L : Type) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]

#synth Algebra (AdeleRing (𝓞 K) K) (AdeleRing (𝓞 K) K) -- Algebra.id (AdeleRing (𝓞 K) K)

#synth Algebra (AdeleRing (𝓞 K) K) (AdeleRing (𝓞 L) L) -- instAlgebraRingOfIntegers_fLT_1 K L

example : Algebra.id (AdeleRing (𝓞 K) K) = instAlgebraRingOfIntegers_fLT_1 K K := by
  ext
  simp
  -- still not rfl
  sorry

I can see several ways to proceed, e.g. remove an instance and then keep adding it locally when required thus accruing technical debt, muck about with instance priorities and get some technical debt that way, try hard to get rid of the diamond by removing the RingHom.fst and RingHom.prod dance etc etc. Does anyone have any advice?

[Kenny Lau]

the map AK -> AL is noncomputable right

[Yaël Dillies]

I don't understand, RingHom.prod, .fst and .snd commute definitionally. Are you sure nothing else is involved in the diamond?

[Yaël Dillies]

Can you show us the definition of instAlgebraRingOfIntegers_fLT_1?

[Kenny Lau]

@Yaël Dillies well the algebra contains a smul too, apart from that issue

[Kenny Lau]

and with my suspicion that AK_fin -> AL_fin is noncomputable, this makes the problem even harder

[Kenny Lau]

given a prime p of K, and x : K_p, you need to collect the primes p' above p, and then send completion to completion

[Yaël Dillies]

How is the smul defined here? If it's defined correctly, then everything should commute still

[Yaël Dillies]

Oh, are you claiming the diamond comes from under the "taking products" part?

[Kenny Lau]

@Yaël Dillies Kevin's post above saays that the Algebra instance is constructed using RingHom.toAlgebra, i.e. there was no smul defined

[Kenny Lau]

Yaël Dillies said:

Oh, are you claiming the diamond comes from under the "taking products" part?

i'm claiming both

[Matthew Jasper]

The reason these aren't def-eq is that the ring hom $K_v \to L_w$ is not def-eq to the identity for $K_v \to K_v$, because UniformSpace.Completion.map blocks def-eq.

[Matthew Jasper]

I haven't checked the infinite adele side, so there might be a problem there as well

[Yakov Pechersky]

This is going to be very difficult to resolve similarly to the reason that docs#FractionRing.liftAlgebra can't be global

[Kevin Buzzard]

How about resolving it by ensuring that the priority of the algebra instance is strictly less than that of Algebra.id?

[Yaël Dillies]

Sadly tweaking priorities is a hack and it will eventually blow to your face

[Kevin Buzzard]

yeah that was my initial instinct but how can it possibly go wrong?

[Yaël Dillies]

Typical place where it could blow up: Assume you have $M / L / K$ and prove something about $\mathbb A_K \to \mathbb A_L \to \mathbb A_M$; then you can't specialise $L = M$ to prove the analogous result for $\mathbb A_K \to \mathbb A_L$

[Kenny Lau]

isn't that what IsScalarTower is meant to solve

[Kenny Lau]

actually can IsScalarTower solve this one?

[Kenny Lau]

instead of requiring the two instances of Algebra A_K A_K to be equal, can we have a predicate saying that two algebras are equal?

[Kenny Lau]

i mean this feels like something like SMulCommClass