Embeddings of number fields

This file defines the embeddings of a number field into an algebraic closed field.

Main Definitions and Results

• NumberField.Embeddings.range_eval_eq_rootSet_minpoly: let x ∈ K with K number field and let A be an algebraic closed field of char. 0, then the images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.
• NumberField.Embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.
• NumberField.InfinitePlace: the type of infinite places of a number field K.
• NumberField.InfinitePlace.mk_eq_iff: two complex embeddings define the same infinite place iff they are equal or complex conjugates.
• NumberField.InfinitePlace.prod_eq_abs_norm: the infinite part of the product formula, that is for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where the product is over the infinite place w and ‖·‖_w is the normalized absolute value for w.

Tags

number field, embeddings, places, infinite places

noncomputable instance NumberField.Embeddings.instFintypeRingHomToNonAssocSemiringToSemiringToDivisionSemiringToSemifieldToNonAssocSemiringToSemiringToDivisionSemiringToSemifield (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] : Fintype (K →+* A)

There are finitely many embeddings of a number field.

Equations

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

theorem NumberField.Embeddings.card (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] [IsAlgClosed A] : Fintype.card (K →+* A) = FiniteDimensional.finrank ℚ K

The number of embeddings of a number field is equal to its finrank.

instance NumberField.Embeddings.instNonemptyRingHomToNonAssocSemiringToSemiringToDivisionSemiringToSemifieldToNonAssocSemiringToSemiringToDivisionSemiringToSemifield (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] [IsAlgClosed A] : Nonempty (K →+* A)

Equations

• ⋯ = ⋯

theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly (K : Type u_1) (A : Type u_2) [Field K] [NumberField K] [Field A] [Algebra ℚ A] [IsAlgClosed A] (x : K) : (Set.range fun (φ : K →+* A) => φ x) = Polynomial.rootSet (minpoly ℚ x) A

Let A be an algebraically closed field and let x ∈ K, with K a number field. The images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.

theorem NumberField.Embeddings.coeff_bdd_of_norm_le {K : Type u_1} [Field K] [NumberField K] {A : Type u_2} [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {B : ℝ} {x : K} (h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B) (i : ℕ) : ‖Polynomial.coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ FiniteDimensional.finrank ℚ K * ↑(Nat.choose (FiniteDimensional.finrank ℚ K) (FiniteDimensional.finrank ℚ K / 2))

theorem NumberField.Embeddings.finite_of_norm_le (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] (B : ℝ) : Set.Finite {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

theorem NumberField.Embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ (φ : K →+* A), ‖φ x‖ = 1) : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

def NumberField.place {K : Type u_1} [Field K] {A : Type u_2} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A) : AbsoluteValue K ℝ

An embedding into a normed division ring defines a place of K

Equations

• NumberField.place φ = AbsoluteValue.comp (IsAbsoluteValue.toAbsoluteValue norm) ⋯

@[simp]

theorem NumberField.place_apply {K : Type u_1} [Field K] {A : Type u_2} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A) (x : K) : (NumberField.place φ) x = ‖φ x‖

@[reducible]

def NumberField.ComplexEmbedding.conjugate {K : Type u_1} [Field K] (φ : K →+* ℂ) : K →+* ℂ

The conjugate of a complex embedding as a complex embedding.

Equations

• NumberField.ComplexEmbedding.conjugate φ = star φ

@[simp]

theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [Field K] (φ : K →+* ℂ) (x : K) : (NumberField.ComplexEmbedding.conjugate φ) x = (starRingEnd ℂ) (φ x)

theorem NumberField.ComplexEmbedding.place_conjugate {K : Type u_1} [Field K] (φ : K →+* ℂ) : NumberField.place (NumberField.ComplexEmbedding.conjugate φ) = NumberField.place φ

@[reducible]

def NumberField.ComplexEmbedding.IsReal {K : Type u_1} [Field K] (φ : K →+* ℂ) : Prop

An embedding into ℂ is real if it is fixed by complex conjugation.

