CyclotomicLocalBase.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The unramified cyclotomic coefficient ring

We use the actual subring ℤ[eta] of ℂ. At a maximal ideal above a rational prime not dividing the order of eta, its localization has maximal ideal generated by that prime. The central argument proves the vanishing of the universal derivation by differentiating eta ^ L = 1.

abbrev OAI.CirculantHadamard.CyclotomicLocalBase.Order line 31
Source documentation
The cyclotomic order as an actual subalgebra of the complex numbers.
```
abbrev Order (eta : ℂ) := Algebra.adjoin ℤ ({eta} : Set ℂ)
```
def OAI.CirculantHadamard.CyclotomicLocalBase.generator line 34
Source documentation
The distinguished root in its integral order.
```
def generator (eta : ℂ) : Order eta :=
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order
abbrev OAI.CirculantHadamard.CyclotomicLocalBase.Local line 38
Source documentation
Localization of the actual cyclotomic order at the chosen prime ideal.
```
abbrev Local (eta : ℂ) (m : Ideal (Order eta)) [m.IsPrime] :=
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order
theorem OAI.CirculantHadamard.CyclotomicLocalBase.order_pos line 43
def OAI.CirculantHadamard.CyclotomicLocalBase.powerBasis line 51
Source documentation
The genuine finite integral power basis of ℤ[eta].
```
def powerBasis (hη : IsPrimitiveRoot eta L) (hL : 0 < L) :
    PowerBasis ℤ (Order eta) :=
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order
theorem OAI.CirculantHadamard.CyclotomicLocalBase.powerBasis_gen line 55
theorem OAI.CirculantHadamard.CyclotomicLocalBase.order_finite line 59
theorem OAI.CirculantHadamard.CyclotomicLocalBase.order_free line 62
theorem OAI.CirculantHadamard.CyclotomicLocalBase.order_noetherian line 65
theorem OAI.CirculantHadamard.CyclotomicLocalBase.generator_pow line 70
theorem OAI.CirculantHadamard.CyclotomicLocalBase.local_noetherian line 75
instance OAI.CirculantHadamard.CyclotomicLocalBase.local_charZero line 79
theorem OAI.CirculantHadamard.CyclotomicLocalBase.prime_ne_zero line 83
theorem OAI.CirculantHadamard.CyclotomicLocalBase.order_not_mem line 86
theorem OAI.CirculantHadamard.CyclotomicLocalBase.order_isUnit line 96
theorem OAI.CirculantHadamard.CyclotomicLocalBase.formallyUnramified_of_powerBasis line 103
theorem OAI.CirculantHadamard.CyclotomicLocalBase.formallyUnramified line 151
Source documentation
Every absolute differential vanishes: the root has invertible derivative, and the same vanishing extends across the localization denominators.
```
theorem formallyUnramified (hη : IsPrimitiveRoot eta L) (hp : p.Prime)
    (hpL : ¬ p ∣ L) (m : Ideal (Order eta)) [m.IsMaximal]
    (hpm : (p : Order eta) ∈ m) : Algebra.FormallyUnramified ℤ (Local eta m) := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order, OAI.CirculantHadamard.CyclotomicLocalBase.Local
theorem OAI.CirculantHadamard.CyclotomicLocalBase.liesOver_prime line 167
Source documentation
The rational prime ideal lies under the chosen maximal ideal.
```
theorem liesOver_prime (hp : p.Prime) (m : Ideal (Order eta)) [hm : m.IsMaximal]
    (hpm : (p : Order eta) ∈ m) : m.LiesOver (Ideal.span {(p : ℤ)}) := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order
theorem OAI.CirculantHadamard.CyclotomicLocalBase.maximalIdeal_eq_span line 184
Source documentation
The maximal ideal is generated by the actual rational prime.
```
theorem maximalIdeal_eq_span (hη : IsPrimitiveRoot eta L) (hp : p.Prime)
    (hpL : ¬ p ∣ L) (m : Ideal (Order eta)) [m.IsMaximal]
    (hpm : (p : Order eta) ∈ m) :
    maximalIdeal (Local eta m) = Ideal.span {(p : Local eta m)} := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order, OAI.CirculantHadamard.CyclotomicLocalBase.Local
theorem OAI.CirculantHadamard.CyclotomicLocalBase.prime_not_isUnit line 200
theorem OAI.CirculantHadamard.CyclotomicLocalBase.isDiscreteValuationRing line 207
Source documentation
The concrete unramified localization is a discrete valuation ring.
```
theorem isDiscreteValuationRing (hη : IsPrimitiveRoot eta L) (hp : p.Prime)
    (hpL : ¬ p ∣ L) (m : Ideal (Order eta)) [m.IsMaximal]
    (hpm : (p : Order eta) ∈ m) : IsDiscreteValuationRing (Local eta m) := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicLocalBase.Order, OAI.CirculantHadamard.CyclotomicLocalBase.Local