Zulip Chat Archive

Stream: maths

Topic: Determinant of adjugate matrix


Eric Wieser (Oct 25 2021 at 08:57):

I'd like to show that (adjugate A).det = A.det ^ (fintype.card n - 1). Right now we only have docs#matrix.det_adjugate_of_cancel, but this assumes cancellation is possible which seems unnecessary as both sides of the statement are just sums of products.

Am I correct in assuming this is true without that assumption? I was hoping the lemmas in #9947 would help with showing this, but I can't think of a proof strategy that doesn't involve unfolding matrix.det and doing some painful sum manipulation.

David Wärn (Oct 25 2021 at 09:08):

There's a trick to proving this, where you consider the 'generic n×nn \times n-matrix' with coefficients in the polynomial ring over Z\mathbb Z in n2n^2 variables. Its determinant is non-zero, hence cancellable, so the mathlib lemma applies. Now any n×nn \times n-matrix over any ring is the image of this generic matrix under some ring hom, so by some naturality lemmas the theorem holds for any matrix.

Eric Wieser (Oct 25 2021 at 09:10):

That's a formal approach to my "both sides of the statement are just sums of products." hand-wave, right?

Eric Wieser (Oct 25 2021 at 09:14):

Unfortunately mv_polynomial isn't available to import yet where I want to generalize this lemma

Eric Wieser (Oct 25 2021 at 09:15):

But I assume you mean something like showing ∃ (A' : matrix n n (mv_polynomial ℤ (n × n))) (f : mv_polynomial ℤ (n × n) →+* α), A = A'.map f

Eric Wieser (Oct 25 2021 at 09:17):

Or possibly

 (f : mv_polynomial  (n × n) →+* α), A = ((prod.mk : matrix n n (n × n)).map X).map f

David Wärn (Oct 25 2021 at 09:24):

That looks about right. You'd need to know that A'.det is nonzero, and that the polynomial ring is an integral domain. And you could write down the ring hom f explicitly (it maps the variables to entries of A)

Eric Wieser (Oct 25 2021 at 09:33):

Will be back shortly with a few sorries...

Eric Wieser (Oct 25 2021 at 09:43):

lemma det_adjugate' {A : matrix n n α} :
  (adjugate A).det = A.det ^ (fintype.card n - 1) :=
begin
  -- get rid of the `- 1`
  cases h_card : fintype.card n,
  { haveI : is_empty n := fintype.card_eq_zero_iff.mp h_card,
    rw [nat.zero_sub, pow_zero, adjugate_subsingleton, det_one] },
  rw h_card,

  -- express `A` as a polynomial in n^2 variables
  let A' := (matrix.map (prod.mk) (mv_polynomial.X : (n × n)  mv_polynomial _ )),
  have : A = ring_hom.map_matrix (mv_polynomial.aeval (λ p : n × n, A p.1 p.2)).to_ring_hom A',
  { ext i j,
    simp },
  rw [this, ring_hom.map_adjugate, ring_hom.map_det, ring_hom.map_det, ring_hom.map_pow],
  congr' 1,

  apply det_adjugate_of_cancel,
  rw [h_card, nat.succ_sub_succ_eq_sub, nat.sub_zero, pow_succ],
  intros b hb,
  apply mul_left_cancel₀ _ hb,
  show (map prod.mk mv_polynomial.X).det  0,
  sorry
end

(below docs#ring_hom.map_adjugate)

Eric Wieser (Oct 25 2021 at 09:44):

So yes, "You'd need to know that A'.det is nonzero" is the missing piece

Eric Wieser (Oct 25 2021 at 09:53):

Which frankly feels almost as hard as the original

Reid Barton (Oct 25 2021 at 09:56):

A'.det has to be nonzero because otherwise, the determinant of every n x n matrix would be zero (same argument)

Eric Wieser (Oct 25 2021 at 10:23):

Got it, thanks; edited above

Eric Wieser (Oct 25 2021 at 10:24):

It's unfortunate that file#linear_algebra/matrix/nonsingular_inverse will now have to import file#ring_theory/polynomial/basic, but I guess that's better than not having the proof at all

Yakov Pechersky (Oct 25 2021 at 12:34):

I did a similar proof through the polynomial matrix ring for the commutativity of the multiplication of adjugate (in a not necessarily commutative base ring) below in the file.

Yakov Pechersky (Oct 25 2021 at 12:35):

Darij Grinberg has great notes on these sorts of proofs.

Kevin Buzzard (Oct 25 2021 at 14:08):

They're a basic technique in algebraic geometry. To prove certain kinds of statements for all X, you only have to prove them for the universal X, and the universal X might have nice properties which a general X doesn't have. For example in algebraic geometry the universal X might be flat, or integral (which was what happened here).

Kevin Buzzard (Oct 25 2021 at 14:10):

An interesting example where this technique didn't work was Eric's question the other day about whether a and b non-invertible implied ab non-invertible in a not necessarily commutative ring. Then the universal example was a quotient of a non-commuting polynomial ring in two variables by some bi-ideal and seemed hard to work with; it was easier to give a more concrete counterexample.

Kevin Buzzard (Oct 25 2021 at 14:13):

An example where it does work well is in Johan and Rob's work on Witt vectors, where p was much better behaved in the universal object than it was in general

Eric Wieser (Oct 27 2021 at 10:33):

PR'd the above and a similar proof as #9991


Last updated: Dec 20 2023 at 11:08 UTC