RamifiedLocal.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The actual ramified cyclotomic local ring

We adjoin a root of the prime-power cyclotomic polynomial to the given characteristic-zero DVR. Every maximal ideal of this finite integral extension is shown to be generated by the actual element root - 1.

abbrev OAI.CirculantHadamard.RamifiedLocal.Extension line 26
Source documentation
The genuine monic cyclotomic quotient, with no additional ring-data premise.
```
abbrev Extension (A : Type uA) [CommRing A] (p k : ℕ) :=
…
```
def OAI.CirculantHadamard.RamifiedLocal.uniformizer line 30
Source documentation
The actual ramified parameter in the cyclotomic quotient.
```
def uniformizer (A : Type uA) [CommRing A] (p k : ℕ) : Extension A p k :=
…
```
Mentions: OAI.CirculantHadamard.RamifiedLocal.Extension
instance OAI.CirculantHadamard.RamifiedLocal.extensionFinite line 33
theorem OAI.CirculantHadamard.RamifiedLocal.uniformizer_aeval_shifted line 37
theorem OAI.CirculantHadamard.RamifiedLocal.exists_scalar_add_uniformizer_mul line 43
Source documentation
Every element is a scalar modulo the actual root-minus-one parameter.
```
theorem exists_scalar_add_uniformizer_mul (A : Type uA) [CommRing A] (p k : ℕ)
    (x : Extension A p k) :
    ∃ a : A, ∃ b : Extension A p k,
      x = algebraMap A (Extension A p k) a + uniformizer A p k * b := by
…
```
Mentions: OAI.CirculantHadamard.RamifiedLocal.Extension, OAI.CirculantHadamard.RamifiedLocal.uniformizer
theorem OAI.CirculantHadamard.RamifiedLocal.prime_mem_span_uniformizer line 65
theorem OAI.CirculantHadamard.RamifiedLocal.isDomain line 86
theorem OAI.CirculantHadamard.RamifiedLocal.maximal_eq_span_uniformizer line 91
Source documentation
Every maximal ideal of the genuine quotient is the same principal ideal.
```
theorem maximal_eq_span_uniformizer [CharZero A] (M : Ideal (Extension A p k)) [M.IsMaximal] :
    M = Ideal.span {uniformizer A p k} := by
…
```
Mentions: OAI.CirculantHadamard.RamifiedLocal.Extension, OAI.CirculantHadamard.RamifiedLocal.uniformizer
theorem OAI.CirculantHadamard.RamifiedLocal.isLocalRing line 124
theorem OAI.CirculantHadamard.RamifiedLocal.maximalIdeal_eq_span line 137
theorem OAI.CirculantHadamard.RamifiedLocal.root_residue_eq_one line 141
theorem OAI.CirculantHadamard.RamifiedLocal.exists_unit_mul_uniformizer_pow line 152
theorem OAI.CirculantHadamard.RamifiedLocal.algebraMap_injective line 175
theorem OAI.CirculantHadamard.RamifiedLocal.charZero line 182
theorem OAI.CirculantHadamard.RamifiedLocal.uniformizer_ne_zero line 186
theorem OAI.CirculantHadamard.RamifiedLocal.isDiscreteValuationRing line 201
theorem OAI.CirculantHadamard.RamifiedLocal.addVal_prime line 206