English
If S is finite and IsCyclotomicExtension S A B, then Module.Finite A B.
Русский
Если S конечное и IsCyclotomicExtension S A B, то B конечен над A.
LaTeX
$$$[Finite S] \\Rightarrow [IsCyclotomicExtension S A B] \\Rightarrow Module.Finite A B$$$
Lean4
/-- If `S` is finite and `IsCyclotomicExtension S A B`, then `B` is a finite `A`-algebra. -/
protected theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] : Module.Finite A B :=
by
rw [finite_coe_iff] at h₁
induction S, h₁ using Set.Finite.induction_on generalizing h₂ A B with
| empty =>
refine Module.finite_def.2 ⟨({ 1 } : Finset B), ?_⟩
simp [← top_toSubmodule, ← subsingleton_iff_bot_eq_top.mpr inferInstance, toSubmodule_bot, Submodule.one_eq_span]
| @insert n S _ _ H =>
by_cases hn : n = 0
· have : insert n S \ {0} = S \ {0} := by simp_all
rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂
exact H A B
have : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) :=
union_left _ (insert n S) _ _ (subset_insert n S)
have := H A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1})
have : Module.Finite (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) B :=
by
rw [← union_singleton] at h₂
let _ := union_right S { n } A B
have : NeZero n := ⟨hn⟩
exact finite_of_singleton n _ _
exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _
