Ramification of infinite places of a number field #

This file studies the ramification of infinite places of a number field.

Main Definitions and Results #

NumberField.InfinitePlace.comap: the restriction of an infinite place along an embedding.
NumberField.InfinitePlace.orbitRelEquiv: the equiv between the orbits of infinite places under the action of the galois group and the infinite places of the base field.
NumberField.InfinitePlace.IsUnramified: an infinite place is unramified in a field extension if the restriction has the same multiplicity.
NumberField.InfinitePlace.not_isUnramified_iff: an infinite place is not unramified (i.e., is ramified) iff it is a complex place above a real place.
NumberField.InfinitePlace.IsUnramifiedIn: an infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.
IsUnramifiedAtInfinitePlaces: a field extension is unramified at infinite places if every infinite place is unramified.

Tags #

number field, infinite places, ramification

def NumberField.InfinitePlace.comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (w : InfinitePlace K) (f : k →+* K) :

InfinitePlace k

The restriction of an infinite place along an embedding.

Equations

w.comap f = ⟨(↑w).comp ⋯, ⋯⟩

Instances For

source

@[simp]

theorem NumberField.InfinitePlace.comap_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] (φ : K →+* ℂ) (f : k →+* K) :

(mk φ).comap f = mk (φ.comp f)

source

theorem NumberField.InfinitePlace.comap_id {K : Type u_2} [Field K] (w : InfinitePlace K) :

w.comap (RingHom.id K) = w

source

theorem NumberField.InfinitePlace.comap_comp {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] (w : InfinitePlace K) (f : F →+* K) (g : k →+* F) :

w.comap (f.comp g) = (w.comap f).comap g

source

@[simp]

theorem NumberField.InfinitePlace.comap_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] (w : InfinitePlace K) (f : k →+* K) (x : k) :

(w.comap f) x = w (f x)

source

theorem NumberField.InfinitePlace.comp_of_comap_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] {v : InfinitePlace k} {w : InfinitePlace K} {f : k →+* K} (h : w.comap f = v) (x : k) :

w (f x) = v x

source

theorem NumberField.InfinitePlace.comap_mk_lift {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) :

(mk (ComplexEmbedding.lift K φ)).comap (algebraMap k K) = mk φ

source

theorem NumberField.InfinitePlace.IsReal.comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) {w : InfinitePlace K} (hφ : w.IsReal) :

(w.comap f).IsReal

source

theorem NumberField.InfinitePlace.isReal_comap_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k ≃+* K) {w : InfinitePlace K} :

(w.comap ↑f).IsReal ↔ w.IsReal

source

theorem NumberField.InfinitePlace.comap_surjective {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] :

Function.Surjective fun (x : InfinitePlace K) => x.comap (algebraMap k K)

source

theorem NumberField.InfinitePlace.mult_comap_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) (w : InfinitePlace K) :

(w.comap f).mult ≤ w.mult

source

theorem NumberField.InfinitePlace.card_mono (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField k] [NumberField K] :

Fintype.card (InfinitePlace k) ≤ Fintype.card (InfinitePlace K)

source

instance NumberField.InfinitePlace.instMulActionAlgEquiv {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] :

MulAction (K ≃ₐ[k] K) (InfinitePlace K)

The action of the galois group on infinite places.

Equations

NumberField.InfinitePlace.instMulActionAlgEquiv = { smul := fun (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) => w.comap ↑σ.symm, one_smul := ⋯, mul_smul := ⋯ }

source

@[simp]

theorem NumberField.InfinitePlace.instMulActionAlgEquiv_smul_coe_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) (a✝ : K) :

↑(SMul.smul σ w) a✝ = ↑w (σ.symm a✝)

source

theorem NumberField.InfinitePlace.smul_eq_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) :

σ • w = w.comap ↑σ.symm

source

@[simp]

theorem NumberField.InfinitePlace.smul_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) (x : K) :

(σ • w) x = w (σ.symm x)

source

@[simp]

theorem NumberField.InfinitePlace.smul_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (φ : K →+* ℂ) :

σ • mk φ = mk (φ.comp ↑σ.symm)

source

theorem NumberField.InfinitePlace.comap_smul {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) {f : F →+* K} :

(σ • w).comap f = w.comap ((↑σ.symm).comp f)

source

theorem NumberField.InfinitePlace.isReal_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} :

(σ • w).IsReal ↔ w.IsReal

source

theorem NumberField.InfinitePlace.isComplex_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} :

(σ • w).IsComplex ↔ w.IsComplex

source

theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (φ ψ : K →+* ℂ) (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) :

