feat(number_theory/number_field/embeddings) : add infinite_places (#1…

…7844)

This PR adds definitions and basic lemmas about places, complex embeddings and infinite places of number field.

src/algebra/star/basic.lean

@@ -291,16 +291,16 @@ lemma star_ring_end_apply [comm_semiring R] [star_ring R] {x : R} :
 @[simp] lemma star_ring_end_self_apply [comm_semiring R] [star_ring R] (x : R) :
   star_ring_end R (star_ring_end R x) = x := star_star x
 
-instance ring_hom.has_involutive_star {S : Type u} [non_assoc_semiring S] [comm_semiring R]
+instance ring_hom.has_involutive_star {S : Type*} [non_assoc_semiring S] [comm_semiring R]
   [star_ring R] : has_involutive_star (S →+* R) :=
 { to_has_star := { star := λ f, ring_hom.comp (star_ring_end R) f },
   star_involutive :=
     by { intro _, ext, simp only [ring_hom.coe_comp, function.comp_app, star_ring_end_self_apply] }}
 
-lemma ring_hom.star_def {S : Type u} [non_assoc_semiring S] [comm_semiring R] [star_ring R]
+lemma ring_hom.star_def {S : Type*} [non_assoc_semiring S] [comm_semiring R] [star_ring R]
   (f : S →+* R) : has_star.star f = ring_hom.comp (star_ring_end R) f := rfl
 
-lemma ring_hom.star_apply {S : Type u} [non_assoc_semiring S] [comm_semiring R] [star_ring R]
+lemma ring_hom.star_apply {S : Type*} [non_assoc_semiring S] [comm_semiring R] [star_ring R]
   (f : S →+* R) (s : S) : star f s = star (f s) := rfl
 
 -- A more convenient name for complex conjugation

src/analysis/normed/field/basic.lean

