English
Union_right variation: if (S ∪ T) is cyclotomic over A to B, then T yields a cyclotomic extension of adjoin A {b: B | ∃ a ∈ S, a ≠ 0 ∧ b^a = 1} over B.
Русский
Обобщение по сложению: если (S ∪ T) циклотомическое над A в B, то T образует циклотомическое расширение над B, адъянтированный через множества корней единицы.
LaTeX
$$IsCyclotomicExtension (S ∪ T) A B ⇒ IsCyclotomicExtension T (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b^a = 1}) B$$
Lean4
/-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B`
is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 }` given by
roots of unity of order in `T`. -/
theorem union_right [h : IsCyclotomicExtension (S ∪ T) A B] :
IsCyclotomicExtension T (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}) B :=
by
have :
{b : B | ∃ n : ℕ, n ∈ S ∪ T ∧ n ≠ 0 ∧ b ^ n = 1} =
{b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n : ℕ, n ∈ T ∧ n ≠ 0 ∧ b ^ n = 1} :=
by
refine le_antisymm ?_ ?_
· rintro x ⟨n, hn₁ | hn₂, hnpow⟩
· left; exact ⟨n, hn₁, hnpow⟩
· right; exact ⟨n, hn₂, hnpow⟩
· rintro x (⟨n, hn⟩ | ⟨n, hn⟩)
· exact ⟨n, Or.inl hn.1, hn.2⟩
· exact ⟨n, Or.inr hn.1, hn.2⟩
refine ⟨fun hn => ((isCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => ?_⟩
replace h := ((isCyclotomicExtension_iff _ _ _).1 h).2 b
rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h
