Local degree of global field

Stream: Is there code for X?

[David Ang]

Assume the AKLB setup. Do we have the notion of "the unique prime of K below a prime of L"? Here is my attempt at defining the absolute local degree [K_v : Q_p] for a prime v of K and the unique prime p of Q below it:

import Mathlib

namespace IsDedekindDomain.HeightOneSpectrum

variable {A B : Type _} (K L : Type _) [CommRing A] [CommRing B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Field K] [Field L] [Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L]
  [Algebra K L] [IsFractionRing A K] [IsFractionRing B L] [h : IsIntegralClosure B A L]
  [IsScalarTower A B L] [IsScalarTower A K L] (v : HeightOneSpectrum A) (w : HeightOneSpectrum B)

instance : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra A L

instance : Algebra (v.adicCompletion K) (w.adicCompletion L) := sorry

noncomputable def localDeg : ℕ := FiniteDimensional.finrank (v.adicCompletion K) (w.adicCompletion L)

variable (A) in
noncomputable def below : HeightOneSpectrum A :=
  ⟨.comap .., Ideal.comap_isPrime .., w.ne_bot ∘ Ideal.eq_bot_of_comap_eq_bot⟩

noncomputable def absLocalDeg [IsIntegralClosure A ℤ K] : ℕ := (v.below ℤ K).localDeg ℚ K v

end IsDedekindDomain.HeightOneSpectrum

I can't seem to fill in the first instance due to some instance synthesis error, and the second instance seems to require some non-trivial input (the tensor product of K and Q_p is a sum of K_v's). Is there a better way to do this?

[Kevin Buzzard]

A suggestion of I think Amelia was (P : Ideal A) (Q : Ideal B) [Algebra (A\/P) (B\/Q)] [IsScalarTower A (A\/P) (B\/Q)] which puts all the information in the typeclass inference system and works because B/Q is already an A-algebra via the obvious map.

[Kevin Buzzard]

Note that the tensor product of K and Q_p is not K_v, it's the direct sum of K_{v'} as v' runs over all the primes above p.

[Kevin Buzzard]

The instance synthesis error is because it's not reasonable to ask typeclass inference to pull L out of the hat when the statement of the result just mentions A and B. We need some kind of [IsAKLBsetup A K L B] predicate which enables Lean to find all of A,B,K,L given only some of them.

[Kevin Buzzard]

@Richard Hill -- did you ever experiment with such a set-up?

[Richard Hill]

I did experiment with defining the unique prime of K below a prime of L. I used Ideal.comap to construct this function. I don't think such a function is in Mathlib.

The local degree is the product of Ideal.ramificationIdxand Ideal.inertiaDeg. Quite a lot is proved about these in the context of Dedekind domains (in the file Mathlib.NumberTheory.RamificationInertia).

[David Ang]

The statement Algebra.IsIntegral A B only needs A and B but mathlib only has IsIntegralClosure.isIntegral_algebra which needs the L. Seems like I have to change L to something like FractionRing B?

[David Ang]

I'm aware that the ramification inertia file exists, but feels like it's weird to define my local degree as a product of ramification and inertia, since it's a perfectly good definition by itself.

[David Ang]

Something like this works?

import Mathlib

namespace IsDedekindDomain.HeightOneSpectrum

variable {A B : Type _} (K L : Type _) [CommRing A] [CommRing B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Field K] [Field L] [Algebra A B] [Algebra A K] [Algebra A L] [Algebra B L]
  [Algebra K L] [IsFractionRing A K] [IsFractionRing B L] [IsIntegralClosure B A L]
  [IsScalarTower A B L] [IsScalarTower A K L] (v : HeightOneSpectrum A) (w : HeightOneSpectrum B)

noncomputable def localDeg : ℕ :=
  v.asIdeal.ramificationIdx (algebraMap A B) w.asIdeal *
    v.asIdeal.inertiaDeg (algebraMap A B) w.asIdeal

variable (A) in
noncomputable def below : HeightOneSpectrum A :=
  ⟨.comap .., Ideal.comap_isPrime .., w.ne_bot ∘ Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot L⟩

noncomputable def absLocalDeg [IsIntegralClosure A ℤ K] : ℕ :=
  (v.below ℤ K).localDeg v

end IsDedekindDomain.HeightOneSpectrum

I guess it's still not ideal.

[Richard Hill]

I think it might be better to define below v (and similarly the local degree) to depend on A and v (and implicitly B) but not on K or L or the place of K below v.
If you'd like to define the local degree as a special case of finrank, then you need to show that the completion of B at v is an algebra over the completion of A at below v. Once you have this, you can define the local degree to be the degree of the extension of fields of fractions (without mentioning K or L).

[David Ang]

What's the consensus on having the typeclass IsFractionRing R K over the specific FractionRing R?

[Kevin Buzzard]

As more and more of these issues come up I become more and more convinced that we need an IsAKLB prop class which is to four types what IsScalarTower is to three types. I don't think we should be cutting corners by restricting to FractionRing, this will surely lead to problems later on eg you can't use it with $\mathbb{Q}$.

[Johan Commelin]

I hope we can call it IsScalarSquare or something like that. :grinning: IsAKLB is pretty cryptic.