determinant via exterior algebra

Stream: Is there code for X?

[Oliver Nash]

To my delight, I've just discovered that we have the exterior algebra. Do we have the connection with the determinant anywhere (even in a branch)?

[Eric Wieser]

What statement of the connection are you looking for?

[Oliver Nash]

Good question, that was a bit lazy of me!

[Eric Wieser]

We have that the determinant is an alternating map (docs#matrix.det_row_multilinear) and that so is the map from a set of vectors to an element of the exterior algebra (docs#exterior_algebra.ι_multi)

[Oliver Nash]

I suppose I'd like to know that for a finite-dimensional vector space, the endomorphism on the top exterior power induced by an endomorphism of the original vector space, is multiplication by a scalar which is the determinant.

[Eric Wieser]

I can't help feeling you need something about the basis of an exterior algebra or something about exterior powers (branch#koszul_cx) to proceed

[Eric Wieser]

Since there's no canonical top exterior power element of the algebra without a canonical ordered basis, right?

[Oliver Nash]

Yes

[Oliver Nash]

In maths language, if $V$ has dimension $n$ and $T : V → V$ then it induces a map $∧ⁿT : ∧ⁿV → ∧ⁿV$.

[Oliver Nash]

And since $∧ⁿV$ is one-dimensional, this map has to be multiplication by a scalar.

[Eric Wieser]

Yes, that's the statement I thought you were making :)

[Oliver Nash]

Anyway I'm not sure if I'll formalise what I need in this language even though it's how I really think about what I'm doing, and it's how I'd _like_ to formalise it. I'm still weighing my options but it's really great we have the exterior algebra, I do now remember but I had forgotten.

[Eric Wieser]

I think do to much we need to show that exterior_algebra R V is isomorphic to ⨁ i : fin n, (⋀[R] i, V) when findim V = n, and ⋀[R] is an exterior version of docs#pi_tensor_product

[Eric Wieser]

And then you can make your statement about ⋀[R] i, V

[Johan Commelin]

Does lean already know how to extract a scalar out of an endomorphism of a 1-dimensional vector space?

[Johan Commelin]

Ooh that's not what is needed. Ignore me.

[Johan Commelin]

We're not trying to define the determinant this way.

[Oliver Nash]

Eric Wieser said:

I think do to much we need to show that exterior_algebra R V is isomorphic to ⨁ i : fin n, (⋀[R] i, V) when findim V = n, and ⋀[R] is an exterior version of docs#pi_tensor_product

I see, thanks.

[Eric Wieser]

Note that exterior_power is in defined in a branch here: https://github.com/leanprover-community/mathlib/blob/koszul_cx/src/m4r/exterior_power.lean

[Eric Wieser]

That was defined before pi_tensor_product existed I think, so tensor_power probably should be changed to be pi_tensor_product over a uniform type

[Oliver Nash]

Thanks, that's helpful. I'm tempted to use my would-be application as an excuse to build out some missing pieces. In maths language, what I really want is the following construction of the dual basis.

[Oliver Nash]

Given $V$ of dim $n$, and $1 ≤ i ≤ n$, we can define $⊗^{n-1}V → Hom(V, ∧^n V)$ in an obvious way.

[Oliver Nash]

I guess the above is the invariant definition of the adjugate, and then dividing by the determinant, which lives in $∧^nV$ we get the element of the dual.

[Heather Macbeth]

I also have wished that we had that $\Lambda^n V$ (defined either via the exterior algebra or via multilinear alternating maps) is 1-dimensional.

[Oliver Nash]

IIUC, from Eric's remarks we have the exterior algebra but we don't have $∧^iV$ in master yet. So that's step one I guess.

[Heather Macbeth]

But it could be stated as the dimension of alternating_map R (λ i : fin (dim M), M) R.

[Oliver Nash]

You mean quotient?

[Heather Macbeth]

Sorry, alternating_map! Fixed.

[Oliver Nash]

Oh right, yes! That might be a sufficient workaround.

[Eric Wieser]

We should be able to show that alternating_map R is one-dimensional, right?

[Eric Wieser]

We have docs#alternating_map.module

[Eric Wieser]

and docs#multilinear_map.mk_pi_ring_apply and docs#multilinear_map.pi_ring_equiv look pretty close to a statement of one-dimensionality

[Eric Wieser]

Oliver Nash said:

Given $V$ of dim $n$, and $1 ≤ i ≤ n$, we can define $⊗^{n-1}V → Hom(V, ∧^n V)$ in an obvious way.

Isn't this operation basis-dependent, meaning we probably don't get anything useful by just defining it on a choice of basis?

[Oliver Nash]

It doesn't need a choice of basis but I think I compressed a bit too much into that sentence to make my meaning clear.

I'm saying that for each $i$ in the range $1 ≤ i ≤ n$, we have a map: $f_i : \otimes^{n-1} V \to Hom(V, ∧^nV)$. These maps are defined via multilinear maps $\hat f_i : \times^{n-1} V \to Hom(V, ∧^nV)$. So we just need to define $\hat f_i$. To do this let $v_1, \ldots, v_n$ be points of $V$ and define:

$\hat f(v_1, \ldots, v_{i-1}, v_{i+1}, \ldots, v_n) (v_i) = v_1 \wedge \cdots\wedge v_n$.

[Oliver Nash]

In particular for any $v_1, \ldots, v_n$ we have

$f_i(v_1 \otimes \cdots \otimes v_{i-1} \otimes v_{i+1} \otimes \cdots \otimes v_n) \in Hom(V, \wedge^nV)$

and these form a basis of $Hom(V, \wedge^nV)$ if $v_1, \ldots, v_n$ are a basis for $V$.

[Oliver Nash]

So this is a way to get a basis for $V^*$ if we have a basis for $V$ because the basis of $V$ identifies $\wedge^n V$ with the scalars.

[Heather Macbeth]

Eric Wieser said:

and docs#multilinear_map.mk_pi_ring_apply and docs#multilinear_map.pi_ring_equiv look pretty close to a statement of one-dimensionality

Is this the same thing? I want to consider alternating_map R (λ (i : ι), M) R, not multilinear_map R (λ (i : ι), R) M.

[Oliver Nash]

In my case, the above approach to the dual basis would be useful because, at the cost of obtaining a basis of $Hom(V, \wedge^nV)$ (instead of $V^*$) we get a map $\times^n V \to \times^n Hom(V, \wedge^nV)$ which is obviously smooth.

[Eric Wieser]

Oliver Nash said:

It doesn't need a choice of basis but I think I compressed a bit too much into that sentence to make my meaning clear.

I'm saying that for each $i$ in the range $1 ≤ i ≤ n$, we have a map: $f_i : \otimes^{n-1} V \to Hom(V, ∧^nV)$. These maps are defined via multilinear maps $\hat f_i : \times^{n-1} V \to Hom(V, ∧^nV)$. So we just need to define $\hat f_i$. To do this let $v_1, \ldots, v_n$ be points of $V$ and define:

$\hat f(v_1, \ldots, v_{i-1}, v_{i+1}, \ldots, v_n) (v_i) = v_1 \wedge \cdots\wedge v_n$.

Your $v_1, \ldots, v_n$ is what I was referring to as a basis, but I guess it doesn't need to span the entire space

[Eric Wieser]

Heather Macbeth said:

Is this the same thing? I want to consider alternating_map R (λ (i : fin (dim M)), M) R, not multilinear_map R (λ (i : ι), R) M.

No, unfortunately they don't match, they just look somewhat close

[Eric Wieser]

@Oliver Nash, it sounds like what you're describing is just partially applying docs#exterior_algebra.ι_multi (linkifier is broken) with all but one argument such that it becomes a linear map in a single argument?

[Eric Wieser]

I think the currying is docs#multilinear_map.curry_right?

[Eric Wieser]

So you want something like (exterior_algebra.ι_multi R n).to_multilinear_map.curry_right v_rest which gives the linear map from v_last to the tensor algebra

[Oliver Nash]

Eric Wieser said:

Oliver Nash, it sounds like what you're describing is just partially applying docs#exterior_algebra.ι_multi (linkifier is broken) with all but one argument such that it becomes a linear map in a single argument?

Yes exactly. Or more precisely, that's the definition, but what I really want is that this construction agrees with docs#basis.coord smuld with the wedge of all elements.

[Eric Wieser]

That doesn't feel true to me; with my definition, isn't (ι_multi R n).to_multilinear_map.curry_right v_rest v_last = ι_multi R n v_all?

[Eric Wieser]

So there's no smul component?

[Eric Wieser]

I get the feeling that what you're asking for is all in the statement and we already have the pieces to prove it if you can state it.

[Oliver Nash]

I probably haven't said it quite right because I'm mixing formal and informal mathematics, but there is a correct precise statement which it looks like, to my surprise and delight, I can probably formalise and prove easily enough.

[Oliver Nash]

I have one hour left today. I'll park some other threads and see if I can formalise all this now.

[Eric Wieser]

The one caveat of course is that the construction I'm describing maps into the exterior algebra not the exterior powers

[Oliver Nash]

Oh!

[Oliver Nash]

That may be a problem because it's important that I know the codomain is 1-dimensional.

[Oliver Nash]

Still, I'll see what I can do and what might be missing.

[Kyle Miller]

I'm not sure if this really helps much with formalization, but one version of the determinant I like is to say for $T:V\to V$ that $\det T=\operatorname{tr}(\wedge^nT)$. This is "more" basis-free since you don't need anything but finite dimensionality of $\wedge^n V$ to make the definition.

Also, you can generalize: $\operatorname{tr}(\wedge^k T)$ is coefficient $n-k$ of the characteristic polynomial of $T$ (with some $\pm$).

A reason I like this is that sometimes you can factor $T$ as $A\circ B$ with $A:W\to V$ and $B:V\to W$, then get $\det T=\operatorname{tr}(\wedge^n(B\circ A))$, which can be interesting when $W$ is not $n$-dimensional.

[Kyle Miller]

So, if there were a polynomial-valued trace for graded homomorphisms (the coefficient of $x^k$ is the trace when restricted to grading $k$) you could (sort of) get the characteristic polynomial as the trace of $\wedge T:\wedge V\to\wedge V$. It's not quite the characteristic polynomial since it'd be $\det(xT+I)$ rather than $\det(xI-T)$.

[Eric Wieser]

I'm afraid I'm confused by your notation and $\wedge^nT$ vs $\wedge^nV$, since $V$ is a type but $T$ is (linear?) map.

[Eric Wieser]

I guess you're using the one applied to $T$ to mean some lift of the map to $\wedge^nT : \wedge^nV \to \wedge^nV$?

[Kyle Miller]

Yeah, taking exterior powers is functorial, so I'm using $\wedge^n$ for both the map on objects and the map on morphisms. It comes from the induced map on tensor powers, which is also functorial.

[Eric Wieser]

Should we add {tensor,free,exterior,clifford}_algebra.map as a definition that simply composes with \io and calls lift, which would make $\wedge^nT$ spelt exterior_algebra.map T? (I realize you're talking about exterior powers not algebras so this is only tangentially related)

[Kyle Miller]

Without being too familiar with this part of the library, I'd think we should have these induced maps on these algebras, and that seems like a good construction.

[Eric Wieser]

Probably every single lift in the library should have a corresponding map and map_equiv...

[Scott Morrison]

We should have all the Schur functors, in any linear symmetric monoidal category. :-)

[Oliver Nash]

I'm just returning to this now. Do we have:

import linear_algebra.exterior_algebra

variables (ι R M : Type*) [field R] [add_comm_group M] [module R M]
variables (n : ℕ) (v : fin n → M)

lemma wedge_zero_iff_linear_independent :
  exterior_algebra.ι_multi R n v ≠ 0 ↔ linear_independent R v :=
begin
  sorry,
end

[Eric Wieser]

Yes, that's docs#alternating_map.map_linear_dependent

[Eric Wieser]

Or at least, modulo not_congr

[Eric Wieser]

Oh, I guess that's only one direction

[Oliver Nash]

OK thanks, it's a start anyway!

[Eric Wieser]

Ah, we're also missing no_zero_smul_divisors R (exterior_algebra R M)

[Oliver Nash]

Lean just told me this too!

[Eric Wieser]

Edited above with my two sorrys

[Oliver Nash]

Thanks. I'll see if I can fill some of this in.

[Eric Wieser]

I guess we probably want this first:

instance [no_zero_smul_divisors R S] : no_zero_smul_divisors R (free_algebra S X) := sorry

[Oliver Nash]

I'm suppose to be turning a sphere inside out and yet I'm learning about no_zero_smul_divisors :joy:

[Oliver Nash]

Eric Wieser said:

Ah, we're also missing no_zero_smul_divisors R (exterior_algebra R M)

Actually I'm OK thanks to no_zero_smul_divisors.of_division_ring:

import linear_algebra.exterior_algebra

variables (ι R M : Type*) [field R] [add_comm_group M] [module R M]
variables (n : ℕ) (v : fin n → M)

lemma wedge_ne_zero_iff_linear_independent :
  exterior_algebra.ι_multi R n v ≠ 0 ↔ linear_independent R v :=
begin
  rw not_iff_comm,
  split,
  { apply alternating_map.map_linear_dependent _ _,
    exact no_zero_smul_divisors.of_division_ring, },
  { intros h₁ h₂,
    sorry },
end

[Eric Wieser]

(docs#no_zero_smul_divisors.of_division_ring)

[Eric Wieser]

That's a slightly weaker statement though, right? Presumably

instance [no_zero_smul_divisors R S] : no_zero_smul_divisors R (exterior_algebra S X) := sorry

is true, but I guess you don't care because that's not a sphere that's the wrong way out.

[Oliver Nash]

Basically yes.

[Oliver Nash]

FWIW I tried to fill in the sorry above (linear independent implies wedge non-zero) yesterday evening and it seems non-trivial. Presumably there is some clever invocation of universal properties that gets you there but I couldn't see it. I could think of three proofs but they all require a specific model. The first two work if we know know the direct sum of quotient of tensor powers by alternating map gives a model. The third one is low-tech but probably least work, and would entail directly constructing a model of the exterior algebra from an ordered basis by defining it to be the free module on all 2^n subsets and defining the appropriate product.

[Oliver Nash]

I'd love to do this but I think it's just too much of a detour so I'm leaving this remark here in case anyone else fancies filling this gap.

[Eric Wieser]

Eric Wieser said:

I guess we probably want this first:

instance [no_zero_smul_divisors R S] : no_zero_smul_divisors R (free_algebra S X) := sorry

I had a go at this, but only got as far as #10247 and gave up at:

instance [no_zero_divisors R] : no_zero_smul_divisors R (free_algebra R X) :=
⟨λ c x h, begin
  induction x using free_algebra.induction,
  { rw [algebra.smul_def c, ←ring_hom.map_mul, algebra_map_eq_zero_iff] at h,
    rw algebra_map_eq_zero_iff,
    apply eq_zero_or_eq_zero_of_mul_eq_zero h, },
  { sorry },
  { sorry },
  { sorry } -- definitely false
end⟩

[Kyle Miller]

I started trying to make a model for the exterior algebra as

def exterior_algebra.model (R : Type*) [field R] (n : ℕ) := finset (fin n) → R

using the pi instance for the R-module structure but then defining multiplication via some convolution on partitions of a finite set weighted by the sign function:

def inversions : list (fin n) → ℕ
| [] := 0
| (x :: xs) := (xs.filter (λ y, y < x)).length + inversions xs

/-- in `{-1, 0, 1}`; `0` if they have an element in common, otherwise from parity of transpositions to put the union of `s` and `t` in order  -/
def sign (s t : finset (fin n)) : ℤ :=
let xs : list (fin n) := s.sort (≤),
    ys : list (fin n) := t.sort (≤)
in if s ∩ t = ∅ then (-1) ^ inversions (xs ++ ys) else 0

def partitions (b : model_basis R n) : finset (model_basis R n × model_basis R n) :=
finset.univ.filter (λ p, disjoint p.1 p.2 ∧ b = p.1 ∪ p.2)

def mul (x y : model R n) : model R n := λ b,
∑ p in partitions b, sign p.1 p.2 * x p.1 * y p.2

I'm giving up for now. Something that would need to be proved for associativity of the multiplication is

lemma sign_assoc (s t u : finset (fin n)) :
  sign s t * sign (s ∪ t) u = sign s (t ∪ u) * sign t u

as well as some additional lemmas to reassociate sums over partitions.

https://gist.github.com/kmill/a341402abba64f9d8788dd5c1e5ca82b

[Kyle Miller]

From a universal property point of view, I guess a concrete model is a way to get "invariants" for elements of the universal object, since you have a map from it to the model and can infer things about elements by looking at their images.

[Eric Wieser]

That only works as a model of an exterior algebra over a finite dimensional space, right?

[Eric Wieser]

This paper has a nice model of exterior algebras that also works for Grassmann-Cayley algebras, but again only for finite-dimensional ones

[Kyle Miller]

Yeah, it's true it's only for finite-dimensional M, but it can still be useful for showing wedge products of linearly independent lists are nonzero since you can extend the list into a basis for M and send everything else to zero in exterior_algebra.model R n.

The model can be fixed to work for infinite-dimensional M by changing the definition of the model to use an arbitrary totally ordered indexing set (rather than fin n) and making it be finitely supported functions.

[Oliver Nash]

Kyle Miller said:

I started trying to make a model for the exterior algebra as
...
https://gist.github.com/kmill/a341402abba64f9d8788dd5c1e5ca82b

Oh cool! It would be great to get this gap filled one way or another, and I agree there are various ways to make this handle the infinite-dimensional case too. FWIW, another possible route to a proof (that linear independent implies wedge non-zero) just occurred to me which should work using the model of the exterior algebra that we have taken as our definition (namely a quotient of the tensor algebra).

[Oliver Nash]

Specifically if we could fill this in:

import linear_algebra.exterior_algebra
import linear_algebra.pi_tensor_product

variables (R M : Type*) [field R] [add_comm_group M] [module R M]

def alternating_map.to_exterior_hom {n : ℕ} (f : alternating_map R M R (fin n)) :
  exterior_algebra R M →ₗ[R] R :=
sorry

[Oliver Nash]

then given a linearly-independent family v, we can use it to define an f above which will evaluate to 1 on exterior_algebra.ι_multi R n v which must mean exterior_algebra.ι_multi R n v is non-zero.

[Oliver Nash]

But the only way I can see to define alternating_map.to_exterior_hom is to start all the way back at free_algebra. Anyway.

[Eric Wieser]

In #10255 I'm only a few sorries away from showing tensor_algebra R M ≃ₐ[R] ⨁ n, ⨂[R]^n M, which might help a little when working with the exterior_algebra

[Eric Wieser]

Oliver Nash said:

But the only way I can see to define alternating_map.to_exterior_hom is to start all the way back at free_algebra. Anyway.

Here's an outline of how to define this that I think would work:

• Invoke docs#clifford_algebra.foldr with codomain (Π i : fin n.succ, alternating_map R M A (fin i)), ie tuples of alternatings maps of increasing degree
  • Start the fold with x = ![0, 0, 0, ..., f]
  • The recursive step should send v, ![x1, x2, ..., xn] to ![x2.curry_left v, x3.curry_left v, ..., 0]
    • This satisfies the requirement that applying the recursive step twice should give zero, as (g.curry_left v).curry_left v = 0 and we're inserting zeros on the LHS
• Invoke the alternating_map R M A (fin 0) term on the empty tuple to extra the term A.

[Eric Wieser]

I spent a while thinking about how to apply foldr in clever ways in #14790

[Eric Wieser]

#14802 adds some of the machinery needed to implement that

[Eric Wieser]

This strategy turns out to be cursed because (x i).curry_left v is of type alternating_map R M N (fin ↑(i.succ))not alternating_map R M N (fin (succ ↑i)), and for reasons that escape me, src#fin.succ is defined such that docs#fin.coe_succ is not true by rfl

[Reid Barton]

Oh because of the pattern match. I imagine it would be fine to redefine fin.succ to move the pattern match into the components.

[Eric Wieser]

The same applies for pretty much all the definitions about fin

[Reid Barton]

equiv used to have a bunch of definitions like this too and changing them to constructor-of-(pattern matches) didn't have any downsides (besides making the definitions somewhat less readable).

[Reid Barton]

In Lean 4, eta for structures should make this mostly irrelevant.

[Eric Wieser]

I fought through the pain in #14803

[Eric Wieser]

It's annoying that what looked like a fairly neat recursion scheme has turned into a dependently-typed mess

[Eric Wieser]

I was able to replace fin n with nat and all the pain went away

[Eric Wieser]

docs#exterior_algebra.lift_alternating now exists (but isn't in the docs yet), from which your alternating_map.to_exterior_hom follows straightforwardly; now what was it that we wanted it for again?

[Oliver Nash]

I wanted this (or something close at least) because I wanted to prove that barycentric coordinates were smooth without having to choose a basis. In the end I caved in and proved the result by choosing coordinates and using determinants: docs#affine_basis.det_smul_coords_eq_cramer_coords

[Oliver Nash]

The point is that if you let coordinates take values in the top exterior power instead of scalars then you obviate the need to divide by a determinant (except at the very end) but for this all to work I needed more basic facts about exterior algebras than we had at the time.

[Eric Wieser]

Probably extending a basis on the vector space to a basis on the exterior algebra should be next on my todo list

[Oliver Nash]

That would certainly be worth having!

[Oliver Nash]

Or you could go crazy and do the whole thing again but for Weyl algebras + symmetric algebra instead of Clifford algebras + exterior algebra.

[Oliver Nash]

(don't do this: these are much less important)

[Eric Wieser]

It's annoying that we seem to have to rebuild everything from scratch for each one of these

[Eric Wieser]

(I know little abotu Weyl/symmetric algebras, but I assume one is a special case of the other?)

[Oliver Nash]

Indeed, it is partly to raise this point that I mention this.

[Oliver Nash]

A Weyl algebra is sort of a Clifford algebra but with a skew-symmetric form instead of symmetric. And when you take the zero form you get the symmetric algebra.

[Oliver Nash]

(which are polynomials without having to choose a basis)

[Eric Wieser]

To some extent we might be shooting ourselves in the foot by saying "the fact that the clifford algebra is a quotient of the tensor algebra is an implementation detail"

[Eric Wieser]

Since that fact is precisely the thing that's shared by these four algebras

[Oliver Nash]

Well I think we should allow ourselves to use this model if it makes a proof easier but the fact that this model is actually our implementation should be an implementation detail.

[Oliver Nash]

(That might just amount to not hiding our implementation.)