MoritaUniformizer110.lean

1 import Mathlib.NumberTheory.LocalField.Basic
2 import Mathlib.RingTheory.DiscreteValuationRing.Basic
3 import Mathlib.SetTheory.Cardinal.Finite
4 
5 /-! Uniformizer arithmetic in the actual integer ring of a local field.
6 An irreducible integer-ring element generates the actual maximal ideal,
7 so primality, nonzeroness, and residue size are derived rather than supplied. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.MoritaUniformizer110
11 open ValuativeRel
12 
13 variable {E : Type*} [Field E] [ValuativeRel E] [TopologicalSpace E]
14   [IsNonarchimedeanLocalField E]
15 
16 /-- The literal ideal generated by an integer-ring uniformizer. -/
17 def uniformizerIdeal (π : 𝒪[E]) : Ideal 𝒪[E] := Ideal.span {π}
18 
19 /-- The DVR instance of the actual integer ring constructs a uniformizer. -/
20 theorem exists_uniformizer : ∃ π : 𝒪[E], Irreducible π :=
21   IsDiscreteValuationRing.exists_irreducible 𝒪[E]
22 
23 /-- Irreducibility identifies the generated ideal with the actual maximal ideal. -/
24 theorem uniformizerIdeal_eq_maximalIdeal (π : 𝒪[E]) (hπ : Irreducible π) :
25     uniformizerIdeal π = 𝓂[E] := hπ.maximalIdeal_eq.symm
26 
27 theorem uniformizerIdeal_ne_bot (π : 𝒪[E]) (hπ : Irreducible π) :
28     uniformizerIdeal π ≠ ⊥ := by
29   rw [uniformizerIdeal_eq_maximalIdeal π hπ]
30   exact IsDiscreteValuationRing.not_a_field 𝒪[E]
31 
32 theorem uniformizerIdeal_isMaximal (π : 𝒪[E]) (hπ : Irreducible π) :
33     (uniformizerIdeal π).IsMaximal := by
34   rw [uniformizerIdeal_eq_maximalIdeal π hπ]
35   infer_instance
36 
37 /-- The prime-ideal hypothesis for the ideal-power quotient theorem is derived. -/
38 theorem uniformizerIdeal_isPrime (π : 𝒪[E]) (hπ : Irreducible π) :
39     (uniformizerIdeal π).IsPrime :=
40   (uniformizerIdeal_isMaximal π hπ).isPrime
41 
42 /-- The canonical quotient by a uniformizer is the actual residue field. -/
43 def uniformizerResidueEquiv (π : 𝒪[E]) (hπ : Irreducible π) :
44     (𝒪[E] ⧸ uniformizerIdeal π) ≃+* 𝓀[E] :=
45   Ideal.quotEquivOfEq (uniformizerIdeal_eq_maximalIdeal π hπ)
46 
47 @[simp] theorem uniformizerResidueEquiv_mk (π : 𝒪[E]) (hπ : Irreducible π)
48     (x : 𝒪[E]) :
49     uniformizerResidueEquiv π hπ (Ideal.Quotient.mk (uniformizerIdeal π) x) =
50       IsLocalRing.residue 𝒪[E] x := rfl
51 
52 /-- Quotient finiteness follows from local-field residue finiteness. -/
53 theorem uniformizer_quotient_finite (π : 𝒪[E]) (hπ : Irreducible π) :
54     Finite (𝒪[E] ⧸ uniformizerIdeal π) :=
55   Finite.of_equiv 𝓀[E] (uniformizerResidueEquiv π hπ).symm.toEquiv
56 
57 /-- Its size is the actual residue size, with no supplied finite-card premise. -/
58 theorem card_uniformizer_quotient (π : 𝒪[E]) (hπ : Irreducible π) :
59     Nat.card (𝒪[E] ⧸ uniformizerIdeal π) = Nat.card 𝓀[E] :=
60   Nat.card_congr (uniformizerResidueEquiv π hπ).toEquiv
61 
62 end PaperXI.MoritaUniformizer110

Back to source controls