Ramification of infinite places

Stream: Is there code for X?

[Andrew Yang]

Do we have something close to this?

import Mathlib
open FiniteDimensional (finrank)
open NumberField (InfinitePlace)

lemma card_infinitePlace_eq_finrank_mul_of_odd {k K} [Field k] [Field K] [NumberField k]
    [NumberField K] [Algebra k K] [IsGalois k K] (h : Odd (finrank k K)) :
    Fintype.card (InfinitePlace K) = finrank k K * Fintype.card (InfinitePlace k) := sorry

[Riccardo Brasca]

cc @Xavier Roblot

[Kevin Buzzard]

I'm confused. What about $\mathbb{Q}(2^{1/3})/\mathbb{Q})$?

[Andrew Yang]

Oops I forgot IsGalois k K. Fixed.

[Xavier Roblot]

No, we do not have anything close to this result but it might not be too difficult to prove things in that direction. I’m quite busy this weekend but I’ll have more time to see what can be done during the week.

[Andrew Yang]

I have pushed a preliminary version here: https://github.com/leanprover-community/flt-regular/blob/master/FltRegular/NumberTheory/InfinitePlace.lean

[Junyan Xu]

I think we should replace the current definition

def ComplexEmbedding.IsRamified (φ : K →+* ℂ) : Prop :=
    ∃ (σ : K ≃ₐ[k] K), σ ≠ 1 ∧ IsConjGal φ σ

by ¬IsReal φ ∧ IsReal (φ.comp (algebraMap k K)), which extends to the case of non-Galois K/k. The idea is that algebraMap k K induces a homomorphism from the completion of k w.r.t. the absolute value induced by φ.comp (algebraMap k K) to the completion of K w.r.t. the absolute value induced by φ; the completion is ℝ or ℂ when the embedding is real or complex respectively, and we consider the extension of archimedean local fields ℝ → ℂ as having ramification index 2 (and inertial degree 1). (This is also the factor of 2 (mult) that appears in docs#NumberField.Units.dirichletUnitTheorem.logEmbedding_component docs#NumberField.mixedEmbedding.convexBodySum; the natural normalized absolute value on ℂ should be the usual one squared, but I don't think we should change it in mathlib ...)

[Xavier Roblot]

@Andrew Yang Well, I see you didn't wait in the end and wrote the code yourself :wink:

On a quick look, it looks great but I do agree with Junyan that the definition of IsRamified should be changed similarly to what he suggests. The definition of IsRamified for infinite place should be changed also accordingly. I'll have more time to look in details if needed later this week.

BTW, the normalised absolute value can be obtained using docs#NumberField.InfinitePlace.mult as it is done in docs#NumberField.InfinitePlace.prod_eq_abs_norm

[Andrew Yang]

Yeah I botched together a first version just so that the sorry can be filled.

[Andrew Yang]

I fixed the definition. I wonder if we should use ¬IsReal or IsComplex, or whether we should actually do

def InfinitePlace.IsUnramified (w : InfinitePlace K) : Prop :=
  mult (w.map (algebraMap k K)) = mult w

[Xavier Roblot]

Andrew Yang said:

I fixed the definition. I wonder if we should use ¬IsReal or IsComplex, or whether we should actually do

def InfinitePlace.IsUnramified (w : InfinitePlace K) : Prop :=
  mult (w.map (algebraMap k K)) = mult w

Yes, that's probably the best way to define it.