Introduction: Allen Knutson

Stream: new members

[Allen Knutson]

Hello everyone. I am learning about Lean and hoping to direct a couple of undergraduates to formalize some of the basics of Schubert polynomials in Lean. First up is dealing with the polynomial ring Z[x_1,x_2,...] and the division algorithm. Another short-term goal is Tits' theorem in type A, that any two minimal ways to write a permutation as a product of simple transpositions can be related by commuting and braid moves.

[Eric Wieser]

#3770 looks like it might be somewhat related to Tits' theorem

[Kevin Buzzard]

We have the polynomial ring: assuming you mean $\Z[x_1, x_2, \ldots]$ it's mv_polynomial ℕ ℤ (import data.mv_polynomial.basic), although the naturals start at 0 around here (blame the computer scientists). What's "the division algorithm"?

[Allen Knutson]

What I had meant by it was the proof that $k[x]$ is a Euclidean domain for k a field (exhibit the actual quotient with remainder). But I actually want to divide by $x_i - x_{i+1}$ in $\mathbb Z[x_1,\ldots,\widehat{x_i},\ldots][x_i]$ while noting that the coefficient on $x_i$ is invertible in that coefficient ring. Anyway I think I've found a way around dealing with any of that, involving proofs that are less edifying for humans but good enough for computers.

[Allen Knutson]

(deleted)

[Allen Knutson]

(deleted)

[Kevin Buzzard]

Mathlib has division of polynomials by monic polynomials (quotient and remainder), and the ability to pull out one variable and consider the multivariable ring as a polynomial ring over (the multivariable ring in the rest).

import data.polynomial.div -- division
import data.mv_polynomial.equiv
-- Let R be a commutative ring and let q ∈ R[X] be a polynomial (soon assumed to be monic)
variables (R : Type) [comm_ring R] (q : polynomial R)

-- Let p ∈ R[X] be a polynomial
variable (p : polynomial R)

open polynomial -- because I can't be bothered to write `polynomial.mod_by_monic_add_div`

-- division
#check p /ₘ q -- polynomial R

-- remainder
#check p %ₘ q -- polynomial R

-- Both return junk if `q` isn't monic

-- remainder has degree less than q, if R isn't the zero ring and q is monic
example [nontrivial R] (hq : q.monic) : degree (p %ₘ q) < degree q :=
begin
  exact degree_mod_by_monic_lt p hq
end


-- quotient divisibility theorem
example (hq : q.monic) : p %ₘ q + q * (p /ₘ q) = p :=
begin
  exact mod_by_monic_add_div p hq
end

-- If `T` is a type, let `R[T]` denote the ring of multivariable
-- polynomials with coefficients indexed by `T`. Exception: `R[X]`
-- means polynomial in one variable

-- `option S` is the type containing `S` and one extra element

-- `R[option S]` is isomorphic as R-algebra to `(R[S])[X]`
noncomputable example (S : Type) :
  mv_polynomial (option S) R ≃ₐ[R] polynomial (mv_polynomial S R) :=
mv_polynomial.option_equiv_left R S

-- A bijection `S ≃ T` induces an R-algebra isomorphism R[S] ≃ₐ[R] R[T]
noncomputable example (S T : Type) (e : S ≃ T) :
  mv_polynomial S R ≃ₐ[R] mv_polynomial T R :=
mv_polynomial.rename_equiv R e

-- `option (ℕ \ {i})` bijects with `ℕ` in the obvious way
example (i : ℕ) : option ({n : ℕ // n ≠ i}) ≃ ℕ :=
{ to_fun := λ x, option.rec_on x i (λ s, s.1),
  inv_fun := λ n, if h : n = i then none else some ⟨n, h⟩,
  left_inv := λ x, begin
    rcases x with _ | ⟨n, hn⟩,
    { simp, },
    { simp [hn], },
  end,
  -- this code is not good
  right_inv := λ n, begin
    by_cases h : n = i,
    { dsimp,
      rw dif_pos h,
      simp [h] },
    { dsimp,
      rw [dif_neg h] },
  end }

[Yury G. Kudryashov]

BTW, sometimes it is useful to divide by a polynomial with an invertible leading coefficient without dividing the denominator by this coefficient first (e.g., in the proof of Sturm's theorem). Probably, we should either add a new function or generalize divide_by_monic.

[Allen Knutson]

That's all pretty great, thanks a lot! Now I'm not sure which proof to use! :smile:

[Allen Knutson]

I looked for emacs support for Lean and found support for Lean 4. Am I right in thinking that if my interest is in MathLib, then I don't want to install that? Is there emacs support for Lean 3?

[Johan Commelin]

Yes, there's quite a number of people using Lean 3 + emacs.

[Johan Commelin]

Does https://github.com/leanprover/lean-mode help?

[Allen Knutson]

"This is the Emacs mode for the Lean 3 theorem prover." Ah perfect, thanks very much.