English
Let f, g be monic over K. If f is irreducible and g(x) − α is irreducible in K⟮α⟯ for α a root of f, then f(g(x)) is irreducible.
Русский
Пусть f, g — монические над K. Если f неприводим и g(x) − α неприводим в K⟮α⟯ при α, являющемся корнем f, то f(g(x)) неприводим.
LaTeX
$$Irreducible (f.comp g) under the stated hypotheses$$
Lean4
/-- Let `f, g` be monic polynomials over `K`. If `f` is irreducible, and `g(x) - α` is irreducible
in `K⟮α⟯` with `α` a root of `f`, then `f(g(x))` is irreducible. -/
theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g.Monic) (hf : Irreducible f)
(hg :
∀ (E : Type u) [Field E] [Algebra K E] (x : E) (_ : minpoly K x = f),
Irreducible (g.map (algebraMap _ _) - C (AdjoinSimple.gen K x))) :
Irreducible (f.comp g) :=
by
have hf' : natDegree f ≠ 0 := fun e ↦ not_irreducible_C (f.coeff 0) (eq_C_of_natDegree_eq_zero e ▸ hf)
have hg' : natDegree g ≠ 0 := by
have := Fact.mk hf
intro e
apply
not_irreducible_C
((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))
-- Needed to specialize `map_sub` to avoid a timeout https://github.com/leanprover-community/mathlib4/pull/8386
rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
apply hg (AdjoinRoot f)
rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
have H₁ : f.comp g ≠ 0 := fun h ↦ by simpa [hf', hg', natDegree_comp] using congr_arg natDegree h
have H₂ : ¬IsUnit (f.comp g) := fun h ↦ by simpa [hf', hg', natDegree_comp] using natDegree_eq_zero_of_isUnit h
have ⟨p, hp₁, hp₂⟩ := WfDvdMonoid.exists_irreducible_factor H₂ H₁
suffices natDegree p = natDegree f * natDegree g from
(associated_of_dvd_of_natDegree_le hp₂ H₁ (this.trans natDegree_comp.symm).ge).irreducible hp₁
have := Fact.mk hp₁
let Kx := AdjoinRoot p
letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finite
have key₁ : f = minpoly K (aeval (root p) g) :=
by
refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
rw [← aeval_comp]
exact aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)
have key₁' : finrank K K⟮aeval (root p) g⟯ = natDegree f :=
by
rw [adjoin.finrank, ← key₁]
exact IsIntegral.of_finite _ _
have key₂ :
g.map (algebraMap _ _) - C (AdjoinSimple.gen K (aeval (root p) g)) = minpoly K⟮aeval (root p) g⟯ (root p) :=
minpoly.eq_of_irreducible_of_monic (hg _ _ key₁.symm) (by simp [AdjoinSimple.gen])
(Monic.sub_of_left (hgm.map _) (degree_lt_degree (by simpa [Nat.pos_iff_ne_zero] using hg')))
have key₂' : finrank K⟮aeval (root p) g⟯ Kx = natDegree g :=
by
trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
· have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ :=
by
apply restrictScalars_injective K
rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left, adjoin_root_eq_top p,
restrictScalars_adjoin]
simp
rw [← finrank_top', ← this, adjoin.finrank]
exact IsIntegral.of_finite _ _
· simp [← key₂]
have := Module.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx
rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