@@ -414,6 +414,12 @@ instance normed_division_ring.to_norm_one_class : norm_one_class α :=
 ⟨mul_left_cancel₀ (mt norm_eq_zero.1 (one_ne_zero' α)) $
   by rw [← norm_mul, mul_one, mul_one]⟩
 
+instance is_absolute_value_norm : is_absolute_value (norm : α → ℝ) :=
+{ abv_nonneg := norm_nonneg,
+  abv_eq_zero := λ _, norm_eq_zero,
+  abv_add := norm_add_le,
+  abv_mul := norm_mul }
+
 @[simp] lemma nnnorm_mul (a b : α) : ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊ :=
 nnreal.eq $ norm_mul a b
 

src/number_theory/number_field/embeddings.lean

@@ -4,25 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best, Xavier Roblot
 -/
 
-import analysis.normed_space.basic
 import number_theory.number_field.basic
-import topology.algebra.polynomial
+import analysis.complex.polynomial
+import data.complex.basic
 
 /-!
 # Embeddings of number fields
 This file defines the embeddings of a number field into an algebraic closed field.
 
 ## Main Results
-* `number_field.embeddings.eq_roots`: 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 `ℚ`.
+* `number_field.embeddings.range_eval_eq_root_set_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 `ℚ`.
 * `number_field.embeddings.pow_eq_one_of_norm_eq_one`: an algebraic integer whose conjugates are
   all of norm one is a root of unity.
 
 ## Tags
-number field, embeddings
+number field, embeddings, places, infinite places
 -/
 
+open_locale classical
+
 namespace number_field.embeddings
 
 section fintype
@@ -42,6 +44,12 @@ variables [is_alg_closed A]
 lemma card : fintype.card (K →+* A) = finrank ℚ K :=
 by rw [fintype.of_equiv_card ring_hom.equiv_rat_alg_hom.symm, alg_hom.card]
 
+instance : nonempty (K →+* A) :=
+begin
+  rw [← fintype.card_pos_iff, number_field.embeddings.card K A],
+  exact finite_dimensional.finrank_pos,
+end
+
 end fintype
 
 section roots
@@ -123,3 +131,119 @@ end
 end bounded
 
 end number_field.embeddings
+
+section place
+
+variables {K : Type*} [field K] {A : Type*} [normed_division_ring A] [nontrivial A] (φ : K →+* A)
+
+/-- An embedding into a normed division ring defines a place of `K` -/
+def number_field.place : absolute_value K ℝ :=
+(is_absolute_value.to_absolute_value (norm : A → ℝ)).comp φ.injective
+
+@[simp]
+lemma number_field.place_apply (x : K) : (number_field.place φ) x = norm (φ x) := rfl
+
+end place
+
+namespace number_field.complex_embedding
+
+open complex number_field
+
+open_locale complex_conjugate
+
+variables {K : Type*} [field K]
+
+/-- The conjugate of a complex embedding as a complex embedding. -/
+@[reducible] def conjugate (φ : K →+* ℂ) : K →+* ℂ := star φ
+
+@[simp]
+lemma conjugate_coe_eq (φ : K →+* ℂ) (x : K) : (conjugate φ) x = conj (φ x) := rfl
+
+lemma place_conjugate (φ : K →+* ℂ) : place (conjugate φ) = place φ :=
+by { ext, simp only [place_apply, norm_eq_abs, abs_conj, conjugate_coe_eq] }
+
+/-- A embedding into `ℂ` is real if it is fixed by complex conjugation. -/
+@[reducible] def is_real (φ : K →+* ℂ) : Prop := is_self_adjoint φ
+
+lemma is_real_iff {φ : K →+* ℂ} : is_real φ ↔ conjugate φ = φ := is_self_adjoint_iff
+
+/-- A real embedding as a ring homomorphism from `K` to `ℝ` . -/
+def is_real.embedding {φ : K →+* ℂ} (hφ : is_real φ) : K →+* ℝ :=
+{ to_fun := λ x, (φ x).re,
+  map_one' := by simp only [map_one, one_re],
+  map_mul' := by simp only [complex.eq_conj_iff_im.mp (ring_hom.congr_fun hφ _), map_mul, mul_re,
+  mul_zero, tsub_zero, eq_self_iff_true, forall_const],
+  map_zero' := by simp only [map_zero, zero_re],
+  map_add' := by simp only [map_add, add_re, eq_self_iff_true, forall_const], }
+
+@[simp]
+lemma is_real.coe_embedding_apply {φ : K →+* ℂ} (hφ : is_real φ) (x : K) :
+  (hφ.embedding x : ℂ) = φ x :=
+begin
+  ext, { refl, },
+  { rw [of_real_im, eq_comm, ← complex.eq_conj_iff_im],
+    rw is_real at hφ,
+    exact ring_hom.congr_fun hφ x, },
+end
+
+lemma is_real.place_embedding {φ : K →+* ℂ} (hφ : is_real φ) :
+  place hφ.embedding = place φ :=
+by { ext x, simp only [place_apply, real.norm_eq_abs, ←abs_of_real, norm_eq_abs,
+  hφ.coe_embedding_apply x], }
+
+lemma is_real_conjugate_iff {φ : K →+* ℂ} :
+  is_real (conjugate φ) ↔ is_real φ := is_self_adjoint.star_iff
+
+end number_field.complex_embedding
+
+section infinite_place
+
+open number_field
+
+variables (K : Type*) [field K]
+
+/-- An infinite place of a number field `K` is a place associated to a complex embedding. -/
+def number_field.infinite_place := { w : absolute_value K ℝ  // ∃ φ : K →+* ℂ, place φ = w}
+
+instance [number_field K] : nonempty (number_field.infinite_place K) := set.range.nonempty _
+
+variables {K}
+
+/-- Return the infinite place defined by a complex embedding `φ`. -/
+noncomputable def number_field.infinite_place.mk (φ : K →+* ℂ) : number_field.infinite_place K :=
+⟨place φ, ⟨φ, rfl⟩⟩
+
+namespace number_field.infinite_place
+
+open number_field
+
+instance : has_coe_to_fun (infinite_place K) (λ _, K → ℝ) := { coe := λ w, w.1 }
+
+instance : monoid_with_zero_hom_class (infinite_place K) K ℝ :=
+{ coe := λ w x, w.1 x,
+  coe_injective' := λ _ _ h, subtype.eq (absolute_value.ext (λ x, congr_fun h x)),
+  map_mul := λ w _ _, w.1.map_mul _ _,
+  map_one := λ w, w.1.map_one,
+  map_zero := λ w, w.1.map_zero, }
+
+instance : nonneg_hom_class (infinite_place K) K ℝ :=
+{ coe :=  λ w x, w x,
+  coe_injective' := λ _ _ h, subtype.eq (absolute_value.ext (λ x, congr_fun h x)),
+  map_nonneg := λ w x, w.1.nonneg _ }
+
+lemma coe_mk (φ : K →+* ℂ) : ⇑(mk φ) = place φ := rfl
+
+lemma apply (φ : K →+* ℂ) (x : K) : (mk φ) x = complex.abs (φ x) := rfl
+
+/-- For an infinite place `w`, return an embedding `φ` such that `w = infinite_place φ` . -/
+noncomputable def embedding (w : infinite_place K) : K →+* ℂ := (w.2).some
+
+lemma mk_embedding (w : infinite_place K) :
+  mk (embedding w) = w :=
+subtype.ext (w.2).some_spec
+
+lemma pos_iff (w : infinite_place K) (x : K) : 0 < w x ↔ x ≠ 0 := absolute_value.pos_iff w.1
+
+end number_field.infinite_place
+
+end infinite_place

src/topology/algebra/ring.lean

@@ -472,3 +472,18 @@ def to_add_group_topology.order_embedding : order_embedding (ring_topology α)
   end }
 
 end ring_topology
+
+section absolute_value
+
+/-- Construct an absolute value on a semiring `T` from an absolute value on a semiring `R`
+and an injective ring homomorphism `f : T →+* R` -/
+def absolute_value.comp {R S T : Type*} [semiring T] [semiring R] [ordered_semiring S]
+  (v : absolute_value R S) {f : T →+* R} (hf : function.injective f)  :
+  absolute_value T S :=
+{ to_fun := v ∘ f,
+  map_mul' := by simp only [function.comp_app, map_mul, eq_self_iff_true, forall_const],
+  nonneg' := by simp only [v.nonneg, forall_const],
+  eq_zero' := by simp only [map_eq_zero_iff f hf, v.eq_zero, forall_const, iff_self],
+  add_le' := by simp only [function.comp_app, map_add, v.add_le, forall_const], }
+
+end absolute_value

src/topology/metric_space/cau_seq_filter.lean

@@ -41,16 +41,10 @@ variables [normed_field β]
  This section shows that if we have a uniform space generated by an absolute value, topological
  completeness and Cauchy sequence completeness coincide. The problem is that there isn't
  a good notion of "uniform space generated by an absolute value", so right now this is
- specific to norm. Furthermore, norm only instantiates is_absolute_value on normed_field.
+ specific to norm. Furthermore, norm only instantiates is_absolute_value on normed_division_ring.
  This needs to be fixed, since it prevents showing that ℤ_[hp] is complete
 -/
 
-instance normed_field.is_absolute_value : is_absolute_value (norm : β → ℝ) :=
-{ abv_nonneg := norm_nonneg,
-  abv_eq_zero := λ _, norm_eq_zero,
-  abv_add := norm_add_le,
-  abv_mul := norm_mul }
-
 open metric
 
 lemma cauchy_seq.is_cau_seq {f : ℕ → β} (hf : cauchy_seq f) :