FirstOrderResidue.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

First-order residues of principal units

For a nonzero element t of a domain, a unit of the form 1 + t * a has a unique coefficient a. A ring homomorphism killing t sends the coefficient of a product to the sum of the coefficients. This constructs the actual first-order homomorphism without identifying any quotient rings.

def OAI.CirculantHadamard.principalUnits line 27
Source documentation
Units whose difference from one is a multiple of the specified element.
```
def principalUnits (t : O) : Subgroup Oˣ where
…
```
theorem OAI.CirculantHadamard.mem_principalUnits line 44
def OAI.CirculantHadamard.principalUnitCoeff line 50
Source documentation
The coefficient of a principal unit. Its uniqueness is proved separately using the domain assumption and t ≠ 0.
```
noncomputable def principalUnitCoeff (t : O) (u : principalUnits t) : O :=
…
```
Mentions: OAI.CirculantHadamard.principalUnits
theorem OAI.CirculantHadamard.principalUnitCoeff_spec line 53
theorem OAI.CirculantHadamard.principalUnitCoeff_eq line 61
theorem OAI.CirculantHadamard.principalUnitCoeff_mul line 67
def OAI.CirculantHadamard.actualFirstOrder line 81
Source documentation
The actual first-order homomorphism associated with a nonzero element killed by the given residue map. Multiplicative K uses addition in K.
```
noncomputable def actualFirstOrder (φ : O →+* K) (t : O) (ht : t ≠ 0)
    (hφt : φ t = 0) : principalUnits t →* Multiplicative K where
…
```
Mentions: OAI.CirculantHadamard.principalUnits
theorem OAI.CirculantHadamard.actualFirstOrder_apply_of_eq line 95

theorem OAI.CirculantHadamard.first_order_sum_eq_zero_of_prod_eq_one line 104

Source documentation

An exact signed product identity among principal units gives a vanishing sum of their first-order residues. Representations are required only on s.

theorem first_order_sum_eq_zero_of_prod_eq_one {ι : Type uIota}
    (φ : O →+* K) (t : O) (ht : t ≠ 0) (hφt : φ t = 0)
    (s : Finset ι) (u : ι → Oˣ) (L : ι → O) (ε : ι → ℤ)
    (hrep : ∀ i ∈ s, (u i : O) = 1 + t * L i)
    (hprod : (∏ i ∈ s, (u i) ^ (ε i)) = 1) :
    ∑ i ∈ s, (ε i : K) * φ (L i) = 0 := by
…