Equations

• NumberField.ComplexEmbedding.IsReal φ = IsSelfAdjoint φ

theorem NumberField.ComplexEmbedding.isReal_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : NumberField.ComplexEmbedding.IsReal φ ↔ NumberField.ComplexEmbedding.conjugate φ = φ

theorem NumberField.ComplexEmbedding.isReal_conjugate_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : NumberField.ComplexEmbedding.IsReal (NumberField.ComplexEmbedding.conjugate φ) ↔ NumberField.ComplexEmbedding.IsReal φ

def NumberField.ComplexEmbedding.IsReal.embedding {K : Type u_1} [Field K] {φ : K →+* ℂ} (hφ : NumberField.ComplexEmbedding.IsReal φ) : K →+* ℝ

A real embedding as a ring homomorphism from K to ℝ .

Equations

• NumberField.ComplexEmbedding.IsReal.embedding hφ = { toMonoidHom := { toOneHom := { toFun := fun (x : K) => (φ x).re, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply {K : Type u_1} [Field K] {φ : K →+* ℂ} (hφ : NumberField.ComplexEmbedding.IsReal φ) (x : K) : ↑((NumberField.ComplexEmbedding.IsReal.embedding hφ) x) = φ x

theorem NumberField.ComplexEmbedding.IsReal.comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] (f : k →+* K) {φ : K →+* ℂ} (hφ : NumberField.ComplexEmbedding.IsReal φ) : NumberField.ComplexEmbedding.IsReal (RingHom.comp φ f)

theorem NumberField.ComplexEmbedding.isReal_comp_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] {f : k ≃+* K} {φ : K →+* ℂ} : NumberField.ComplexEmbedding.IsReal (RingHom.comp φ ↑f) ↔ NumberField.ComplexEmbedding.IsReal φ

theorem NumberField.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 →+* ℂ) (ψ : K →+* ℂ) (h : RingHom.comp φ (algebraMap k K) = RingHom.comp ψ (algebraMap k K)) : ∃ (σ : K ≃ₐ[k] K), RingHom.comp φ ↑(AlgEquiv.symm σ) = ψ

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

IsConj φ σ states that σ : K ≃ₐ[k] K is the conjugation under the embedding φ : K →+* ℂ.

Equations

• NumberField.ComplexEmbedding.IsConj φ σ = (NumberField.ComplexEmbedding.conjugate φ = RingHom.comp φ ↑σ)

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

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

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

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

theorem NumberField.ComplexEmbedding.isConj_one_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} : NumberField.ComplexEmbedding.IsConj φ 1 ↔ NumberField.ComplexEmbedding.IsReal φ

theorem NumberField.ComplexEmbedding.IsReal.isConjGal_one {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} : NumberField.ComplexEmbedding.IsReal φ → NumberField.ComplexEmbedding.IsConj φ 1

Alias of the reverse direction of NumberField.ComplexEmbedding.isConj_one_iff.

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

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

def NumberField.InfinitePlace (K : Type u_2) [Field K] : Type u_2

An infinite place of a number field K is a place associated to a complex embedding.

Equations

