the ring of integers corresponding to decomposition field

Stream: maths

[Yongle Hu]

HI! I encountered a problem while formalizing the properties of the decomposition group. Assume B/A is a finite extension of Dedekind domains, K is the fraction ring of A, L is the fraction ring of B, and L/K is a Galois extension. Let P be a prime ideal lying over a prime ideal p of A. Let Dₚ be the decomposition group of P and Zₚ be the decomposition field, i.e., the intermediate field of L/K fixed by Dₚ.

My problem is: how to define the ring of integers Oₚ corresponding to Zₚ? If both K and L are number fields and A = 𝓞 K, B = 𝓞 L, then we can define it as 𝓞 Zₚ. However, in the general case, there seems to be no canonical definition.

I considered three possible approaches:

1. Define it as the integral closure of A in Zₚ. This would be a subalgebra of Zₚ / A. Then, we need to provide Algebra Oₚ B, Algebra Oₚ L, and instances of IsScalarTower. This might be the simplest approach. However, if we define the ring of integers corresponding to the inertia field in the same way, it might lead to a little mess.

2. Define it as a subalgebra of B/A. For example, we could define it as B ∩ Zₚ. Alternatively, we could define it as the subalgebra fixed by Gal(L/K). However, in the current Mathlib, there does not seem to be a notion of a subalgebra fixed by a group acting on B (only docs#IntermediateField.fixedField). I know that @Thomas Browning introduced a definition of A fixed by a group acting on B in #18560, but it seems that subalgebras fixed by a group acting on B also not introduced in that pr.

3. Define the ring using the properties it should satisfy, then construct one that fulfills those properties. The advantage of this approach is that it unifies with the number field case. However, I don't know how to best formalize these properties.

All three seem feasible, but I'm not sure which one is convenient in practice.

Here is my attempted code:

import Mathlib

variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A)
  (P : Ideal B) [P.IsPrime] [P.LiesOver p]
  (K L : Type*) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L]
  [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
  [IsIntegralClosure B A L] [FiniteDimensional K L]

/-- The decomposition group of `P` over `K`, is the stabilizer of `P` under the action of
  `Gal(L / K)`. -/
def decompositionGroup (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p] : Subgroup (L ≃ₐ[K] L) := sorry

variable {K} {L} in
/-- The `decompositionGroup` is consisting of all elements of the Galois group `L ≃ₐ[K] L` such
that keep `P` invariant. -/
theorem decompositionGroup_mem (σ : L ≃ₐ[K] L) :
    σ ∈ decompositionGroup K L p P ↔ Ideal.map (galRestrict A K L B σ) P = P := sorry

open IntermediateField FiniteDimensional

/-- The decomposition field of `P` over `K` is the fixed field of `decompositionGroup p P`. -/
def decompositionField : IntermediateField K L :=
  IntermediateField.fixedField (decompositionGroup K L p P)

/-- Defined it as an integral closure. -/
def decompositionRing : Subalgebra A (decompositionField p P K L) :=
  integralClosure A (decompositionField p P K L)

/-- Defined it as `B ∩ Zₚ`. -/
def decompositionRing' : Subalgebra A B :=
  ((decompositionField p P K L).toSubalgebra.restrictScalars A).comap (IsScalarTower.toAlgHom A B L)

class IsDecompositionRing (D : Type*) [CommRing D] where
  [isDedekindDomain : IsDedekindDomain D]
  [algebra_bot : Algebra A D] [module_finite : Module.Finite A D]
  [algebra_decompositionField : Algebra D (decompositionField p P K L)]
  [isFractionRing : IsFractionRing D (decompositionField p P K L)]
  [isScalarTower_bot : IsScalarTower A D (decompositionField p P K L)]
  [algebra_top : Algebra D B] [algebra_field : Algebra D L]
  [isScalarTower_top : IsScalarTower D B L]
  [isScalarTower_decompositionField : IsScalarTower D (decompositionField p P K L) L]
  [isScalarTower : IsScalarTower A D B]

attribute [instance] IsDecompositionRing.isDedekindDomain IsDecompositionRing.algebra_bot
  IsDecompositionRing.module_finite IsDecompositionRing.algebra_decompositionField
  IsDecompositionRing.isFractionRing IsDecompositionRing.isScalarTower_bot
  IsDecompositionRing.algebra_top IsDecompositionRing.algebra_field
  IsDecompositionRing.isScalarTower_top IsDecompositionRing.isScalarTower_decompositionField
  IsDecompositionRing.isScalarTower

[Andrew Yang]

Note that we already have docs#ValuationSubring.decompositionSubgroup (without any API)

[Yongle Hu]

Andrew Yang said:

Note that we already have docs#ValuationSubring.decompositionSubgroup (without any API)

I think this is a local setting, while I want to formalize it in the global setting.

[Andrew Yang]

I don't think it matters here. Your D is just the decompositionSubgroup of $B_P$ (as a valuation subring of $L$).

[Thomas Browning]

Can you give an example of a statement where you would need to define the decomposition ring?

[Yongle Hu]

Thomas Browning said:

Can you give an example of a statement where you would need to define the decomposition ring?

I need the decomposition ring to define the the decomposition ideal, and then prove some properties of the decomposition ideal, for example, P is the unique ideal lying over the decomposition ideal.

2024-11-19 000621.png

[Thomas Browning]

But rather than just defining the decomposition ideal for one choice of decomposition ring, wouldn't it be better to define it for any decomposition ring? (any ring and fraction field in an IsScalarTower satisfying certain assumptions)

[Yongle Hu]

That's a good idea! So should I write out the structure that the decomposition ring satisfies, for example

class IsDecompositionRing (D : Type*) [CommRing D] where
  [algebra_decompositionField : Algebra D (decompositionField p P K L)]
  [isFractionRing : IsFractionRing D (decompositionField p P K L)]
  ...

def decompositionIdeal (A B K L D : Type*) ... [CommRing D]
  [IsDecompositionRing p P K L D] : Ideal D := sorry

or should I directly use variables to express it, for example

def decompositionIdeal (A B K L D : Type*) ...  [CommRing D] ...
  [IsFractionRing D (decompositionField p P K L)] : Ideal D := sorrry

[Thomas Browning]

You might not even need to define the ideal, you might be able to get away with typeclass assumptions on the rings and fields, and a LiesOver assumption