NumberFieldPrimeRestriction.lean

1 import PaperX.AbsoluteIntegralFrobenius
2 
3 /-! Restriction of actual primes of the algebraic integers in Qbar to the ring
4 of integers of an arbitrary normal number field. All maps use the same chosen
5 field embedding as absolute Galois restriction. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.NumberFieldPrimeRestriction
9 open scoped Pointwise
10 open AbsoluteIntegralFrobenius
11 open NumberField
12 
13 variable (L : Type*) [Field L] [NumberField L] [Normal ℚ L]
14 
15 /-- The chosen field embedding restricted to the actual rings of integers. -/
16 def integralEmbedding : 𝓞 L →+* IntegralClosure :=
17   RingOfIntegers.mapRingHom (AbsoluteGaloisRestriction.embedding L).toRingHom
18 
19 theorem integralEmbedding_apply (x : 𝓞 L) :
20     (integralEmbedding L x : Qbar) = AbsoluteGaloisRestriction.embedding L (x : L) := rfl
21 
22 theorem integralEmbedding_injective : Function.Injective (integralEmbedding L) := by
23   intro x y h
24   apply Subtype.ext
25   apply (AbsoluteGaloisRestriction.embedding L).injective
26   exact congrArg (fun z : IntegralClosure => (z : Qbar)) h
27 
28 /-- The integral embedding intertwines the actual absolute and restricted actions. -/
29 theorem integralEmbedding_smul (σ : GQ) (x : 𝓞 L) :
30     integralEmbedding L (AbsoluteGaloisRestriction.restriction L σ • x) =
31       σ • integralEmbedding L x := by
32   apply Subtype.ext
33   exact AbsoluteGaloisRestriction.restriction_commutes L σ (x : L)
34 
35 /-- Contraction of an actual algebraic-integer prime to the chosen number field. -/
36 def restrictedPrime (Q : Ideal IntegralClosure) : Ideal (𝓞 L) :=
37   Q.comap (integralEmbedding L)
38 
39 theorem mem_restrictedPrime (Q : Ideal IntegralClosure) (x : 𝓞 L) :
40     x ∈ restrictedPrime L Q ↔ integralEmbedding L x ∈ Q := Iff.rfl
41 
42 theorem restrictedPrime_isPrime (Q : Ideal IntegralClosure) [Q.IsPrime] :
43     (restrictedPrime L Q).IsPrime := Q.comap_isPrime (integralEmbedding L)
44 
45 /-- The actual residue map induced by the integral embedding. -/
46 def quotientEmbedding (Q : Ideal IntegralClosure) :
47     (𝓞 L ⧸ restrictedPrime L Q) →+* (IntegralClosure ⧸ Q) :=
48   Ideal.quotientMap Q (integralEmbedding L) le_rfl
49 
50 theorem quotientEmbedding_mk (Q : Ideal IntegralClosure) (x : 𝓞 L) :
51     quotientEmbedding L Q (Ideal.Quotient.mk (restrictedPrime L Q) x) =
52       Ideal.Quotient.mk Q (integralEmbedding L x) := rfl
53 
54 theorem quotientEmbedding_injective (Q : Ideal IntegralClosure) :
55     Function.Injective (quotientEmbedding L Q) := Ideal.quotientMap_injective
56 
57 variable (p : ℕ) [hp : Fact p.Prime]
58   (Q : Ideal IntegralClosure) [hQover : Q.LiesOver (Ideal.span {(p : ℤ)})]
59 
60 omit hp in
61 /-- Contraction preserves the specified rational prime below the ideal. -/
62 theorem restrictedPrime_liesOver :
63     (restrictedPrime L Q).LiesOver (Ideal.span {(p : ℤ)}) := by
64   constructor
65   rw [Ideal.over_def Q (Ideal.span {(p : ℤ)})]
66   ext z
67   change algebraMap ℤ IntegralClosure z ∈ Q ↔
68     integralEmbedding L (algebraMap ℤ (𝓞 L) z) ∈ Q
69   simp only [map_intCast, eq_intCast]
70 
71 omit hp in
72 theorem prime_mem_restrictedPrime : (p : 𝓞 L) ∈ restrictedPrime L Q := by
73   let : (restrictedPrime L Q).LiesOver (Ideal.span {(p : ℤ)}) :=
74     restrictedPrime_liesOver L p Q
75   simpa only [map_natCast] using
76     (Ideal.mem_of_liesOver (restrictedPrime L Q) (Ideal.span {(p : ℤ)}) (p : ℤ)).mp
77     (Ideal.subset_span (Set.mem_singleton _))
78 
79 include hp hQover in
80 /-- A contracted prime above p is nonzero. -/
81 theorem restrictedPrime_ne_bot : restrictedPrime L Q ≠ ⊥ := by
82   intro h
83   have hz : (p : 𝓞 L) = 0 := by
84     simpa only [h, Ideal.mem_bot] using prime_mem_restrictedPrime L p Q
85   exact hp.out.ne_zero ((Nat.cast_eq_zero.mp hz))
86 
87 include hp hQover in
88 /-- Nonzero prime ideals of a number-field ring of integers are maximal. -/
89 theorem restrictedPrime_isMaximal [Q.IsPrime] : (restrictedPrime L Q).IsMaximal :=
90   (restrictedPrime_isPrime L Q).isMaximal (restrictedPrime_ne_bot L p Q)
91 
92 end PaperX.NumberFieldPrimeRestriction

Back to source controls