∃ (σ : K ≃ₐ[k] K), φ.comp ↑σ.symm = ψ

source

theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w w' : InfinitePlace K} (h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) :

∃ (σ : K ≃ₐ[k] K), σ • w = w'

source

theorem NumberField.InfinitePlace.mem_orbit_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w w' : InfinitePlace K} :

w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

source

noncomputable def NumberField.InfinitePlace.orbitRelEquiv {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] :

Quotient (MulAction.orbitRel (K ≃ₐ[k] K) (InfinitePlace K)) ≃ InfinitePlace k

The orbits of infinite places under the action of the galois group are indexed by the infinite places of the base field.

Equations

NumberField.InfinitePlace.orbitRelEquiv = Equiv.ofBijective (Quotient.lift (fun (x : NumberField.InfinitePlace K) => x.comap (algebraMap k K)) ⋯) ⋯

Instances For

source

theorem NumberField.InfinitePlace.orbitRelEquiv_apply_mk'' {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (w : InfinitePlace K) :

orbitRelEquiv (Quotient.mk'' w) = w.comap (algebraMap k K)

source

def NumberField.InfinitePlace.IsUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] (w : InfinitePlace K) :

Prop

An infinite place is unramified in a field extension if the restriction has the same multiplicity.

Equations

NumberField.InfinitePlace.IsUnramified k w = ((w.comap (algebraMap k K)).mult = w.mult)

Instances For

source

@[reducible, inline]

abbrev NumberField.InfinitePlace.IsRamified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] (w : InfinitePlace K) :

Prop

An infinite place is ramified in a field extension if it is not unramified.

Equations

NumberField.InfinitePlace.IsRamified k w = ¬NumberField.InfinitePlace.IsUnramified k w

Instances For

source

theorem NumberField.InfinitePlace.isUnramified_self {K : Type u_2} [Field K] (w : InfinitePlace K) :

IsUnramified K w

source

theorem NumberField.InfinitePlace.IsUnramified.eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : IsUnramified k w) :

(w.comap (algebraMap k K)).mult = w.mult

source

theorem NumberField.InfinitePlace.isUnramified_iff_mult_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} :

IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult

source

theorem NumberField.InfinitePlace.IsUnramified.comap_algHom {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] [Algebra k K] [Algebra k F] {w : InfinitePlace F} (h : IsUnramified k w) (f : K →ₐ[k] F) :

IsUnramified k (w.comap ↑f)

source

theorem NumberField.InfinitePlace.IsUnramified.of_restrictScalars {k : Type u_1} [Field k] (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] {w : InfinitePlace F} (h : IsUnramified k w) :

IsUnramified K w

source

theorem NumberField.InfinitePlace.IsUnramified.comap {k : Type u_1} [Field k] (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] {w : InfinitePlace F} (h : IsUnramified k w) :

IsUnramified k (w.comap (algebraMap K F))

source

theorem NumberField.InfinitePlace.not_isUnramified_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} :

¬IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal

An infinite place is not unramified (ie. ramified) iff it is a complex place above a real place.

source

theorem NumberField.InfinitePlace.isUnramified_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} :

IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex

source

theorem NumberField.InfinitePlace.isRamified_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} :

IsRamified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal

source

theorem NumberField.InfinitePlace.IsRamified.ne_conjugate {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w₁ w₂ : InfinitePlace K} (h : IsRamified k w₂) :

w₁.embedding ≠ ComplexEmbedding.conjugate w₂.embedding

source

theorem NumberField.InfinitePlace.IsReal.isUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : w.IsReal) :

IsUnramified k w

source

theorem NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* ℂ} (h : IsConj φ σ) :

InfinitePlace.IsUnramified k (InfinitePlace.mk φ) ↔ σ = 1

source

theorem NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {φ : K →+* ℂ} :

IsUnramified k (mk φ) ↔ ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1

source

theorem NumberField.InfinitePlace.mem_stabilizer_mk_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (φ : K →+* ℂ) (σ : K ≃ₐ[k] K) :

σ ∈ MulAction.stabilizer (K ≃ₐ[k] K) (mk φ) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

source

theorem NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : IsUnramified k w) :

MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥

source

theorem NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* ℂ} (h : IsConj φ σ) :

↑(MulAction.stabilizer (K ≃ₐ[k] K) (InfinitePlace.mk φ)) = {1, σ}

source

theorem NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] (w : InfinitePlace K) :

Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1 ∨ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2

source

theorem NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] :

IsUnramified k w ↔ MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥

source

theorem NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] :

IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1

source

theorem NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] :

¬IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2

source

