Normalize polynomial

Stream: mathlib4

[Violeta Hernández]

As I understand it, there's two different spellings for "multiply a polynomial by the inverse of its leading coefficient, which are C p.leadingCoeff⁻¹ * p and normalize p. There's even lemmas written about both, such as docs#Polynomial.monic_mul_leadingCoeff_inv vs docs#Polynomial.monic_normalize.

[Violeta Hernández]

Is there any difference between these? If so, when should I prefer one over the other? If not, why have both?

[Ruben Van de Velde]

It seems that normalize p better captures the semantics, so unless it's weaker somehow, I'd standardize on that

[Violeta Hernández]

I notice monic_normalize requires a field while monic_mul_leadingCoeff_inv only requires a division ring

[Violeta Hernández]

In fact, normalize itself requires commutativity

[Ruben Van de Velde]

In that case, use the other one :)

[Kenny Lau]

in that case, change normalize

[Kenny Lau]

aha, we can't change that because it's actually a general normalize for NormalizationMonoid

[Kenny Lau]

in that case, maybe we should make Polynomial.normalize?

[Kenny Lau]

or... what if we changed NormalizationMonoid to not assume comm? I might be cooking here

[Violeta Hernández]

docs#NormalizationMonoid

[Kenny Lau]

import Mathlib

variable {α : Type*}

/-- Normalization monoid: multiplying with `normUnit` gives a normal form for associated
elements. -/
class NormalizationMonoid' (α : Type*) [CancelMonoidWithZero α] where
  /-- `normUnit` assigns to each element of the monoid a unit of the monoid. -/
  normUnit : α → αˣ
  /-- The proposition that `normUnit` maps `0` to the identity. -/
  normUnit_zero : normUnit 0 = 1
  /-- The proposition that `normUnit` respects multiplication of non-zero elements. -/
  normUnit_mul : ∀ {a b}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit b * normUnit a
  /-- The proposition that `normUnit` maps units to their inverses. -/
  normUnit_coe_units : ∀ u : αˣ, normUnit u = u⁻¹

namespace NormalizationMonoid'
attribute [simp] normUnit_zero normUnit_mul normUnit_coe_units
end NormalizationMonoid'

namespace Polynomial

open NormalizationMonoid'

noncomputable instance [Ring α] [IsDomain α] [NormalizationMonoid' α] :
    NormalizationMonoid' (Polynomial α) where
  normUnit p :=
    ⟨C ↑(normUnit p.leadingCoeff), C ↑(normUnit p.leadingCoeff)⁻¹, by
      rw [← RingHom.map_mul, Units.mul_inv, C_1], by rw [← RingHom.map_mul, Units.inv_mul, C_1]⟩
  normUnit_zero := Units.ext (by simp)
  normUnit_mul hp0 hq0 :=
    Units.ext
      (by
        dsimp
        rw [Ne, ← leadingCoeff_eq_zero] at *
        rw [leadingCoeff_mul, normUnit_mul hp0 hq0, Units.val_mul, C_mul])
  normUnit_coe_units u :=
    Units.ext
      (by
        dsimp
        rw [← mul_one u⁻¹, Units.val_mul, Units.eq_inv_mul_iff_mul_eq]
        rcases Polynomial.isUnit_iff.1 ⟨u, rfl⟩ with ⟨_, ⟨w, rfl⟩, h2⟩
        rw [← h2, leadingCoeff_C, NormalizationMonoid'.normUnit_coe_units,
          ← C_mul, Units.mul_inv, C_1]
        rfl)

end Polynomial

[Kenny Lau]

@Violeta Hernández this seems to work fine

[Violeta Hernández]

Kenny Lau said:

or... what if we changed NormalizationMonoid to not assume comm? I might be cooking here

You're right, I don't see a reason for it to require commutativity. For any division ring you should be able to define an instance by sending a nonzero element to its inverse.

[Violeta Hernández]

Nerd-sniped

[Kenny Lau]

XD

[Kenny Lau]

(just remember to change a*b to b*a as i did above)

[Violeta Hernández]

Well, I think there's now two proposed PRs:

• generalize NormalizationMonoid to the noncomm case
• use normalize pfor polynomials instead of the explicit form throughout

[Violeta Hernández]

I could try a) tomorrow, though maybe you want to get ahead of me.

[Kenny Lau]

i'll leave that to you

[Kenny Lau]

and 3rd PR: prove that every division ring is a normalization monoid

[Kenny Lau]

or actually, group with zero?