English
If C is cyclotomic over B and B is cyclotomic over A, then C is cyclotomic over A provided the algebra map B → C is injective.
Русский
Если C циклотомическое над B, а B циклотомическое над A, то C циклотомическое над A при условии инъективности отображения B → C.
LaTeX
$$If hS: IsCyclotomicExtension S A B and hT: IsCyclotomicExtension T B C and inj: Injective(algebraMap B C), then IsCyclotomicExtension (S ∪ T) A C$$
Lean4
/-- Transitivity of cyclotomic extensions. -/
theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
[hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C] (h : Function.Injective (algebraMap B C)) :
IsCyclotomicExtension (S ∪ T) A C := by
refine ⟨fun hn => ?_, fun x => ?_⟩
· intro hn'
rcases hn with hn | hn
· obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'
refine ⟨algebraMap B C b, ?_⟩
exact hb.map_of_injective h
· exact ((isCyclotomicExtension_iff _ _ _).1 hT).1 hn hn'
· refine
adjoin_induction (hx := ((isCyclotomicExtension_iff T B _).1 hT).2 x)
(fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => ?_)
(fun x y _ _ hx hy => Subalgebra.add_mem _ hx hy) fun x y _ _ hx hy => Subalgebra.mul_mem _ hx hy
let f := IsScalarTower.toAlgHom A B C
have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}).map f :=
⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩
rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb
refine adjoin_mono (fun y hy => ?_) hb
obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy
exact ⟨n, ⟨mem_union_left T hn.1, hn.2.1, by rw [← h₁, ← map_pow, hn.2.2, map_one]⟩⟩
