instAdjoinRootOfIrreduciblePolynomialOfFactMonic

English

For an irreducible monic polynomial p over F, the differential structure can be extended to the adjoining root AdjoinRoot(p).

Русский

Для ирреducible, монической полиномиальной p над F можно наAdjoinRoot(p) определить дифференциал так, чтобы образовывал дифференциальную алгебру.

LaTeX

$$$\\operatorname{Differential}(\\operatorname{AdjoinRoot}(p))$$$

Lean4

noncomputable instance (p : F[X]) [Fact (Irreducible p)] [Fact p.Monic] : Differential (AdjoinRoot p) where
  deriv :=
    Derivation.liftOfSurjective (f := (AdjoinRoot.mk p).toIntAlgHom) AdjoinRoot.mk_surjective (d :=
      implicitDeriv <|
        AdjoinRoot.modByMonicHom Fact.out <|
          -(aeval (AdjoinRoot.root p) (mapCoeffs p)) / (aeval (AdjoinRoot.root p) (derivative p)))
      (by
        rintro x hx
        simp_all only [RingHom.toIntAlgHom_apply, AdjoinRoot.mk_eq_zero]
        obtain ⟨q, rfl⟩ := hx
        simp only [Derivation.leibniz, smul_eq_mul]
        apply dvd_add (dvd_mul_right ..)
        apply dvd_mul_of_dvd_right
        rw [← AdjoinRoot.mk_eq_zero]
        unfold implicitDeriv
        simp only [AdjoinRoot.aeval_eq, Derivation.coe_add, Derivation.coe_smul, Pi.add_apply, Pi.smul_apply,
          Derivation.restrictScalars_apply, derivative'_apply, smul_eq_mul, map_add, map_mul,
          AdjoinRoot.mk_leftInverse Fact.out _]
        rw [div_mul_cancel₀, add_neg_cancel]
        simp only [ne_eq, AdjoinRoot.mk_eq_zero]
        have : 0 < p.natDegree := Irreducible.natDegree_pos (Fact.out)
        apply not_dvd_of_natDegree_lt
        · intro nh
          simp [natDegree_eq_zero_of_derivative_eq_zero nh] at this
        apply natDegree_derivative_lt
        exact Nat.ne_zero_of_lt this)

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