English
Under separability and splitting hypotheses, a counting formula relates the number of F-algebra embeddings from generated fields to the finrank of certain intermediate fields within a splitting field.
Русский
При условии разложимости и распада выполняется счетная формула, связывающая число вложений по F между образующими полями и размером соответствующих средних полей внутри разворачивающего поля.
LaTeX
$$$\text{IsGalois}.of\_separable\_splitting\_field\_aux \ldots$$$
Lean4
theorem of_separable_splitting_field_aux [hFE : FiniteDimensional F E] [sp : p.IsSplittingField F E] (hp : p.Separable)
(K : Type*) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E] {x : E} (hx : x ∈ p.aroots E) :
Nat.card (K⟮x⟯.restrictScalars F →ₐ[F] E) = Nat.card (K →ₐ[F] E) * finrank K K⟮x⟯ :=
by
have h : IsIntegral K x := (isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) x).tower_top
have h1 : p ≠ 0 := fun hp => by
rw [hp, Polynomial.aroots_zero] at hx
exact Multiset.notMem_zero x hx
have h2 : minpoly K x ∣ p.map (algebraMap F K) := by
apply minpoly.dvd
rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ← IsScalarTower.algebraMap_eq]
exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx
let key_equiv : (K⟮x⟯.restrictScalars F →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, @AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f) :=
by
change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _
exact algHomEquivSigma
haveI : ∀ f : K →ₐ[F] E, Finite (@AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f)) := fun f =>
by
have := Finite.of_equiv _ key_equiv
apply Finite.of_injective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2
have : FiniteDimensional F K := FiniteDimensional.left F K E
rw [Nat.card_congr key_equiv, Nat.card_sigma, IntermediateField.adjoin.finrank h, Nat.card_eq_fintype_card]
apply Finset.sum_const_nat
intro f _
rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) h]
· exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2
· refine Polynomial.splits_of_splits_of_dvd _ (Polynomial.map_ne_zero h1) ?_ h2
rw [Polynomial.splits_map_iff, ← IsScalarTower.algebraMap_eq]
exact sp.splits