• NumberField.InfinitePlace K = { w : AbsoluteValue K ℝ // ∃ (φ : K →+* ℂ), NumberField.place φ = w }

instance instNonemptyInfinitePlace (K : Type u_2) [Field K] [NumberField K] : Nonempty (NumberField.InfinitePlace K)

Equations

• ⋯ = ⋯

noncomputable def NumberField.InfinitePlace.mk {K : Type u_2} [Field K] (φ : K →+* ℂ) : NumberField.InfinitePlace K

Return the infinite place defined by a complex embedding φ.

Equations

• NumberField.InfinitePlace.mk φ = { val := NumberField.place φ, property := ⋯ }

instance NumberField.InfinitePlace.instFunLikeInfinitePlaceReal {K : Type u_4} [Field K] : FunLike (NumberField.InfinitePlace K) K ℝ

Equations

• NumberField.InfinitePlace.instFunLikeInfinitePlaceReal = { coe := fun (w : NumberField.InfinitePlace K) (x : K) => ↑w x, coe_injective' := ⋯ }

instance NumberField.InfinitePlace.instMonoidWithZeroHomClassInfinitePlaceRealToMulZeroOneClassToNonAssocSemiringToSemiringToDivisionSemiringToSemifieldToMulZeroOneClassToNonAssocSemiringSemiringInstFunLikeInfinitePlaceReal {K : Type u_2} [Field K] : MonoidWithZeroHomClass (NumberField.InfinitePlace K) K ℝ

Equations

• ⋯ = ⋯

instance NumberField.InfinitePlace.instNonnegHomClassInfinitePlaceRealInstZeroRealInstLERealInstFunLikeInfinitePlaceReal {K : Type u_2} [Field K] : NonnegHomClass (NumberField.InfinitePlace K) K ℝ

Equations

• ⋯ = ⋯

@[simp]

theorem NumberField.InfinitePlace.apply {K : Type u_2} [Field K] (φ : K →+* ℂ) (x : K) : (NumberField.InfinitePlace.mk φ) x = Complex.abs (φ x)

noncomputable def NumberField.InfinitePlace.embedding {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : K →+* ℂ

For an infinite place w, return an embedding φ such that w = infinite_place φ .

Equations

• NumberField.InfinitePlace.embedding w = Exists.choose ⋯

@[simp]

theorem NumberField.InfinitePlace.mk_embedding {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.mk (NumberField.InfinitePlace.embedding w) = w

@[simp]

theorem NumberField.InfinitePlace.mk_conjugate_eq {K : Type u_2} [Field K] (φ : K →+* ℂ) : NumberField.InfinitePlace.mk (NumberField.ComplexEmbedding.conjugate φ) = NumberField.InfinitePlace.mk φ

theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) (x : K) : ‖(NumberField.InfinitePlace.embedding w) x‖ = w x

theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_2} [Field K] (x : K) (r : ℝ) : (∀ (w : NumberField.InfinitePlace K), w x = r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ = r

theorem NumberField.InfinitePlace.le_iff_le {K : Type u_2} [Field K] (x : K) (r : ℝ) : (∀ (w : NumberField.InfinitePlace K), w x ≤ r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

theorem NumberField.InfinitePlace.pos_iff {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0

@[simp]

theorem NumberField.InfinitePlace.mk_eq_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} {ψ : K →+* ℂ} : NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk ψ ↔ φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ

def NumberField.InfinitePlace.IsReal {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : Prop

An infinite place is real if it is defined by a real embedding.

Equations

• NumberField.InfinitePlace.IsReal w = ∃ (φ : K →+* ℂ), NumberField.ComplexEmbedding.IsReal φ ∧ NumberField.InfinitePlace.mk φ = w

def NumberField.InfinitePlace.IsComplex {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : Prop

An infinite place is complex if it is defined by a complex (ie. not real) embedding.

Equations

• NumberField.InfinitePlace.IsComplex w = ∃ (φ : K →+* ℂ), ¬NumberField.ComplexEmbedding.IsReal φ ∧ NumberField.InfinitePlace.mk φ = w

theorem NumberField.InfinitePlace.embedding_mk_eq {K : Type u_2} [Field K] (φ : K →+* ℂ) : NumberField.InfinitePlace.embedding (NumberField.InfinitePlace.mk φ) = φ ∨ NumberField.InfinitePlace.embedding (NumberField.InfinitePlace.mk φ) = NumberField.ComplexEmbedding.conjugate φ

@[simp]

theorem NumberField.InfinitePlace.embedding_mk_eq_of_isReal {K : Type u_2} [Field K] {φ : K →+* ℂ} (h : NumberField.ComplexEmbedding.IsReal φ) : NumberField.InfinitePlace.embedding (NumberField.InfinitePlace.mk φ) = φ

theorem NumberField.InfinitePlace.isReal_iff {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsReal w ↔ NumberField.ComplexEmbedding.IsReal (NumberField.InfinitePlace.embedding w)

theorem NumberField.InfinitePlace.isComplex_iff {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsComplex w ↔ ¬NumberField.ComplexEmbedding.IsReal (NumberField.InfinitePlace.embedding w)

@[simp]

theorem NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} (h : NumberField.InfinitePlace.IsReal w) : NumberField.ComplexEmbedding.conjugate (NumberField.InfinitePlace.embedding w) = NumberField.InfinitePlace.embedding w

@[simp]

theorem NumberField.InfinitePlace.not_isReal_iff_isComplex {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} : ¬NumberField.InfinitePlace.IsReal w ↔ NumberField.InfinitePlace.IsComplex w

@[simp]

theorem NumberField.InfinitePlace.not_isComplex_iff_isReal {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} : ¬NumberField.InfinitePlace.IsComplex w ↔ NumberField.InfinitePlace.IsReal w

theorem NumberField.InfinitePlace.isReal_or_isComplex {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.IsReal w ∨ NumberField.InfinitePlace.IsComplex w

theorem NumberField.InfinitePlace.ne_of_isReal_isComplex {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} {w' : NumberField.InfinitePlace K} (h : NumberField.InfinitePlace.IsReal w) (h' : NumberField.InfinitePlace.IsComplex w') : w ≠ w'

theorem NumberField.InfinitePlace.disjoint_isReal_isComplex (K : Type u_2) [Field K] : Disjoint {w : NumberField.InfinitePlace K | NumberField.InfinitePlace.IsReal w} {w : NumberField.InfinitePlace K | NumberField.InfinitePlace.IsComplex w}

noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} (hw : NumberField.InfinitePlace.IsReal w) : K →+* ℝ

The real embedding associated to a real infinite place.

Equations

• NumberField.InfinitePlace.embedding_of_isReal hw = NumberField.ComplexEmbedding.IsReal.embedding ⋯

@[simp]

theorem NumberField.InfinitePlace.embedding_of_isReal_apply {K : Type u_2} [Field K] {w : NumberField.InfinitePlace K} (hw : NumberField.InfinitePlace.IsReal w) (x : K) : ↑((NumberField.InfinitePlace.embedding_of_isReal hw) x) = (NumberField.InfinitePlace.embedding w) x

@[simp]

theorem NumberField.InfinitePlace.isReal_of_mk_isReal {K : Type u_2} [Field K] {φ : K →+* ℂ} (h : NumberField.InfinitePlace.IsReal (NumberField.InfinitePlace.mk φ)) : NumberField.ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isReal_mk_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} : NumberField.InfinitePlace.IsReal (NumberField.InfinitePlace.mk φ) ↔ NumberField.ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isComplex_mk_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} : NumberField.InfinitePlace.IsComplex (NumberField.InfinitePlace.mk φ) ↔ ¬NumberField.ComplexEmbedding.IsReal φ

@[simp]

theorem NumberField.InfinitePlace.not_isReal_of_mk_isComplex {K : Type u_2} [Field K] {φ : K →+* ℂ} (h : NumberField.InfinitePlace.IsComplex (NumberField.InfinitePlace.mk φ)) : ¬NumberField.ComplexEmbedding.IsReal φ

noncomputable def NumberField.InfinitePlace.mult {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : ℕ

The multiplicity of an infinite place, that is the number of distinct complex embeddings that define it, see card_filter_mk_eq.

Equations

• NumberField.InfinitePlace.mult w = if NumberField.InfinitePlace.IsReal w then 1 else 2

theorem NumberField.InfinitePlace.card_filter_mk_eq {K : Type u_2} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) : (Finset.filter (fun (φ : K →+* ℂ) => NumberField.InfinitePlace.mk φ = w) Finset.univ).card = NumberField.InfinitePlace.mult w

noncomputable instance NumberField.InfinitePlace.NumberField.InfinitePlace.fintype {K : Type u_2} [Field K] [NumberField K] : Fintype (NumberField.InfinitePlace K)

Equations

• NumberField.InfinitePlace.NumberField.InfinitePlace.fintype = Set.fintypeRange fun (φ : K →+* ℂ) => NumberField.place φ

theorem NumberField.InfinitePlace.sum_mult_eq {K : Type u_2} [Field K] [NumberField K] : (Finset.sum Finset.univ fun (w : NumberField.InfinitePlace K) => NumberField.InfinitePlace.mult w) = FiniteDimensional.finrank ℚ K

noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_2} [Field K] : { φ : K →+* ℂ // NumberField.ComplexEmbedding.IsReal φ } ≃ { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w }

The map from real embeddings to real infinite places as an equiv

Equations

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

noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_2} [Field K] : { φ : K →+* ℂ // ¬NumberField.ComplexEmbedding.IsReal φ } → { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }

The map from nonreal embeddings to complex infinite places

Equations

• NumberField.InfinitePlace.mkComplex = Subtype.map NumberField.InfinitePlace.mk ⋯

@[simp]

theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_2} [Field K] (φ : { φ : K →+* ℂ // NumberField.ComplexEmbedding.IsReal φ }) : ↑(NumberField.InfinitePlace.mkReal φ) = NumberField.InfinitePlace.mk ↑φ

@[simp]

theorem NumberField.InfinitePlace.mkComplex_coe {K : Type u_2} [Field K] (φ : { φ : K →+* ℂ // ¬NumberField.ComplexEmbedding.IsReal φ }) : ↑(NumberField.InfinitePlace.mkComplex φ) = NumberField.InfinitePlace.mk ↑φ

theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_2} [Field K] [NumberField K] (x : K) : (Finset.prod Finset.univ fun (w : NumberField.InfinitePlace K) => w x ^ NumberField.InfinitePlace.mult w) = ↑|(Algebra.norm ℚ) x|

The infinite part of the product formula : for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where ‖·‖_w is the normalized absolute value for w.

theorem NumberField.InfinitePlace.one_le_of_lt_one {K : Type u_2} [Field K] [NumberField K] {w : NumberField.InfinitePlace K} {a : ↥(NumberField.ringOfIntegers K)} (ha : a ≠ 0) (h : ∀ ⦃z : NumberField.InfinitePlace K⦄, z ≠ w → z ↑a < 1) : 1 ≤ w ↑a

theorem NumberField.is_primitive_element_of_infinitePlace_lt {K : Type u_2} [Field K] [NumberField K] {x : ↥(NumberField.ringOfIntegers K)} {w : NumberField.InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) (h₃ : NumberField.InfinitePlace.IsReal w ∨ |((NumberField.InfinitePlace.embedding w) ↑x).re| < 1) : ℚ⟮↑x⟯ = ⊤

theorem NumberField.adjoin_eq_top_of_infinitePlace_lt {K : Type u_2} [Field K] [NumberField K] {x : ↥(NumberField.ringOfIntegers K)} {w : NumberField.InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) (h₃ : NumberField.InfinitePlace.IsReal w ∨ |((NumberField.InfinitePlace.embedding w) ↑x).re| < 1) : Algebra.adjoin ℚ {↑x} = ⊤

@[inline, reducible]

noncomputable abbrev NumberField.InfinitePlace.NrRealPlaces (K : Type u_2) [Field K] [NumberField K] : ℕ

The number of infinite real places of the number field K.

Equations

• NumberField.InfinitePlace.NrRealPlaces K = Fintype.card { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsReal w }

@[inline, reducible]

noncomputable abbrev NumberField.InfinitePlace.NrComplexPlaces (K : Type u_2) [Field K] [NumberField K] : ℕ

The number of infinite complex places of the number field K.

Equations

• NumberField.InfinitePlace.NrComplexPlaces K = Fintype.card { w : NumberField.InfinitePlace K // NumberField.InfinitePlace.IsComplex w }

theorem NumberField.InfinitePlace.card_real_embeddings (K : Type u_2) [Field K] [NumberField K] : Fintype.card { φ : K →+* ℂ // NumberField.ComplexEmbedding.IsReal φ } = NumberField.InfinitePlace.NrRealPlaces K

theorem NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces (K : Type u_2) [Field K] [NumberField K] : Fintype.card (NumberField.InfinitePlace K) = NumberField.InfinitePlace.NrRealPlaces K + NumberField.InfinitePlace.NrComplexPlaces K

theorem NumberField.InfinitePlace.card_complex_embeddings (K : Type u_2) [Field K] [NumberField K] : Fintype.card { φ : K →+* ℂ // ¬NumberField.ComplexEmbedding.IsReal φ } = 2 * NumberField.InfinitePlace.NrComplexPlaces K

theorem NumberField.InfinitePlace.card_add_two_mul_card_eq_rank (K : Type u_2) [Field K] [NumberField K] : NumberField.InfinitePlace.NrRealPlaces K + 2 * NumberField.InfinitePlace.NrComplexPlaces K = FiniteDimensional.finrank ℚ K

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one {K : Type u_2} [Field K] [NumberField K] (h : FiniteDimensional.finrank ℚ K = 1) : NumberField.InfinitePlace.NrComplexPlaces K = 0

theorem NumberField.InfinitePlace.nrRealPlaces_eq_one_of_finrank_eq_one {K : Type u_2} [Field K] [NumberField K] (h : FiniteDimensional.finrank ℚ K = 1) : NumberField.InfinitePlace.NrRealPlaces K = 1

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

The restriction of an infinite place along an embedding.

Equations

• NumberField.InfinitePlace.comap w f = { val := AbsoluteValue.comp ↑w ⋯, property := ⋯ }

@[simp]

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

theorem NumberField.InfinitePlace.comap_id {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.comap w (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 : NumberField.InfinitePlace K) (f : F →+* K) (g : k →+* F) : NumberField.InfinitePlace.comap w (RingHom.comp f g) = NumberField.InfinitePlace.comap (NumberField.InfinitePlace.comap w f) g

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

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

theorem NumberField.InfinitePlace.comap_surjective {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (h : Algebra.IsAlgebraic k K) : Function.Surjective fun (x : NumberField.InfinitePlace K) => NumberField.InfinitePlace.comap x (algebraMap k K)

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

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 (NumberField.InfinitePlace k) ≤ Fintype.card (NumberField.InfinitePlace K)

@[simp]

theorem NumberField.InfinitePlace.instMulActionAlgEquivToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifieldInfinitePlaceToMonoidToDivInvMonoidAut_smul_coe_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) : ∀ (a : K), ↑(SMul.smul σ w) a = ↑w ((AlgEquiv.symm σ) a)

instance NumberField.InfinitePlace.instMulActionAlgEquivToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifieldInfinitePlaceToMonoidToDivInvMonoidAut {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] : MulAction (K ≃ₐ[k] K) (NumberField.InfinitePlace K)

The action of the galois group on infinite places.

Equations

• NumberField.InfinitePlace.instMulActionAlgEquivToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifieldInfinitePlaceToMonoidToDivInvMonoidAut = MulAction.mk ⋯ ⋯

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 : NumberField.InfinitePlace K) : σ • w = NumberField.InfinitePlace.comap w ↑(AlgEquiv.symm σ)

@[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 : NumberField.InfinitePlace K) (x : K) : (σ • w) x = w ((AlgEquiv.symm σ) x)

@[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 →+* ℂ) : σ • NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk (RingHom.comp φ ↑(AlgEquiv.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] (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) {f : F →+* K} : NumberField.InfinitePlace.comap (σ • w) f = NumberField.InfinitePlace.comap w (RingHom.comp (↑(AlgEquiv.symm σ)) f)

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 : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsReal (σ • w) ↔ NumberField.InfinitePlace.IsReal w

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 : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsComplex (σ • w) ↔ NumberField.InfinitePlace.IsComplex w

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 →+* ℂ) (ψ : K →+* ℂ) (h : RingHom.comp φ (algebraMap k K) = RingHom.comp ψ (algebraMap k K)) : ∃ (σ : K ≃ₐ[k] K), RingHom.comp φ ↑(AlgEquiv.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 : NumberField.InfinitePlace K} {w' : NumberField.InfinitePlace K} (h : NumberField.InfinitePlace.comap w (algebraMap k K) = NumberField.InfinitePlace.comap w' (algebraMap k K)) : ∃ (σ : K ≃ₐ[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 : NumberField.InfinitePlace K} {w' : NumberField.InfinitePlace K} : w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ NumberField.InfinitePlace.comap w (algebraMap k K) = NumberField.InfinitePlace.comap w' (algebraMap k K)

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) (NumberField.InfinitePlace K)) ≃ NumberField.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) => NumberField.InfinitePlace.comap x (algebraMap k K)) ⋯) ⋯

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 : NumberField.InfinitePlace K) : NumberField.InfinitePlace.orbitRelEquiv (Quotient.mk'' w) = NumberField.InfinitePlace.comap w (algebraMap k K)

def NumberField.InfinitePlace.IsUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] (w : NumberField.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 = (NumberField.InfinitePlace.mult (NumberField.InfinitePlace.comap w (algebraMap k K)) = NumberField.InfinitePlace.mult w)

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

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

theorem NumberField.InfinitePlace.isUnramified_iff_mult_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsUnramified k w ↔ NumberField.InfinitePlace.mult w ≤ NumberField.InfinitePlace.mult (NumberField.InfinitePlace.comap w (algebraMap k K))

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 : NumberField.InfinitePlace F} (h : NumberField.InfinitePlace.IsUnramified k w) (f : K →ₐ[k] F) : NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.comap w ↑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 : NumberField.InfinitePlace F} (h : NumberField.InfinitePlace.IsUnramified k w) : NumberField.InfinitePlace.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 : NumberField.InfinitePlace F} (h : NumberField.InfinitePlace.IsUnramified k w) : NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.comap w (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 : NumberField.InfinitePlace K} : ¬NumberField.InfinitePlace.IsUnramified k w ↔ NumberField.InfinitePlace.IsComplex w ∧ NumberField.InfinitePlace.IsReal (NumberField.InfinitePlace.comap w (algebraMap k K))

theorem NumberField.InfinitePlace.isUnramified_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsUnramified k w ↔ NumberField.InfinitePlace.IsReal w ∨ NumberField.InfinitePlace.IsComplex (NumberField.InfinitePlace.comap w (algebraMap k K))

theorem NumberField.InfinitePlace.IsReal.isUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : NumberField.InfinitePlace K} (h : NumberField.InfinitePlace.IsReal w) : NumberField.InfinitePlace.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] {σ : K ≃ₐ[k] K} {φ : K →+* ℂ} (h : NumberField.ComplexEmbedding.IsConj φ σ) : NumberField.InfinitePlace.IsUnramified k (NumberField.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 →+* ℂ} : NumberField.InfinitePlace.IsUnramified k (NumberField.InfinitePlace.mk φ) ↔ ∀ (σ : K ≃ₐ[k] K), NumberField.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 →+* ℂ) (σ : K ≃ₐ[k] K) : σ ∈ MulAction.stabilizer (K ≃ₐ[k] K) (NumberField.InfinitePlace.mk φ) ↔ σ = 1 ∨ NumberField.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 : NumberField.InfinitePlace K} (h : NumberField.InfinitePlace.IsUnramified k w) : MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥

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 : NumberField.ComplexEmbedding.IsConj φ σ) : ↑(MulAction.stabilizer (K ≃ₐ[k] K) (NumberField.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 : NumberField.InfinitePlace K) : Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1 ∨ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[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 : NumberField.InfinitePlace K} [IsGalois k K] : NumberField.InfinitePlace.IsUnramified k w ↔ MulAction.stabilizer (K ≃ₐ[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 : NumberField.InfinitePlace K} [IsGalois k K] : NumberField.InfinitePlace.IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[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 : NumberField.InfinitePlace K} [IsGalois k K] : ¬NumberField.InfinitePlace.IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2

theorem NumberField.InfinitePlace.card_stabilizer {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : NumberField.InfinitePlace K} [IsGalois k K] : Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = if NumberField.InfinitePlace.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 : NumberField.InfinitePlace K} [IsGalois k K] (hw : ¬NumberField.InfinitePlace.IsUnramified k w) : Even (Nat.card (K ≃ₐ[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 : NumberField.InfinitePlace K} [IsGalois k K] [FiniteDimensional k K] (hw : ¬NumberField.InfinitePlace.IsUnramified k w) : Even (Fintype.card (K ≃ₐ[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 : NumberField.InfinitePlace K} [IsGalois k K] (hw : ¬NumberField.InfinitePlace.IsUnramified k w) : Even (FiniteDimensional.finrank k K)

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 : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsUnramified k (σ • w) ↔ NumberField.InfinitePlace.IsUnramified k w

def NumberField.InfinitePlace.IsUnramifiedIn {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra k K] (w : NumberField.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), NumberField.InfinitePlace.comap v (algebraMap k K) = w → NumberField.InfinitePlace.IsUnramified k v

theorem NumberField.InfinitePlace.isUnramifiedIn_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : NumberField.InfinitePlace K} : NumberField.InfinitePlace.IsUnramifiedIn K (NumberField.InfinitePlace.comap w (algebraMap k K)) ↔ NumberField.InfinitePlace.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] [FiniteDimensional k K] {w : NumberField.InfinitePlace k} (hw : ¬NumberField.InfinitePlace.IsUnramifiedIn K w) : Even (Fintype.card (K ≃ₐ[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 : NumberField.InfinitePlace k} (hw : ¬NumberField.InfinitePlace.IsUnramifiedIn K w) : Even (FiniteDimensional.finrank k K)

theorem NumberField.InfinitePlace.card_isUnramified (k : Type u_1) [Field k] (K : Type u_2) [Field K] [NumberField K] [Algebra k K] [NumberField k] [IsGalois k K] : (Finset.filter (NumberField.InfinitePlace.IsUnramified k) Finset.univ).card = (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ).card * FiniteDimensional.finrank k K

theorem NumberField.InfinitePlace.card_isUnramified_compl (k : Type u_1) [Field k] (K : Type u_2) [Field K] [NumberField K] [Algebra k K] [NumberField k] [IsGalois k K] : (Finset.filter (NumberField.InfinitePlace.IsUnramified k) Finset.univ)ᶜ.card = (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ)ᶜ.card * (FiniteDimensional.finrank k K / 2)

theorem NumberField.InfinitePlace.card_eq_card_isUnramifiedIn (k : Type u_1) [Field k] (K : Type u_2) [Field K] [NumberField K] [Algebra k K] [NumberField k] [IsGalois k K] : Fintype.card (NumberField.InfinitePlace K) = (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ).card * FiniteDimensional.finrank k K + (Finset.filter (NumberField.InfinitePlace.IsUnramifiedIn K) Finset.univ)ᶜ.card * (FiniteDimensional.finrank k K / 2)

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

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

Equations

• ⋯ = ⋯

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] (h : 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 : NumberField.InfinitePlace K) : NumberField.InfinitePlace.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 : NumberField.InfinitePlace k) : NumberField.InfinitePlace.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] [FiniteDimensional k K] (h : Odd (Fintype.card (K ≃ₐ[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 (FiniteDimensional.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) * FiniteDimensional.finrank k K

theorem IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt {K : Type u_1} [Field K] [NumberField K] {ζ : K} {k : ℕ} (hk : 2 < k) (hζ : IsPrimitiveRoot ζ k) : NumberField.InfinitePlace.NrRealPlaces K = 0