Inertia subgroup, etc. for an infinite extension of algebraic number fields

We will use the following conventions:

• A place of an arbitrary field is a non-trivial AbsoluteValue of it to ℝ.
• A place is called finite, if it is non-archimedean.
• A place is called archimedean or infinite, if it is not non-archimedean.

References:

• J. W. S. Cassels. Global Fields. Chapter II in J. W. S. Cassels, A. Frohlich, editors, Algebraic Number Theory.

theorem AbsoluteValue.exists_ringHom_complex_of_not_isNonarchimedean {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (h1 : v.IsNontrivial) (h2 : ¬IsNonarchimedean ⇑v) : ∃ (φ : K →+* ℂ), NumberField.place φ ≈ v

Gelfand-Tornheim theorem: if a field K has an infinite place, then there exists an embedding K →+* ℂ such that the absolute value is equivalent to the usual absolute value on ℂ.

Proof: see E. Artin, Theory of Algebraic Numbers, pp. 45 and 67.

def AbsoluteValue.toValuation {R : Type u_1} [Ring R] [Nontrivial R] (v : AbsoluteValue R ℝ) (h : IsNonarchimedean ⇑v) : Valuation R NNReal

A non-archimedean absolute value is a valuation.

Equations

• v.toValuation h = { toFun := fun (x : R) => ⟨v x, ⋯⟩, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

theorem AbsoluteValue.toValuation_toFun_coe {R : Type u_1} [Ring R] [Nontrivial R] (v : AbsoluteValue R ℝ) (h : IsNonarchimedean ⇑v) (x : R) : ↑((v.toValuation h) x) = v x

Decomposition subgroup for a place

def AbsoluteValue.decompositionSubgroup (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) : Subgroup Gal(K/F)

The decomposition subgroup Dᵥ(K/F) in Gal(K/F) for a place v of K consists of all σ preserving the set {x | v x ≤ 1}. This definition also works for infinite places.

Equations

• AbsoluteValue.decompositionSubgroup F v = { carrier := {σ : Gal(K/F) | ⇑σ '' {x : K | v x ≤ 1} = {x : K | v x ≤ 1}}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem AbsoluteValue.mem_decompositionSubgroup_iff (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (σ : Gal(K/F)) : σ ∈ decompositionSubgroup F v ↔ ⇑σ '' {x : K | v x ≤ 1} = {x : K | v x ≤ 1}

theorem AbsoluteValue.apply_le_one_of_mem_decompositionSubgroup {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) {σ : Gal(K/F)} (h : σ ∈ decompositionSubgroup F v) {x : K} (hx : v x ≤ 1) : v (σ x) ≤ 1

theorem AbsoluteValue.apply_le_one_iff_of_mem_decompositionSubgroup {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) {σ : Gal(K/F)} (h : σ ∈ decompositionSubgroup F v) {x : K} : v (σ x) ≤ 1 ↔ v x ≤ 1

theorem AbsoluteValue.decompositionSubgroup_eq_of_isNonarchimedean (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (h : IsNonarchimedean ⇑v) : decompositionSubgroup F v = ValuationSubring.decompositionSubgroup F (v.toValuation h).valuationSubring

Our definition is the same as ValuationSubring.decompositionSubgroup for finite places.

Inertia subgroup for a place

def AbsoluteValue.inertiaSubgroup (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) : Subgroup Gal(K/F)

The inertia subgroup Iᵥ(K/F) in Gal(K/F) for a finite place v of K consists of all σ preserving the set {x | v x ≤ 1} and such that for all such x, v (σ x - x) < 1. For infinite places Iᵥ(K/F) is just defined to be the decomposition subgroup Dᵥ(K/F).

Equations

• One or more equations did not get rendered due to their size.

theorem AbsoluteValue.mem_inertiaSubgroup_iff (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (σ : Gal(K/F)) : σ ∈ inertiaSubgroup F v ↔ ⇑σ '' {x : K | v x ≤ 1} = {x : K | v x ≤ 1} ∧ (¬IsNonarchimedean ⇑v ∨ ∀ (x : K), v x ≤ 1 → v (σ x - x) < 1)

theorem AbsoluteValue.mem_inertiaSubgroup_iff_of_isNonarchimedean (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (h : IsNonarchimedean ⇑v) (σ : Gal(K/F)) : σ ∈ inertiaSubgroup F v ↔ ⇑σ '' {x : K | v x ≤ 1} = {x : K | v x ≤ 1} ∧ ∀ (x : K), v x ≤ 1 → v (σ x - x) < 1

theorem AbsoluteValue.mem_inertiaSubgroup_iff_of_not_isNonarchimedean (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (h : ¬IsNonarchimedean ⇑v) (σ : Gal(K/F)) : σ ∈ inertiaSubgroup F v ↔ ⇑σ '' {x : K | v x ≤ 1} = {x : K | v x ≤ 1}

theorem AbsoluteValue.inertiaSubgroup_le_decompositionSubgroup (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) : inertiaSubgroup F v ≤ decompositionSubgroup F v

theorem AbsoluteValue.inertiaSubgroup_eq_decompositionSubgroup_of_not_isNonarchimedean (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (h : ¬IsNonarchimedean ⇑v) : inertiaSubgroup F v = decompositionSubgroup F v

theorem AbsoluteValue.apply_le_one_of_mem_inertiaSubgroup {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) {σ : Gal(K/F)} (h : σ ∈ inertiaSubgroup F v) {x : K} (hx : v x ≤ 1) : v (σ x) ≤ 1

theorem AbsoluteValue.apply_le_one_iff_of_mem_inertiaSubgroup {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) {σ : Gal(K/F)} (h : σ ∈ inertiaSubgroup F v) {x : K} : v (σ x) ≤ 1 ↔ v x ≤ 1

theorem AbsoluteValue.apply_sub_lt_one_of_mem_inertiaSubgroup_of_isNonarchimedean {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) {σ : Gal(K/F)} (h : σ ∈ inertiaSubgroup F v) (h2 : IsNonarchimedean ⇑v) {x : K} (hx : v x ≤ 1) : v (σ x - x) < 1

theorem AbsoluteValue.inertiaSubgroup_eq_of_isNonarchimedean (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (h : IsNonarchimedean ⇑v) : inertiaSubgroup F v = Subgroup.map (ValuationSubring.decompositionSubgroup F (v.toValuation h).valuationSubring).subtype (ValuationSubring.inertiaSubgroup F (v.toValuation h).valuationSubring)

Our definition is the same as ValuationSubring.inertiaSubgroup for finite places.

Assertion that a place is unramified

theorem AbsoluteValue.decompositionSubgroup_eq_comap (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : decompositionSubgroup K v = Subgroup.comap (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (decompositionSubgroup F v)

If L / K / F is an extension tower with L / F Galois, v is a place of L, then Dᵥ(L/K) = Dᵥ(L/F) ⊓ Gal(L/K).

theorem AbsoluteValue.map_decompositionSubgroup_le (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : Subgroup.map (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (decompositionSubgroup K v) ≤ decompositionSubgroup F v

If L / K / F is an extension tower with L / F Galois, v is a place of L, then Iᵥ(L/K) ≤ Iᵥ(L/F).

theorem AbsoluteValue.inertiaSubgroup_eq_comap (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : inertiaSubgroup K v = Subgroup.comap (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (inertiaSubgroup F v)

If L / K / F is an extension tower with L / F Galois, v is a place of L, then Iᵥ(L/K) = Iᵥ(L/F) ⊓ Gal(L/K).

theorem AbsoluteValue.map_inertiaSubgroup_le (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : Subgroup.map (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (inertiaSubgroup K v) ≤ inertiaSubgroup F v

If L / K / F is an extension tower with L / F Galois, v is a place of L, then Iᵥ(L/K) ≤ Iᵥ(L/F).

def AbsoluteValue.IsUnramifiedOfIsScalarTower (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : Prop

If L / K / F is an extension tower with L / F Galois, v is a place of L, then v is called unramified in L / K, if Iᵥ(L/F) ≤ Gal(L/K), or equivalently Iᵥ(L/K) = Iᵥ(L/F).

Equations

• AbsoluteValue.IsUnramifiedOfIsScalarTower F K v = (AbsoluteValue.inertiaSubgroup F v ≤ (IntermediateField.restrictRestrictAlgEquivMapHom F L K L).range)

theorem AbsoluteValue.isUnramifiedOfIsScalarTower_iff_map_inertiaSubgroup_eq (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : IsUnramifiedOfIsScalarTower F K v ↔ Subgroup.map (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (inertiaSubgroup K v) = inertiaSubgroup F v