CyclotomicAwayLocal.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The actual away coefficient localization

The prime ideal is the contraction of a maximal ideal of the actual global root ring. Its maximality follows from integrality of the coefficient inclusion, and the single-generator theorem identifies its localization with the unramified cyclotomic construction.

abbrev OAI.CirculantHadamard.CyclotomicAwayLocal.awayPrime line 25
Source documentation
The actual prime ideal on the coefficient ring with one direction omitted.
```
abbrev awayPrime (u p : ℕ) (m : Ideal (B u)) : Ideal (awayRing u p) :=
…
```
abbrev OAI.CirculantHadamard.CyclotomicAwayLocal.AwayLocal line 29
Source documentation
The coefficient localization used in the prime-direction comparison.
```
abbrev AwayLocal (u p : ℕ) (m : Ideal (B u)) [m.IsPrime] :=
…
```
instance OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_algebra line 32
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.awayInclusion_isIntegral line 39
Source documentation
Integrality follows from the genuine finite integer module structure of the global root ring, through the coefficient inclusion.
```
theorem awayInclusion_isIntegral (u p : ℕ) :
    (awayInclusion u p).toRingHom.IsIntegral := by
…
```
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.awayMaximal line 47
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.natCast_mem_comap_of_mem line 52
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.prime_mem_awayPrime line 58
instance OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_charZero line 62
instance OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_noetherian line 68
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.maximalIdeal_eq_span_of_eq line 73
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_maximalIdeal_eq_span line 83
Source documentation
The maximal ideal of the exact contracted localization is generated by the rational prime; no ring-property premise is assumed.
```
theorem awayLocal_maximalIdeal_eq_span (u p : ℕ) (hu : Odd u)
    (hp : p ∈ u.primeFactors) (m : Ideal (B u)) [m.IsMaximal]
    (hpm : (p : B u) ∈ m) :
    maximalIdeal (AwayLocal u p m) = Ideal.span {(p : AwayLocal u p m)} := by
…
```
Mentions: OAI.CirculantHadamard.CyclotomicAwayLocal.AwayLocal
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_prime_ne_zero line 93
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_prime_not_isUnit line 97
theorem OAI.CirculantHadamard.CyclotomicAwayLocal.awayLocal_isDiscreteValuationRing line 103