RamifiedConjugation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Cyclotomic conjugation and norm divisibility in a DVR

The conjugation fixes the coefficient ring and sends the actual adjoined root to its multiplicative inverse. In a DVR every ring automorphism preserves the canonical additive valuation, because it sends units to units and uniformizers to uniformizers. Consequently a norm equal to a unit times an even scalar power forces the corresponding half-power to divide the element.

theorem OAI.CirculantHadamard.RamifiedConjugation.addVal_ringEquiv line 32
Source documentation
Ring automorphisms of a DVR preserve its integer-valued order.
```
theorem addVal_ringEquiv (e : R ≃+* R) (x : R) :
    addVal R (e x) = addVal R x := by
…
```
theorem OAI.CirculantHadamard.RamifiedConjugation.enat_add_self_injective line 45
theorem OAI.CirculantHadamard.RamifiedConjugation.pow_dvd_of_norm_eq line 62
Source documentation
A norm with an even scalar exponent gives divisibility by half that power. The statement includes zero and needs no normalization assumption on the scalar's valuation.
```
theorem pow_dvd_of_norm_eq (e : R ≃+* R) (a x b : R) (t : ℕ)
    (hb : IsUnit b) (h : x * e x = a ^ (2 * t) * b) : a ^ t ∣ x := by
…
```
abbrev OAI.CirculantHadamard.RamifiedConjugation.CyclotomicRing line 79
Source documentation
The actual cyclotomic quotient used by the ramified construction.
```
abbrev CyclotomicRing := AdjoinRoot (cyclotomic n A)
```
theorem OAI.CirculantHadamard.RamifiedConjugation.root_pow_order line 83
Source documentation
The adjoined root satisfies the stated order relation even before domainhood or characteristic zero has been established.
```
theorem root_pow_order : AdjoinRoot.root (cyclotomic n A) ^ n = 1 := by
…
```
theorem OAI.CirculantHadamard.RamifiedConjugation.root_isPrimitiveRoot line 94
Source documentation
The quotient root is a primitive root of the exact specified order.
```
theorem root_isPrimitiveRoot :
    IsPrimitiveRoot (AdjoinRoot.root (cyclotomic n A)) n := by
…
```
theorem OAI.CirculantHadamard.RamifiedConjugation.root_pow_pred_mul_root line 100
theorem OAI.CirculantHadamard.RamifiedConjugation.inverse_root_aeval line 106
def OAI.CirculantHadamard.RamifiedConjugation.conjugationHom line 116
Source documentation
The root-inverting endomorphism fixes the coefficient algebra.
```
def conjugationHom : CyclotomicRing A n →ₐ[A] CyclotomicRing A n :=
…
```
Mentions: OAI.CirculantHadamard.RamifiedConjugation.CyclotomicRing
theorem OAI.CirculantHadamard.RamifiedConjugation.conjugationHom_root line 121
theorem OAI.CirculantHadamard.RamifiedConjugation.conjugationHom_comp_self line 128
def OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation line 150
Source documentation
The actual involutive algebra automorphism inverting the cyclotomic root.
```
def cyclotomicConjugation : CyclotomicRing A n ≃ₐ[A] CyclotomicRing A n :=
…
```
Mentions: OAI.CirculantHadamard.RamifiedConjugation.CyclotomicRing
theorem OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation_root line 154
theorem OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation_involutive line 159
theorem OAI.CirculantHadamard.RamifiedConjugation.cyclotomicConjugation_addVal line 166
theorem OAI.CirculantHadamard.RamifiedConjugation.cyclotomic_pow_dvd_of_norm_eq line 171