norm_eq_prod_embeddings_gen — Mathlib

English

Let pb be a power basis of L over R. If the minimal polynomial of pb.gen splits in F and pb.gen is separable over R, then the R→F image of the norm of pb.gen equals the product over all R-embeddings σ: L → F of σ(pb.gen).

Русский

Пусть pb задаёт базис силой мощности L над R. Если minpoly_R(pb.gen) распадается в F и pb.gen разделим над R, тогда образ нормы pb.gen через algebraMap_R^F равен произведению σ(pb.gen) по всем R-встраиваниям σ: L → F.

LaTeX

$$$ (\\operatorname{algebraMap} \\, R \\, F)(\\operatorname{norm} \\, R \\, pb.gen) = \\prod_{\\sigma \\in (L \\to_{R} F)} {\\sigma(pb.gen)} $$$

Lean4

theorem norm_eq_prod_embeddings_gen [Algebra R F] (pb : PowerBasis R S)
    (hE : (minpoly R pb.gen).Splits (algebraMap R F)) (hfx : IsSeparable R pb.gen) :
    algebraMap R F (norm R pb.gen) = (@Finset.univ _ (PowerBasis.AlgHom.fintype pb)).prod fun σ => σ pb.gen :=
  by
  letI := Classical.decEq F
  rw [PowerBasis.norm_gen_eq_prod_roots pb hE]
  rw [@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv' (fun σ => σ pb.gen)
      (fun x => x) ?_]
  · rw [Finset.prod_mem_multiset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr,
      Multiset.map_id]
    · exact nodup_roots (.map hfx)
    · intro x; rfl
  · intro σ; simp only [PowerBasis.liftEquiv'_apply_coe]

Похожие утверждения