English
Let ζ1 and ζ2 be primitive roots of unity of orders k1 and k2, respectively, and let ζ be a primitive root of order lcm(k1,k2). Then the smallest subalgebra of R containing ζ1 and ζ2 is the same as the one containing ζ.
Русский
Пусть ζ1 и ζ2 — примитивные корни единицы порядка k1 и k2, соответственно, и ζ — примитивный корень порядка lcm(k1,k2). Тогда малейшее подалгебраическое замыкание, содержащее ζ1 и ζ2, совпадает с замыканием, содержащее ζ.
LaTeX
$$$\\operatorname{Algebra.adjoin} S\\{\\zeta_1,\\zeta_2\\} = \\operatorname{Algebra.adjoin} S\\{\\zeta\\}$$$
Lean4
/-- The sub-algebra generated by two roots of unity of order `k₁` and `k₂` resp. is the same as the one
generated by a root of unity of order `lcm k₁ k₂`.
See `IsPrimitiveRoot.pow_mul_pow_lcm` for how to construct a root of unity of order `lcm k₁ k₂`
from roots of unity of order `k₁` and `k₂`.
-/
theorem adjoin_pair_eq (S : Type*) [CommSemiring S] [Algebra S R] {ζ₁ ζ₂ : R} {k₁ : ℕ} {k₂ : ℕ}
(hζ₁ : IsPrimitiveRoot ζ₁ k₁) (hζ₂ : IsPrimitiveRoot ζ₂ k₂) (hk₁ : k₁ ≠ 0) (hk₂ : k₂ ≠ 0) {ζ : R}
(hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)) : Algebra.adjoin S { ζ₁, ζ₂ } = Algebra.adjoin S { ζ } :=
by
have : NeZero (k₁.lcm k₂) := ⟨Nat.lcm_ne_zero hk₁ hk₂⟩
refine le_antisymm (Algebra.adjoin_le ?_) (Algebra.adjoin_le ?_)
· refine Set.pair_subset_iff.mpr ⟨?_, ?_⟩
· obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <| (hζ₁.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_left k₂
exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _
· obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <| (hζ₂.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_right k₂
exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _
· have hζ' := IsPrimitiveRoot.pow_mul_pow_lcm hζ₁ hζ₂ hk₁ hk₂
obtain ⟨_, _, rfl⟩ := hζ'.eq_pow_of_pow_eq_one hζ.pow_eq_one
aesop
