AlternatingLocalization.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Local representatives of the fixed alternating product

All local rings are actual localizations at maximal ideals. Their maps into the common fraction field are canonical. The adjoined-root comparison map is constructed from the actual base-ring inclusion and cyclotomic relation. Membership in every maximal localization implies membership in the base ring.

abbrev OAI.CirculantHadamard.AlternatingLocalization.AtMaximal line 36
def OAI.CirculantHadamard.AlternatingLocalization.toFraction line 39
theorem OAI.CirculantHadamard.AlternatingLocalization.toFraction_injective line 45
theorem OAI.CirculantHadamard.AlternatingLocalization.local_representative_eq line 58
Source documentation
The integral representative and a local representative of the same fixed fraction agree under the actual coefficient localization map.
```
theorem local_representative_eq {R : Type uR} [CommRing R] [IsDomain R]
    (K : Type uK) [Field K] [Algebra R K] [IsFractionRing R K]
    (m : MaximalSpectrum R) (b : R) (v : AtMaximal R m)
    (h : algebraMap R K b = toFraction K m v) :
    algebraMap R (AtMaximal R m) b = v := by
…
```
Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal, OAI.CirculantHadamard.AlternatingLocalization.toFraction
abbrev OAI.CirculantHadamard.AlternatingLocalization.AtComap line 73
Source documentation
The actual coefficient localization at the contracted prime. Maximality of the contraction is a separate input to the local comparison theorem, not an assumption needed to construct this map.
```
abbrev AtComap (f : A₀ →+* R) (m : MaximalSpectrum R) :=
…
```
def OAI.CirculantHadamard.AlternatingLocalization.baseToLocal line 76
theorem OAI.CirculantHadamard.AlternatingLocalization.baseToLocal_algebraMap line 80
def OAI.CirculantHadamard.AlternatingLocalization.comparisonToLocal line 88
Source documentation
The comparison algebra is mapped by the universal property of its actual cyclotomic quotient, rather than by assuming an arbitrary extension map.
```
def comparisonToLocal (f : A₀ →+* R) (m : MaximalSpectrum R) (p : ℕ) (rho : R)
    (hroot : (Polynomial.cyclotomic p R).eval rho = 0) :
    AdjoinRoot (Polynomial.cyclotomic p (AtComap f m)) →+* AtMaximal R m :=
…
```
Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtComap, OAI.CirculantHadamard.AlternatingLocalization.AtMaximal
theorem OAI.CirculantHadamard.AlternatingLocalization.comparisonToLocal_root line 95
theorem OAI.CirculantHadamard.AlternatingLocalization.comparisonToLocal_of line 102
theorem OAI.CirculantHadamard.AlternatingLocalization.residue_charP line 112
Source documentation
Residue characteristic is derived from membership of the rational prime, not assumed as an independent property of the chosen maximal ideal.
```
theorem residue_charP (m : MaximalSpectrum R) (p : ℕ) (hp : p.Prime)
    (hpm : (p : R) ∈ m.asIdeal) :
    CharP (IsLocalRing.ResidueField (AtMaximal R m)) p := by
…
```
Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal

theorem OAI.CirculantHadamard.AlternatingLocalization.residue_root_eq_one line 124

Source documentation

A p-th root has residue one at every maximal ideal containing p.

theorem residue_root_eq_one (m : MaximalSpectrum R) (p : ℕ) (hp : p.Prime)
    (hpm : (p : R) ∈ m.asIdeal) (rho : R) (hrho : rho ^ p = 1) :
    IsLocalRing.residue (AtMaximal R m) (algebraMap R (AtMaximal R m) rho) = 1 := by
…

Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal

theorem OAI.CirculantHadamard.AlternatingLocalization.residue_unit_eq_one_of_span line 138
theorem OAI.CirculantHadamard.AlternatingLocalization.map_residueOneAssociated line 156

theorem OAI.CirculantHadamard.AlternatingLocalization.local_edge_of_associated line 176

Source documentation

The local association is converted to the actual fraction-field quotient only after the augmentation image is known to be nonzero.

theorem local_edge_of_associated {R : Type uR} {K : Type uK} [CommRing R] [IsDomain R]
    [Field K] [Algebra R K] [IsFractionRing R K] (m : MaximalSpectrum R)
    (a b : R) (hb : algebraMap R K b ≠ 0)
    (h : LocalComparison.ResidueOneAssociated (IsLocalRing.residue (AtMaximal R m))
      (algebraMap R (AtMaximal R m) a) (algebraMap R (AtMaximal R m) b)) :
    ∃ v : (AtMaximal R m)ˣ,
      toFraction K m (v : AtMaximal R m) = algebraMap R K a / algebraMap R K b ∧
      IsLocalRing.residue (AtMaximal R m) (v : AtMaximal R m) = 1 := by
