NormSignArithmetic.lean

1 import PaperX.NormSignFormula
2 import PaperX.NormSignGeometry
3 import Mathlib.NumberTheory.NumberField.Norm
4 
5 /-! The geometric real-coordinate sign is exactly the sign of the actual field
6 norm and of the integral norm on the ring of integers. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperX.NormSignArithmetic
11 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
12 open NormSignGeometry
13 open scoped Classical
14 variable (K : Type*) [Field K] [NumberField K]
15 
16 theorem field_norm_pos_iff {x : K} (hx : x ≠ 0) :
17     (0 : ℝ) < Algebra.norm ℚ x ↔ 0 < realProduct K (mixedEmbedding K x) := by
18   rw [field_norm_eq_real_mul_complex]
19   exact mul_pos_iff_of_pos_right (complex_factor_pos K hx)
20 
21 theorem field_norm_neg_iff {x : K} (hx : x ≠ 0) :
22     (Algebra.norm ℚ x : ℝ) < 0 ↔ realProduct K (mixedEmbedding K x) < 0 := by
23   rw [field_norm_eq_real_mul_complex]
24   have hp := complex_factor_pos K hx
25   unfold realProduct
26   constructor
27   · intro h
28     nlinarith
29   · intro h
30     exact mul_neg_of_neg_of_pos h hp
31 
32 theorem integer_norm_pos_iff {x : 𝓞 K} (hx : x ≠ 0) :
33     0 < Algebra.norm ℤ x ↔ 0 < realProduct K (mixedEmbedding K (x : K)) := by
34   have hn : (x : K) ≠ 0 := by exact_mod_cast hx
35   have he : (Algebra.norm ℚ (x : K) : ℝ) = (Algebra.norm ℤ x : ℝ) := by
36     rw [← Algebra.coe_norm_int, Rat.cast_intCast]
37   rw [← Int.cast_pos (R := ℝ), ← he]
38   exact field_norm_pos_iff K hn
39 
40 theorem integer_norm_neg_iff {x : 𝓞 K} (hx : x ≠ 0) :
41     Algebra.norm ℤ x < 0 ↔ realProduct K (mixedEmbedding K (x : K)) < 0 := by
42   have hn : (x : K) ≠ 0 := by exact_mod_cast hx
43   have he : (Algebra.norm ℚ (x : K) : ℝ) = (Algebra.norm ℤ x : ℝ) := by
44     rw [← Algebra.coe_norm_int, Rat.cast_intCast]
45   rw [← Int.cast_lt_zero (R := ℝ), ← he]
46   exact field_norm_neg_iff K hn
47 
48 /-- No sign assumption is added: membership in the actual positive cone forces
49 the integral norm to be positive. -/
50 theorem integer_norm_pos_of_mem_signCone {x : 𝓞 K}
51     (hx : mixedEmbedding K (x : K) ∈ signCone K true) : 0 < Algebra.norm ℤ x := by
52   have hne : x ≠ 0 := by
53     intro he
54     subst x
55     have hp := fundamentalCone.normAtPlace_pos_of_mem hx.1.1
56       (Classical.arbitrary (InfinitePlace K))
57     simp at hp
58   exact (integer_norm_pos_iff K hne).mpr hx.2
59 
60 theorem integer_norm_neg_of_mem_signCone {x : 𝓞 K}
61     (hx : mixedEmbedding K (x : K) ∈ signCone K false) : Algebra.norm ℤ x < 0 := by
62   have hne : x ≠ 0 := by
63     intro he
64     subst x
65     have hp := fundamentalCone.normAtPlace_pos_of_mem hx.1.1
66       (Classical.arbitrary (InfinitePlace K))
67     simp at hp
68   exact (integer_norm_neg_iff K hne).mpr (neg_pos.mp hx.2)
69 
70 end PaperX.NormSignArithmetic

Back to source controls