English
If f and g are commuting endomorphisms and both semisimple, then f + g is semisimple.
Русский
Если f и g коммьютируют и оба семисемпсимальны, то f + g семисемпсим.
LaTeX
$$$ Commute(f,g) \land IsSemisimple(f) \land IsSemisimple(g) \Rightarrow IsSemisimple(f+g)$$$
Lean4
theorem of_mem_adjoin_pair {a : End K M} (ha : a ∈ Algebra.adjoin K { f, g }) : a.IsSemisimple :=
by
let R := K[X] ⧸ Ideal.span {minpoly K f}
let S := AdjoinRoot ((minpoly K g).map <| algebraMap K R)
have : Module.Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| Algebra.IsIntegral.isIntegral f).finite
have : Module.Finite R S :=
(AdjoinRoot.powerBasis' <| (minpoly.monic <| Algebra.IsIntegral.isIntegral g).map _).finite
have : Module.Finite K S := .trans R S
have : IsArtinianRing R := .of_finite K R
have : IsReduced R :=
(Ideal.isRadical_iff_quotient_reduced _).mp <| span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
have : IsReduced S :=
by
simp_rw [S, AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]
exact (PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical
let φ : S →ₐ[K] End K M :=
Ideal.Quotient.liftₐ _ (eval₂AlgHom' (Ideal.Quotient.liftₐ _ (aeval f) fun a ↦ ?_) g ?_)
((Ideal.span_singleton_le_iff_mem _).mpr ?_ : _ ≤ RingHom.ker _)
rotate_left 1
· rw [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly]; exact id
· rintro ⟨p⟩;
exact
p.induction_on (fun k ↦ by simp [R, Algebra.commute_algebraMap_left])
(fun p q hp hq ↦ by simpa [R] using hp.add_left hq) fun n k ↦ by
simpa [R, pow_succ, ← mul_assoc _ _ X] using (·.mul_left comm)
· simpa only [RingHom.mem_ker, eval₂AlgHom'_apply, eval₂_map, AlgHom.comp_algebraMap_of_tower] using minpoly.aeval K g
have : Algebra.adjoin K { f, g } ≤ φ.range :=
Algebra.adjoin_le fun x ↦ by
rintro (hx | hx) <;> rw [hx]
· exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
· exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp (this ha)
refine
isSemisimple_of_squarefree_aeval_eq_zero ((minpoly.isRadical K p).squarefree <| minpoly.ne_zero <| .of_finite K p)
?_
rw [aeval_algHom, φ.comp_apply, minpoly.aeval, map_zero]