…

Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated, OAI.CirculantHadamard.AlternatingLocalization.AtMaximal, OAI.CirculantHadamard.AlternatingLocalization.toFraction

theorem OAI.CirculantHadamard.AlternatingLocalization.natCast_isUnit_of_primeFactors line 191
Source documentation
A finite prime factorization supplies the away-from-u unit, including u=1.
```
theorem natCast_isUnit_of_primeFactors {R : Type uR} [CommRing R]
    (u : ℕ) (hu : u ≠ 0) (hprime : ∀ p ∈ u.primeFactors, IsUnit (p : R)) :
    IsUnit (u : R) := by
…
```
theorem OAI.CirculantHadamard.AlternatingLocalization.local_norm_factor_isUnit line 200
theorem OAI.CirculantHadamard.AlternatingLocalization.exists_unit_of_edges line 218
theorem OAI.CirculantHadamard.AlternatingLocalization.exists_unit_of_factor_units line 250
Source documentation
Ordinary local units give an actual local unit representative of the fixed field product. The representatives are not independently chosen field values.
```
theorem exists_unit_of_factor_units (f : R →+* K) (t : Finset I)
    (x : Finset I → R) (hx : ∀ S ⊆ t, IsUnit (x S)) :
    ∃ v : Rˣ, f (v : R) = alternatingProduct t (fun S => f (x S)) := by
…
```
Mentions: OAI.CirculantHadamard.alternatingProduct

theorem OAI.CirculantHadamard.AlternatingLocalization.exists_local_unit_away line 276

Source documentation

The away-from-u case uses only the evaluated norm identity and avoidance of the actual rational prime factors of u.

theorem exists_local_unit_away (m : MaximalSpectrum R) (u : ℕ) (hu : u ≠ 0)
    (t : Finset I) (x y : Finset I → R)
    (hnorm : ∀ S ⊆ t, x S * y S = (u : R) ^ 2)
    (havoid : ∀ p ∈ u.primeFactors, (p : R) ∉ m.asIdeal) :
    ∃ v : (AtMaximal R m)ˣ,
      toFraction K m (v : AtMaximal R m) =
        alternatingProduct t (fun S => algebraMap R K (x S)) := by
…

Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal, OAI.CirculantHadamard.AlternatingLocalization.toFraction, OAI.CirculantHadamard.alternatingProduct

theorem OAI.CirculantHadamard.AlternatingLocalization.exists_base_of_edges_and_norm line 294

Source documentation

Every maximal ideal is covered either by a genuine prime-direction edge comparison or by the norm argument. Local character comparison supplies the edge hypotheses, without assuming that the product belongs to the base ring.

theorem exists_base_of_edges_and_norm (u : ℕ) (hu : u ≠ 0)
    (t : Finset I) (prime : I → ℕ)
    (hcover : ∀ p ∈ u.primeFactors, ∃ i ∈ t, prime i = p)
    (x y : Finset I → R) (hnorm : ∀ S ⊆ t, x S * y S = (u : R) ^ 2)
    (hedge : ∀ m : MaximalSpectrum R, ∀ i ∈ t, (prime i : R) ∈ m.asIdeal →
      ∀ S ∈ (t.erase i).powerset, ∃ v : (AtMaximal R m)ˣ,
        toFraction K m (v : AtMaximal R m) =
          algebraMap R K (x (insert i S)) / algebraMap R K (x S) ∧
        IsLocalRing.residue (AtMaximal R m) (v : AtMaximal R m) = 1) :
    ∃ b : R, algebraMap R K b =
      alternatingProduct t (fun S => algebraMap R K (x S)) := by
…

Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal, OAI.CirculantHadamard.AlternatingLocalization.toFraction, OAI.CirculantHadamard.alternatingProduct

theorem OAI.CirculantHadamard.AlternatingLocalization.coprime_natCast_isUnit line 330
Source documentation
Bezout makes the complementary integer factor a unit in the actual localization at any prime containing p.
```
theorem coprime_natCast_isUnit {R : Type uR} [CommRing R]
    (I : Ideal R) [I.IsPrime] (p c : ℕ) (hpc : Nat.Coprime p c)
    (hpI : (p : R) ∈ I) : IsUnit (c : Localization.AtPrime I) := by
…
```

theorem OAI.CirculantHadamard.AlternatingLocalization.actual_local_character_association line 348

Source documentation

Apply the proved DVR comparison after coefficient localization and map its actual unit through the cyclotomic quotient into the target maximal localization. The group order and scalar prime exponent are the same p ^ (e + 1).

