Documentation

@[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)

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

w.comap (RingHom.id K) = w

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

@[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)

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

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 φ

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

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

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

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)

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

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

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)

🔸 coverage

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

@[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✝)

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

@[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)

@[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)

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)

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

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

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 = ψ

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'

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)

🔸 coverage

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

Instances For

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)

🔹 coverage

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

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

Equations

Instances For

🔹 coverage

@[reducible, inline]

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

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

Equations

Instances For

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

IsUnramified K w

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

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

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)

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

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))

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.

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

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

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

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

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

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)

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)

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

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)

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 φ

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.

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

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)

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 φ

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.

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

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

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

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 φ σ

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 = ⊥

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, σ}

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

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 = ⊥

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

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

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

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 φ σ

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

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))

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))

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)

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

🔹 coverage

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

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

Equations

Instances For

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

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))

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)

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

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)

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)

🔶 coverage

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

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

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

IsUnramifiedAtInfinitePlaces K K

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

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

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

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

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

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

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

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

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

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

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.

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.