discr_powerBasis_eq_norm — Mathlib

English

The discriminant of a power basis equals (−1)^{n(n−1)/2} times the norm from K to E of the derivative of the minimal polynomial evaluated at the generator.

Русский

Дискриминант базы степеней равен (−1)^{n(n−1)/2} умноженному на норму K/E от производной минимального многочлена, вычисленной в генераторе.

LaTeX

$$$$ \\mathrm{discr}\\,K(pb.basis) = (-1)^{\\frac{n(n-1)}{2}} \\cdot \\mathrm{norm}_K(\\mathrm{aeval}\\, pb.gen\\ (\\mathrm{minpoly}\\ K\\ pb.gen)'.\\text{derivative}) $$$$

Lean4

/-- Formula for the discriminant of a power basis using the norm of the field extension. -/
theorem discr_powerBasis_eq_norm [Algebra.IsSeparable K L] :
    discr K pb.basis = (-1) ^ (n * (n - 1) / 2) * norm K (aeval pb.gen (minpoly K pb.gen).derivative) :=
  by
  let E := AlgebraicClosure L
  letI := fun a b : E => Classical.propDecidable (Eq a b)
  have e : Fin pb.dim ≃ (L →ₐ[K] E) := by
    refine equivOfCardEq ?_
    rw [Fintype.card_fin, AlgHom.card]
    exact (PowerBasis.finrank pb).symm
  have hnodup : ((minpoly K pb.gen).aroots E).Nodup :=
    nodup_roots (Separable.map (Algebra.IsSeparable.isSeparable K pb.gen))
  have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ (minpoly K pb.gen).aroots E :=
    by
    intro σ
    rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply]
    repeat' simp [minpoly.ne_zero (Algebra.IsSeparable.isIntegral K pb.gen)]
  apply (algebraMap K E).injective
  rw [RingHom.map_mul, RingHom.map_pow, RingHom.map_neg, RingHom.map_one, discr_powerBasis_eq_prod'' _ _ _ e]
  congr
  rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag]
  conv_rhs =>
    congr
    rfl
    ext σ
    rw [← aeval_algHom_apply,
      aeval_root_derivative_of_splits (minpoly.monic (Algebra.IsSeparable.isIntegral K pb.gen))
        (IsAlgClosed.splits_codomain _) (hroots σ),
      ← Finset.prod_mk _ (hnodup.erase _)]
  rw [Finset.prod_sigma', Finset.prod_sigma']
  refine
      prod_bij' (fun i _ ↦ ⟨e i.2, e i.1 pb.gen⟩) (fun σ hσ ↦ ⟨e.symm (PowerBasis.lift pb σ.2 ?_), e.symm σ.1⟩) ?_ ?_ ?_
        ?_ (fun i _ ↦ by simp) <;>
    simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def, mem_roots', mem_singleton,
      true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply, PowerBasis.lift_gen, implies_true,
      Equiv.symm_apply_apply, Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *
  · simpa only [aeval_def, eval₂_eq_eval_map] using hσ.2.2
  · exact fun a b hba ↦ ⟨fun h ↦ hba <| e.injective <| pb.algHom_ext h.symm, hroots _⟩
  · rintro a b hba ha
    rw [ha, PowerBasis.lift_gen] at hba
    exact hba.1 rfl
  · exact fun a b _ ↦ pb.algHom_ext <| pb.lift_gen _ _

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