theorem actual_local_character_association
    (f : A₀ →+* R) (m : MaximalSpectrum R)
    [IsDomain (AtComap f m)] [CharZero (AtComap f m)]
    [IsDiscreteValuationRing (AtComap f m)]
    (p : ℕ) [NeZero p] (hp : p.Prime) (hpm : (p : R) ∈ m.asIdeal)
    (hmax : IsLocalRing.maximalIdeal (AtComap f m) =
      Ideal.span {(p : AtComap f m)})
    (rho : R) (hrho : rho ^ p = 1)
    (hroot : (Polynomial.cyclotomic p R).eval rho = 0)
    (n e c : ℕ) [NeZero n] (hn : n = p ^ (e + 1))
    (hrhon : rho ^ n = 1) (hc : IsUnit (c : AtComap f m))
    (F K : Elem A₀ n)
…

Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtComap

instance OAI.CirculantHadamard.AlternatingLocalization.B_local_algebra line 446
Source documentation
Name the canonical algebra structures directly to avoid searching through iterated-localization algebra instances for the concrete coefficient ring.
```
instance B_local_algebra (u : ℕ) (m : MaximalSpectrum (B u)) :
    Algebra (B u) (AtMaximal (B u) m) :=
…
```
Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal
instance OAI.CirculantHadamard.AlternatingLocalization.B_fraction_algebra line 450
theorem OAI.CirculantHadamard.AlternatingLocalization.rhoB_cyclotomic_root line 454
Source documentation
The selected element of B satisfies the actual cyclotomic relation.
```
theorem rhoB_cyclotomic_root (u : ℕ) (p : PrimeIndex u) :
    (Polynomial.cyclotomic p.val (B u)).eval (rhoB u p) = 0 := by
…
```
theorem OAI.CirculantHadamard.AlternatingLocalization.subset_evaluations_local_associated line 466

theorem OAI.CirculantHadamard.AlternatingLocalization.exists_local_edge_unit line 516

Source documentation

The denominator is nonzero because it is an actual evaluated norm factor.

theorem exists_local_edge_unit (u : ℕ) [NeZero (u ^ 2)]
    (hu : 0 < u) (huodd : Odd u)
    (x : Elem GaussianRing (u ^ 2))
    (hx : x * ringStar x = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
    (p : PrimeIndex u) (m : MaximalSpectrum (B u))
    (hpm : (p.val : B u) ∈ m.asIdeal)
    (S : Finset (PrimeIndex u)) (hpS : p ∉ S) :
    ∃ v : (AtMaximal (B u) m)ˣ,
      toFraction (FractionRing (B u)) m (v : AtMaximal (B u) m) =
        algebraMap (B u) (FractionRing (B u)) (subsetEvaluation u hu (insert p S) x) /
          algebraMap (B u) (FractionRing (B u)) (subsetEvaluation u hu S x) ∧
      IsLocalRing.residue (AtMaximal (B u) m) (v : AtMaximal (B u) m) = 1 := by
…

Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal, OAI.CirculantHadamard.AlternatingLocalization.toFraction

theorem OAI.CirculantHadamard.AlternatingLocalization.exists_local_unit_alternatingProduct line 537

Source documentation

At every maximal ideal over p, the one fixed global alternating product is the image of a unit with residue one. No edge comparison is an input.

theorem exists_local_unit_alternatingProduct (u : ℕ) [NeZero (u ^ 2)]
    (hu : 0 < u) (huodd : Odd u)
    (x : Elem GaussianRing (u ^ 2))
    (hx : x * ringStar x = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
    (p : PrimeIndex u) (m : MaximalSpectrum (B u))
    (hpm : (p.val : B u) ∈ m.asIdeal) :
    ∃ v : (AtMaximal (B u) m)ˣ,
      toFraction (FractionRing (B u)) m (v : AtMaximal (B u) m) =
        alternatingProduct (Finset.univ : Finset (PrimeIndex u))
          (fun S => algebraMap (B u) (FractionRing (B u)) (subsetEvaluation u hu S x)) ∧
      IsLocalRing.residue (AtMaximal (B u) m) (v : AtMaximal (B u) m) = 1 := by
…

Mentions: OAI.CirculantHadamard.AlternatingLocalization.AtMaximal, OAI.CirculantHadamard.AlternatingLocalization.toFraction, OAI.CirculantHadamard.alternatingProduct

theorem OAI.CirculantHadamard.AlternatingLocalization.exists_integral_alternatingProduct line 559

Source documentation

Integrality of the actual subset-character alternating product. The maximal ideals over prime divisors use the proved local comparison; every other maximal ideal uses the actual norm identity.

theorem exists_integral_alternatingProduct (u : ℕ) [NeZero (u ^ 2)]
    (hu : 0 < u) (huodd : Odd u)
    (x : Elem GaussianRing (u ^ 2))
    (hx : x * ringStar x = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing)) :
    ∃ z : B u, algebraMap (B u) (FractionRing (B u)) z =
      alternatingProduct (Finset.univ : Finset (PrimeIndex u))
        (fun S => algebraMap (B u) (FractionRing (B u)) (subsetEvaluation u hu S x)) := by
…

Mentions: OAI.CirculantHadamard.alternatingProduct