NormSignFormula.lean

1 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
2 
3 /-!
4 The signed field norm in mixed embedding coordinates.
5 
6 The embedding-fiber argument follows the proof of
7 `NumberField.InfinitePlace.prod_eq_abs_norm` in Mathlib, with the factors retained
8 before taking absolute values. That source carries the following notice:
9 Copyright (c) 2022 Xavier Roblot. All rights reserved.
10 Released under Apache 2.0 license as described in the file LICENSE.
11 Authors: Xavier Roblot
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 
16 namespace PaperX.NormSignArithmetic
17 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
18 open scoped Classical
19 variable (K : Type*) [Field K] [NumberField K]
20 
21 theorem embedding_fiber_eq_pair (w : InfinitePlace K) :
22     ({φ : K →+* ℂ | mk φ = w} : Finset _) =
23       {embedding w, ComplexEmbedding.conjugate (embedding w)} := by
24   ext φ
25   simp only [Finset.mem_filter, Finset.mem_univ, true_and,
26     Finset.mem_insert, Finset.mem_singleton]
27   conv_lhs => rw [← mk_embedding w, mk_eq_iff]
28   exact or_congr Iff.rfl ⟨fun h => by
29     simpa only [ComplexEmbedding.conjugate, star_star] using congrArg star h,
30     fun h => by
31       simpa only [ComplexEmbedding.conjugate, star_star] using congrArg star h⟩
32 
33 theorem embedding_fiber_product_real (x : K) (w : InfinitePlace K) (hw : IsReal w) :
34     (∏ φ ∈ ({φ : K →+* ℂ | mk φ = w} : Finset _), φ x) =
35       (embedding_of_isReal hw x : ℂ) := by
36   rw [embedding_fiber_eq_pair, conjugate_embedding_eq_of_isReal hw]
37   simp
38 
39 theorem embedding_fiber_product_complex (x : K) (w : InfinitePlace K)
40     (hw : IsComplex w) :
41     (∏ φ ∈ ({φ : K →+* ℂ | mk φ = w} : Finset _), φ x) =
42       ((‖embedding w x‖ ^ 2 : ℝ) : ℂ) := by
43   rw [embedding_fiber_eq_pair]
44   have hne : embedding w ≠ ComplexEmbedding.conjugate (embedding w) := by
45     intro h
46     exact (isComplex_iff.mp hw) (ComplexEmbedding.isReal_iff.mpr h.symm)
47   rw [Finset.prod_pair hne]
48   simp only [ComplexEmbedding.conjugate_coe_eq]
49   rw [Complex.mul_conj, Complex.normSq_eq_norm_sq]
50 
51 /-- The signed rational field norm, before taking absolute values. -/
52 theorem field_norm_eq_real_mul_complex (x : K) :
53     (Algebra.norm ℚ x : ℝ) =
54       (∏ w : {w : InfinitePlace K // IsReal w}, (mixedEmbedding K x).1 w) *
55         ∏ w : {w : InfinitePlace K // IsComplex w}, ‖(mixedEmbedding K x).2 w‖ ^ 2 := by
56   apply Complex.ofReal_injective
57   rw [Complex.ofReal_ratCast, Complex.ofReal_mul, Complex.ofReal_prod, Complex.ofReal_prod]
58   calc
59     (Algebra.norm ℚ x : ℂ) = ∏ φ : K →+* ℂ, φ x := by
60       simpa only [eq_ratCast] using (Algebra.norm_eq_prod_embeddings ℚ ℂ x).trans
61         (Fintype.prod_equiv (RingHom.equivRatAlgHom K ℂ).symm _ _ (fun _ => rfl))
62     _ = (∏ w : {w : InfinitePlace K // IsReal w}, ((mixedEmbedding K x).1 w : ℂ)) *
63         ∏ w : {w : InfinitePlace K // IsComplex w}, ((‖(mixedEmbedding K x).2 w‖ ^ 2 : ℝ) : ℂ) := by
64       rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => φ x), prod_eq_prod_mul_prod]
65       congr 1
66       · apply Finset.prod_congr rfl
67         intro w _
68         exact embedding_fiber_product_real K x w.1 w.2
69       · apply Finset.prod_congr rfl
70         intro w _
71         exact embedding_fiber_product_complex K x w.1 w.2
72 
73 theorem complex_factor_pos {x : K} (hx : x ≠ 0) :
74     0 < ∏ w : {w : InfinitePlace K // IsComplex w}, ‖(mixedEmbedding K x).2 w‖ ^ 2 := by
75   apply Finset.prod_pos
76   intro w _
77   apply pow_pos
78   rw [norm_pos_iff, mixedEmbedding_apply_isComplex]
79   exact fun h => hx ((embedding w.1).injective (by simpa using h))
80 
81 end PaperX.NormSignArithmetic

Back to source controls