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.coe_mk_comp {k : Type u_1} [Field k] {K : Type u_2} [Field K] {ψ : K →+* ℂ} {f : k →+* K} (h : Function.Injective ⇑f) :

↑(mk (ψ.comp f)) = (↑(mk ψ)).comp h

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.IsComplex.of_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) {w : InfinitePlace K} (hf : (w.comap f).IsComplex) :

w.IsComplex

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.comap_embedding_of_isReal {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) {w : InfinitePlace K} (h : (w.comap f).IsReal) :

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

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

@[implicit_reducible]

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

MulAction Gal(K/k) (InfinitePlace K)

The action of the Galois group on infinite places.

Equations

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

source

@[simp]

theorem NumberField.InfinitePlace.smul_coe_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : Gal(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] (σ : Gal(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] (σ : Gal(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] (σ : Gal(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] (σ : Gal(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] {σ : Gal(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] {σ : Gal(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)) :

∃ (σ : Gal(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)) :

∃ (σ : Gal(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 Gal(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 Gal(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 (i.e. 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.isComplex {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : IsRamified k w) :

w.IsComplex

source

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

(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.IsRamified.comap_embedding {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : IsRamified k w) :

(w.comap (algebraMap k K)).embedding = w.embedding.comp (algebraMap k K)

source

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

(w.comap (algebraMap k K)).embedding = (ComplexEmbedding.conjugate w.embedding).comp (algebraMap k K)

source

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

ComplexEmbedding.IsMixed k w.embedding

source

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

ComplexEmbedding.IsMixed k (ComplexEmbedding.conjugate w.embedding)

source

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

IsRamified k (mk φ) ↔ ComplexEmbedding.IsMixed k φ

source

theorem NumberField.ComplexEmbedding.IsMixed.mk_isRamified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {φ : K →+* ℂ} :

IsMixed k φ → InfinitePlace.IsRamified k (InfinitePlace.mk φ)

Alias of the reverse direction of NumberField.InfinitePlace.isRamified_mk_iff_isMixed.

source

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

ComplexEmbedding.IsUnmixed k w.embedding

source

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

ComplexEmbedding.IsUnmixed k (ComplexEmbedding.conjugate w.embedding)

source

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

IsUnramified k (mk φ) ↔ ComplexEmbedding.IsUnmixed k φ

source

theorem NumberField.ComplexEmbedding.IsUnmixed.mk_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {φ : K →+* ℂ} :

IsUnmixed k φ → InfinitePlace.IsUnramified k (InfinitePlace.mk φ)

Alias of the reverse direction of NumberField.InfinitePlace.isUnramified_mk_iff_isUnmixed.

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] {σ : Gal(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 φ) ↔ ∀ (σ : Gal(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 →+* ℂ) (σ : Gal(K/k)) :

σ ∈ MulAction.stabilizer Gal(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 Gal(K/k) w = ⊥

source

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

↑(MulAction.stabilizer Gal(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 Gal(K/k) w) = 1 ∨ Nat.card ↥(MulAction.stabilizer Gal(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 Gal(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 Gal(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 Gal(K/k) w) = 2

source

theorem NumberField.InfinitePlace.isRamified_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] :

IsRamified k w ↔ Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = 2

source

theorem NumberField.InfinitePlace.exists_isConj_of_isRamified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {φ : K →+* ℂ} (h : IsRamified k (mk φ)) :

∃ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ

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 Gal(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 Gal(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] (hw : ¬IsUnramified k w) :

Even (Nat.card Gal(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] {σ : Gal(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

An 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] {w : InfinitePlace k} (hw : ¬IsUnramifiedIn K w) :

Even (Nat.card Gal(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] (h : Odd (Nat.card Gal(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

source

instance NumberField.InfinitePlace.LiesOver.instLiesOverRealValAbsoluteValueExistsRingHomComplexEqPlaceMkOfLiesOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {φ : K →+* ℂ} {ψ : L →+* ℂ} [ComplexEmbedding.LiesOver ψ φ] :

(↑(mk ψ)).LiesOver ↑(mk φ)

source

theorem NumberField.InfinitePlace.LiesOver.comap_eq {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [(↑w).LiesOver ↑v] :

w.comap (algebraMap K L) = v

source

theorem NumberField.InfinitePlace.LiesOver.mk_embedding_comp {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [(↑w).LiesOver ↑v] :

mk (w.embedding.comp (algebraMap K L)) = v

source

theorem NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [(↑w).LiesOver ↑v] :

w.embedding.comp (algebraMap K L) = v.embedding ∨ (ComplexEmbedding.conjugate w.embedding).comp (algebraMap K L) = v.embedding

If w : InfinitePlace L lies above v : InfinitePlace K, then either w.embedding extends v.embedding as complex embeddings, or conjugate w.embedding extends v.embedding.

source

theorem NumberField.InfinitePlace.LiesOver.isComplex_of_isComplex_under {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) {v : InfinitePlace K} [(↑w).LiesOver ↑v] (hv : v.IsComplex) :

w.IsComplex

If w : InfinitePlace L lies above v : InfinitePlace K and v is complex, then so is w.

source

theorem NumberField.InfinitePlace.LiesOver.isReal_of_isReal_over {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) {v : InfinitePlace K} [(↑w).LiesOver ↑v] (hw : w.IsReal) :

v.IsReal

If w : InfinitePlace L lies above v : InfinitePlace K and w is real, then so is v.

source

theorem NumberField.InfinitePlace.IsRamified.liesOver_isReal_under {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [(↑w).LiesOver ↑v] (hw : IsRamified K w) :

v.IsReal

source

theorem NumberField.InfinitePlace.IsUnramified.liesOver_isReal_over {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (w : InfinitePlace L) (v : InfinitePlace K) [(↑w).LiesOver ↑v] (hw : IsUnramified K w) (hv : v.IsReal) :

w.IsReal

source

def NumberField.InfinitePlace.placesOver {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

Set (InfinitePlace L)

The set of infinite places of L that lie above a given infinite place of K.

Equations

NumberField.InfinitePlace.placesOver L v = {w : NumberField.InfinitePlace L | (↑w).LiesOver ↑v}

Instances For

source

def NumberField.InfinitePlace.unramifiedPlacesOver {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

Set (InfinitePlace L)

The set of infinite places of L that are unramified over a given infinite place of K.

Equations

NumberField.InfinitePlace.unramifiedPlacesOver L v = {w : NumberField.InfinitePlace L | (↑w).LiesOver ↑v ∧ NumberField.InfinitePlace.IsUnramified K w}

Instances For

source

def NumberField.InfinitePlace.ramifiedPlacesOver {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

Set (InfinitePlace L)

The set of infinite places of L that are ramified over a given infinite place of K.

Equations

NumberField.InfinitePlace.ramifiedPlacesOver L v = {w : NumberField.InfinitePlace L | (↑w).LiesOver ↑v ∧ NumberField.InfinitePlace.IsRamified K w}

Instances For

source

theorem NumberField.InfinitePlace.mk_mem_unramifiedPlacesOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {φ : L →+* ℂ} (h : φ ∈ ComplexEmbedding.unmixedEmbeddingsOver L v.embedding) :

mk φ ∈ unramifiedPlacesOver L v

source

theorem NumberField.InfinitePlace.liesOver_embedding_of_mem_ramifiedPlacesOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} (hw : w ∈ ramifiedPlacesOver L v) :

ComplexEmbedding.LiesOver w.embedding v.embedding

source

theorem NumberField.InfinitePlace.liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} (hw : w ∈ ramifiedPlacesOver L v) :

ComplexEmbedding.LiesOver (ComplexEmbedding.conjugate w.embedding) v.embedding

source

theorem NumberField.InfinitePlace.mk_mem_ramifiedPlacesOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {φ : L →+* ℂ} (h : φ ∈ ComplexEmbedding.mixedEmbeddingsOver L v.embedding) :

mk φ ∈ ramifiedPlacesOver L v

source

theorem NumberField.InfinitePlace.embedding_mem_mixedEmbeddingsOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} (w : InfinitePlace L) (hw : w ∈ ramifiedPlacesOver L v) :

w.embedding ∈ ComplexEmbedding.mixedEmbeddingsOver L v.embedding

source

theorem NumberField.InfinitePlace.conjugate_embedding_mem_mixedEmbeddingsOver {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} (w : InfinitePlace L) (hw : w ∈ ramifiedPlacesOver L v) :

ComplexEmbedding.conjugate w.embedding ∈ ComplexEmbedding.mixedEmbeddingsOver L v.embedding

source

theorem NumberField.InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

Disjoint (ramifiedPlacesOver L v) (unramifiedPlacesOver L v)

source

theorem NumberField.InfinitePlace.union_ramifiedPlacesOver_unramifiedPlacesOver {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

ramifiedPlacesOver L v ∪ unramifiedPlacesOver L v = placesOver L v

source

theorem NumberField.InfinitePlace.bijOn_sumElim_conjugate {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

Set.BijOn (Sum.elim embedding (ComplexEmbedding.conjugate ∘ embedding)) (Set.sumEquiv.symm (ramifiedPlacesOver L v, ramifiedPlacesOver L v)) (ComplexEmbedding.mixedEmbeddingsOver L v.embedding)

source

theorem NumberField.InfinitePlace.ramifiedPlacesOver_ncard {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

2 * (ramifiedPlacesOver L v).ncard = (ComplexEmbedding.mixedEmbeddingsOver L v.embedding).ncard

The number of mixed embeddings over an infinite place is twice the number of ramified places over the place.

source

theorem NumberField.InfinitePlace.unramifiedPlacesOver_ncard {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) :

(unramifiedPlacesOver L v).ncard = (ComplexEmbedding.unmixedEmbeddingsOver L v.embedding).ncard

The number of unramified places over an infinite place is equal to the number of unmixed embeddings over the place.

source

theorem NumberField.InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrank {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField K] [NumberField L] :

(unramifiedPlacesOver L v).ncard + 2 * (ramifiedPlacesOver L v).ncard = Module.finrank K L

The degree of L over K is equal to the number of unramified places over v plus twice the number of ramified places over v.

Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Ramification of infinite places of a number field #

Main Definitions and Results #

Tags #