Determinant of adjugate matrix

Stream: maths

[Eric Wieser]

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]

There's a trick to proving this, where you consider the 'generic $n \times n$-matrix' with coefficients in the polynomial ring over $\mathbb Z$ in $n^2$ variables. Its determinant is non-zero, hence cancellable, so the mathlib lemma applies. Now any $n \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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

Or possibly

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

[David Wärn]

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]

Will be back shortly with a few sorries...

[Eric Wieser]

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]

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

[Eric Wieser]

Which frankly feels almost as hard as the original

[Reid Barton]

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

[Eric Wieser]

Got it, thanks; edited above

[Eric Wieser]

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]

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]

Darij Grinberg has great notes on these sorts of proofs.

[Kevin Buzzard]

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]

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]

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]

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