theorem NumberField.InfinitePlace.card_stabilizer {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] :

Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = if IsUnramified k w then 1 else 2

source

theorem NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] (hw : ¬IsUnramified k w) :

Even (Nat.card (K ≃ₐ[k] K))

source

theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] [FiniteDimensional k K] (hw : ¬IsUnramified k w) :

Even (Fintype.card (K ≃ₐ[k] K))

source

theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] (hw : ¬IsUnramified k w) :

Even (Module.finrank k K)

source

theorem NumberField.InfinitePlace.isUnramified_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} :

IsUnramified k (σ • w) ↔ IsUnramified k w

source

def NumberField.InfinitePlace.IsUnramifiedIn {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra k K] (w : InfinitePlace k) :

Prop

A infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.

Equations

NumberField.InfinitePlace.IsUnramifiedIn K w = ∀ (v : NumberField.InfinitePlace K), v.comap (algebraMap k K) = w → NumberField.InfinitePlace.IsUnramified k v

Instances For

source

theorem NumberField.InfinitePlace.isUnramifiedIn_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : InfinitePlace K} :

IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

source

theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] [FiniteDimensional k K] {w : InfinitePlace k} (hw : ¬IsUnramifiedIn K w) :

Even (Fintype.card (K ≃ₐ[k] K))

source

theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramifiedIn {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : InfinitePlace k} (hw : ¬IsUnramifiedIn K w) :

Even (Module.finrank k K)

source

theorem NumberField.InfinitePlace.card_isUnramified (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField K] [NumberField k] [IsGalois k K] :

{w : InfinitePlace K | IsUnramified k w}.card = {w : InfinitePlace k | IsUnramifiedIn K w}.card * Module.finrank k K

source

theorem NumberField.InfinitePlace.card_isUnramified_compl (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField K] [NumberField k] [IsGalois k K] :

{w : InfinitePlace K | IsUnramified k w}ᶜ.card = {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)

source

theorem NumberField.InfinitePlace.card_eq_card_isUnramifiedIn (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField K] [NumberField k] [IsGalois k K] :

Fintype.card (InfinitePlace K) = {w : InfinitePlace k | IsUnramifiedIn K w}.card * Module.finrank k K + {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)

source

class IsUnramifiedAtInfinitePlaces (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] :

Prop

A field extension is unramified at infinite places if every infinite place is unramified.

isUnramified (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.IsUnramified k w

Instances

source

instance IsUnramifiedAtInfinitePlaces.id (K : Type u_2) [Field K] :

IsUnramifiedAtInfinitePlaces K K

source

theorem IsUnramifiedAtInfinitePlaces.trans (k : Type u_1) [Field k] (K : Type u_2) [Field K] (F : Type u_3) [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] [h₁ : IsUnramifiedAtInfinitePlaces k K] [h₂ : IsUnramifiedAtInfinitePlaces K F] :

IsUnramifiedAtInfinitePlaces k F

source

theorem IsUnramifiedAtInfinitePlaces.top (k : Type u_1) [Field k] (K : Type u_2) [Field K] (F : Type u_3) [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] [h : IsUnramifiedAtInfinitePlaces k F] :

IsUnramifiedAtInfinitePlaces K F

source

theorem IsUnramifiedAtInfinitePlaces.bot (k : Type u_1) [Field k] (K : Type u_2) [Field K] (F : Type u_3) [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] [h₁ : IsUnramifiedAtInfinitePlaces k F] [Algebra.IsAlgebraic K F] :

IsUnramifiedAtInfinitePlaces k K

source

theorem NumberField.InfinitePlace.isUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsUnramifiedAtInfinitePlaces k K] (w : InfinitePlace K) :

IsUnramified k w

source

theorem NumberField.InfinitePlace.isUnramifiedIn {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra k K] [IsUnramifiedAtInfinitePlaces k K] (w : InfinitePlace k) :

IsUnramifiedIn K w

source

theorem IsUnramifiedAtInfinitePlaces_of_odd_card_aut {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] [FiniteDimensional k K] (h : Odd (Fintype.card (K ≃ₐ[k] K))) :

IsUnramifiedAtInfinitePlaces k K

source

theorem IsUnramifiedAtInfinitePlaces_of_odd_finrank {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (h : Odd (Module.finrank k K)) :

IsUnramifiedAtInfinitePlaces k K

source

theorem IsUnramifiedAtInfinitePlaces.card_infinitePlace (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] :

Fintype.card (NumberField.InfinitePlace K) = Fintype.card (NumberField.InfinitePlace k) * Module.finrank k K

Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Ramification of infinite places of a number field #

Main Definitions and Results #

Tags #