Units in cyclotomic fields

This file records how complex conjugation acts on cyclotomic units and proves that the quotient of a unit by its conjugate is a square of a root of unity.

theorem eq_one_mod_one_sub {A : Type u_2} [CommRing A] {t : A} : (algebraMap A (A ⧸ Ideal.span {t - 1})) t = 1

theorem complexConj_zeta {p : ℕ} [NeZero p] {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : 2 < p) : (NumberField.IsCMField.complexConj K) ζ = ζ⁻¹

Complex conjugation sends a primitive p-th root of unity to its inverse.

theorem roots_of_unity_in_cyclo {p : ℕ} [NeZero p] {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hpo : Odd p) (x : K) (h : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1) : ∃ (m : ℕ) (k : ℕ), x = (-1) ^ k * ↑↑⋯.unit ^ m

theorem unit_inv_conj_not_neg_zeta_runity_aux {p : ℕ} [NeZero p] {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (u : (NumberField.RingOfIntegers K)ˣ) [Fact (Nat.Prime p)] (hp : 2 < p) : (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers K ⧸ Ideal.span {↑⋯.unit - 1})) ↑↑((NumberField.IsCMField.unitsMulComplexConjInv K) u) = 1

theorem unit_inv_conj_not_neg_zeta_runity {p : ℕ} [NeZero p] {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (u : (NumberField.RingOfIntegers K)ˣ) (n : ℕ) [Fact (Nat.Prime p)] (hp : 2 < p) : u * ((NumberField.IsCMField.unitsComplexConj K) u)⁻¹ ≠ -⋯.unit ^ n

theorem unit_inv_conj_is_root_of_unity {p : ℕ} [NeZero p] {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [NumberField K] [IsCyclotomicExtension {p} ℚ K] (u : (NumberField.RingOfIntegers K)ˣ) [H : Fact (Nat.Prime p)] (hp : 2 < p) : ∃ (m : ℕ), u * ((NumberField.IsCMField.unitsComplexConj K) u)⁻¹ = (⋯.unit ^ m) ^ 2