LocalComparison.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local character comparison in the actual cyclotomic quotient

Starting with a characteristic-zero DVR whose maximal ideal is generated by the rational prime p, all ramified rings needed by the induction are constructed as the actual cyclotomic quotients. No projection-divisibility, comparison, or existence-of-valuation premise is taken from the caller.

The conclusion uses membership in the ideal generated by root - 1 to state residue one. This is independent of how a local-ring instance is installed and can be transported directly to a later localization.

def OAI.CirculantHadamard.LocalComparison.orderPRoot line 32
Source documentation
The fixed primitive-order-p root used at every induction level.
```
def orderPRoot (p : ℕ) : RamifiedLocal.Extension A p 0 :=
…
```
Mentions: OAI.CirculantHadamard.RamifiedLocal.Extension
theorem OAI.CirculantHadamard.LocalComparison.orderPRoot_pow line 35
theorem OAI.CirculantHadamard.LocalComparison.orderPRoot_pow_level line 41
def OAI.CirculantHadamard.LocalComparison.orderPValue line 50
Source documentation
Actual order-p evaluation of an element of the cyclic group ring of order p ^ (e + 1).
```
def orderPValue (p e : ℕ) [NeZero p] :
    Elem A (p ^ (e + 1)) →ₐ[A] RamifiedLocal.Extension A p 0 :=
…
```
Mentions: OAI.CirculantHadamard.RamifiedLocal.Extension
theorem OAI.CirculantHadamard.LocalComparison.orderPValue_scalar line 54
theorem OAI.CirculantHadamard.LocalComparison.orderPValue_projection line 59
def OAI.CirculantHadamard.LocalComparison.OrderPCompared line 68
Source documentation
The conclusion of comparison, expressed by an actual unit and membership in the actual ramified maximal ideal.
```
def OrderPCompared (p e : ℕ) [NeZero p] (F : Elem A (p ^ (e + 1))) : Prop :=
…
```

theorem OAI.CirculantHadamard.LocalComparison.local_character_comparison line 81

Source documentation

Character comparison with every ramified extension constructed from the input DVR. Both factors are compared, with matching group/scalar exponents.

theorem local_character_comparison (p : ℕ) [NeZero p] (hp : p.Prime)
    (hmax : IsLocalRing.maximalIdeal A = Ideal.span {(p : A)})
    (e : ℕ) (b : Aˣ) (F K : Elem A (p ^ (e + 1)))
    (hFK : F * K = scalar (p ^ (e + 1)) ((p : A) ^ (e + 1) * (b : A))) :
    OrderPCompared A p e F ∧ OrderPCompared A p e K := by
…

Mentions: OAI.CirculantHadamard.LocalComparison.OrderPCompared

theorem OAI.CirculantHadamard.LocalComparison.local_character_comparison_denominators line 146

Source documentation

The augmentation denominators used in the corresponding ratio statement are nonzero in the coefficient DVR.

theorem local_character_comparison_denominators [IsDiscreteValuationRing A] (p : ℕ) (hp : p.Prime)
    (e : ℕ) (b : Aˣ) (F K : Elem A (p ^ (e + 1)))
    (hFK : F * K = scalar (p ^ (e + 1)) ((p : A) ^ (e + 1) * (b : A))) :
    augmentation (p ^ (e + 1)) F ≠ 0 ∧ augmentation (p ^ (e + 1)) K ≠ 0 :=
…