Hodge star operator

Stream: maths

[Oliver Nash]

I was recently reminded that Mathlib has no definition of the Hodge star operator and I think it would make a great, and very accessible, first project.

I've just created https://github.com/leanprover-community/mathlib4/issues/17722 to advertise this.

[Oliver Nash]

(It would also make a great $n$ th project for $n > 0$.)

[Eric Wieser]

Does going through CliffordAlgebra make sense here? I believe there the hodge star of $x$ can be computed by taking the product of the generators in order, then multiplying by $x$. The choice of bilinear form comes into play when transporting though docs#CliffordAlgebra.changeFormEquiv

[Daniel Morrison]

I am interested in working on this but I'm not familiar with how to set up such a project, could you advise me on how I should get started?

[Kim Morrison]

It depends on a bit on what you mean by "set up such a project".

Does https://leanprover-community.github.io/contribute/index.html help?

Typically one would work on something like this by:

• saying that you're doing so
• cloning the mathlib repository
• creating a branch
• creating a new file to work in
• importing approximately what seems relevant
• writing down the essential definitions
• (optional, but good for new contributors) post the definitions here and ask for feedback
• write down every lemma you can think of about those definitions
• create a PR, and make sure that it appears on the #queue
• respond to feedback!

[Kim Morrison]

(and, for your first PR, go into it expecting that the last bullet point may constitute half the work)

[Daniel Morrison]

That does help, thank you!

What I'm mostly worried about is the steps

• import what seems relevant
• writing down definitions

Is it just a matter of trial and error or is there a good way of figuring out how to build the definition?

[Kevin Buzzard]

Try building one and then show it publically and see if people have comments. This is one of the hardest parts but there are experts here to help.

[Daniel Morrison]

Okay, so the answer is I should stop overthinking it and just try something! :)

[Kim Morrison]

(And for "import what seems relevant" it's fine to start off in a file with import Mathlib. There are then automated tools to strip the imports down once you have some content.)

[Oliver Nash]

@Daniel Morrison awesome! I'm delighted you're interested in helping here. Rereading my remarks at #17722 now I have two remarks:

• I think I overstated things when I said "certainly make a definition" that also covers the case of the symplectic star. This would be nice but even just the symmetric case would be great.
• I omitted to write down the key equation $\alpha \wedge \star \beta = (\alpha, \beta) vol$

I'm going to amend the issue now to make these adjustments.

[Oliver Nash]

Eric Wieser said:

Does going through CliffordAlgebra make sense here? I believe there the hodge star of $x$ can be computed by taking the product of the generators in order, then multiplying by $x$. The choice of bilinear form comes into play when transporting though docs#CliffordAlgebra.changeFormEquiv

Certainly docs#CliffordAlgebra.equivExterior looks very relevant and I'm surprised to find I've never thought about this. I can't immediately see if this point of view helps but I'd be interested if it did.

[Eric Wieser]

One sense in which it doesn't help is that many lemmas are missing about that the functions underlying that equivalence

[Oliver Nash]

Perhaps but filling in lemmas to get to a goal is the business of building Mathlib :)

[Oliver Nash]

FWIW here's how I'm used to thinking about the Hodge star. Let $V$ be an $n$-dimensional vector space over a field $K$.

Firstly, a choice of non-degenerate metric on $V$ induces a non-degenerate metric on $\wedge^i V$ for all $i$. This gives an identification with the dual:
$\wedge^i V \simeq (\wedge^i V)^*$

Secondly, the wedge product gives a bilinear map:
$\wedge^i V \times \wedge^{n-i} V \to \wedge^n V$
or equivalently:
$\wedge^i V \to (\wedge^{n-i} V)^* \otimes \wedge^n V$

Using the identification to the dual we thus have:
$\wedge^i V \to (\wedge^{n-i} V) \otimes \wedge^n V$

And then finally choose a volume form $\wedge^n V \simeq K$ (which is determined up to sign because it should have norm one) we get the Hodge star.

[Eric Wieser]

Oliver Nash said:

I can't immediately see if this point of view helps but I'd be interested if it did.

I think the construction is immediate as $x^\star =E_Q(E_Q^{-1}(x)\prod_i \iota(v_i))$ where $v_i$ is some ordered finite basis and $E_Q : Cl(Q) \cong \bigwedge(V)$

[Oliver Nash]

Oh nice, I really should have known this.

I think the way to say this in a basis-free way is if $q : \wedge^* V \to Cl(V)$ is the linear isomorphism (the inverse of your $E_Q$), $vol \in \wedge^n V$ is a chosen volume element, and $\alpha \in \wedge^i V$ then $q(\star \alpha) = q(\alpha)q(vol)$ where, of course the product on the RHS is the Clifford algebra product.

[Oliver Nash]

Looking now I think people call $q$ the quantisation map and $q(vol)$ the chirality element (and sometimes denote it $\Gamma$).

[Oliver Nash]

I now belatedly realise this was implicit in things I did know. The existence of $q$ means there must be a linear map $\rho : V \to End(\wedge^*V)$ such that $\rho(v)^2 = \|v\|^2 1$ for all $v$. At least up to signs, the action is $\rho(v)\alpha = v^* \rfloor \alpha + v \wedge \alpha$, where $v^* \in V^*$ is the dual of $v$ wrt the metric, and the first term is the interior product (sadly I'm using rfloor because the right symbol, seems unavailable in Zulip LaTeX).

The is an important thing for differential geometers because this means the tangent bundle of an oriented Riemannian manifold is a Clifford bundle and so has a Dirac operator, which is the deRham operator $d + d^*$, with square the (real) Hodge Laplacian etc.

[Eric Wieser]

Oliver Nash said:

I now belatedly realise this was implicit in things I did know. The existence of $q$ means there must be a linear map $\rho : V \to End(\wedge^*V)$ such that $\rho(v)^2 = \|v\|^2 1$ for all $v$. At least up to signs, the action is $\rho(v)\alpha = v^* \rfloor \alpha + v \wedge \alpha$, where $v^* \in V^*$ is the dual of $v$ wrt the metric, and the first term is the interior product

This looks a lot like the construction of equivExterior!

[Oliver Nash]

I thought it might be :)

[Oliver Nash]

Somebody should also add the definition of interior product to Mathlib!

(It might exist implicitly, with some crazy name.)

[Eric Wieser]

Of what type signature?

[Oliver Nash]

Bilinear map $V^* \times \wedge^{i+1} V \to \wedge^i V$.

[Eric Wieser]

That sounds like docs#CliffordAlgebra.contractLeft

[Daniel Morrison]

@Oliver Nash I would personally enjoy getting the symplectic version because my thesis is on symplectic manifolds. :smile:

It turns out that ExteriorAlgebra is defined to be CliffordAlgebra 0 so the CliffordAlgebra approach may be a smart way to do it. I starting working on the part where a bilinear form on V induces a bilinear form on $\bigwedge^k V$, but I may take a detour to trying out the Clifford Algebra approach.

[Eric Wieser]

That induced bilinear form would be a nice result to have still

[Daniel Morrison]

Yeah I'm planning to do that still and I'll need it anyway for the inner product property of the Hodge star.

[Daniel Morrison]

Update: I was able write down a definition of the Hodge star! Here's the code, feedback is appreciated.

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.BilinearForm.Basic
import Mathlib.LinearAlgebra.Finsupp
import Mathlib.LinearAlgebra.Orientation
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.InnerProductSpace.Orientation
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

open ExteriorAlgebra CliffordAlgebra LinearMap

noncomputable section Clifford

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
variable [Nontrivial E]
instance : Nonempty (Fin <| Module.finrank ℝ E) := Fin.pos_iff_nonempty.mp Module.finrank_pos
variable (o : Orientation ℝ E (Fin <| Module.finrank ℝ E))

def basis : OrthonormalBasis (Fin <| Module.finrank ℝ E) ℝ E :=
  OrthonormalBasis.adjustToOrientation (stdOrthonormalBasis ℝ E) o

def vol : ExteriorAlgebra ℝ E := (ιMulti ℝ (Module.finrank ℝ E)) (basis o)

variable (B : LinearMap.BilinForm ℝ E) --(Bsymm : B.IsSymm) --(Bnondeg : B.Nondegenerate)

def Q := BilinMap.toQuadraticMap B
def C := CliffordAlgebra (Q B)

def HodgeStar : (ExteriorAlgebra ℝ E) → (ExteriorAlgebra ℝ E) :=
  fun v ↦ equivExterior (Q B) ((equivExterior (Q B)).symm v * (equivExterior (Q B)).symm (vol o))

end Clifford

[Daniel Morrison]

This is on branch morrison-daniel/hodge-star

[Kim Morrison]

You'll need to think about naming: can't just put basis, vol, Q and C in the root namespace.

[Kim Morrison]

Can you prove it's involutive?

[Kim Morrison]

Does the expected thing on homogeneous elements?

[Antoine Chambert-Loir]

Part of this does not really needs a “metric” but just a nondegenerate bilinear form, that provides the identification of $V$ with its dual. It is also useful in non Euclidean settings, Minkowski or symplectic.

[Antoine Chambert-Loir]

(I'm responding to an earlier message of @Oliver Nash )

[Oliver Nash]

Agreed Antoine!

In fact I emphasised we should cover the symplectic case in the original issue #17722 but then I worried that I might be setting the bar too high so I wrote my sketch here using the language of metric. Certainly the Clifford algebra trick used above won't work unless Eric has set things up so that we get the Weyl algebra in the skew case (which I think he hasn't, and presumably has char 2 issues).

[Oliver Nash]

Aside from the usual Mathlib philosophy I'm all in favour of being general: I want to be able to write Maxwell's equations (Minkowski star) and state Liouville's divergence theorem (symplectic star) etc.

[Dominic Steinitz]

Oliver Nash said:

Aside from the usual Mathlib philosophy I'm all in favour of being general: I want to be able to write Maxwell's equations (Minkowski star) and state Liouville's divergence theorem (symplectic star) etc.

:thumbs_up: and also be able to describe electromagnetism as a gauge theory.

[Daniel Morrison]

I can prove the Hodge star is linear and that 1 maps to the volume element, but I think to do anything more I need additional properties of the Clifford algebra product. Anyone have an idea for a smart way to move forward?

[Oliver Nash]

You're probably running into the point Eric highlighted above

You should be able to get a bit further if you can verify that the remarks I made here are correct. E.g., let's try to consider the action on a vector $v$, then the defining equation we're using is $q(\star v) = q(v)\Gamma$ but according to my remark, $q(v)\Gamma = v^* \rfloor vol + v \wedge vol$. The second term is zero (for dimensional reasons) and the first gives the familiar formula for Hodge star on vectors (up to signs). So proving a lemma about docs#CliffordAlgebra.equivExterior capturing this action would help you progress.

However looking a bit more closely now I think the issue of signs which I've been ignoring is a bit more serious, and probably means we should not take this approach. To be specific, consider the involutive (up to signs) property. This is actually easy because we get: $q(\star\star\alpha) = q(\star\alpha)\Gamma = q(\alpha)\Gamma^2$. Now $\Gamma^2$ is a scalar and in positive signature we have $\Gamma^2 = (-1)^{n(n-1)/2}$. So that would say $\star\star\alpha = (-1)^{n(n-1)/2} \alpha$ for all $\alpha$. This can't be right because in general the square of the star depends on the degree of the form.

With this in mind, I think we should define the Hodge star independently of the Clifford algebra stuff, but it would be lovely eventually to prove a version of $q(\star\alpha) = \pm q(\alpha)\Gamma$ for homogeneous $\alpha$ with the appropriate sign.

[Eric Wieser]

Whoops, I should have remembered that. Indeed, the signs of the hodge star are not the same as the "Clifford dual"

[Eric Wieser]

One path possible path here is using @Sophie Morel's work on the basis for exterior algebras, which I've just gotten back to reviewing.

[Eric Wieser]

(I've a branch myself for a basis on the Clifford algebra, but it's much less mature)

[Daniel Morrison]

Then what would make sense for me to work on, in the interest of not duplicating work? Maybe I can go back to the induced form on the exterior algebra.

[Oliver Nash]

The induced form would be great to have, and we’ll want it no matter what route we take.

[Oliver Nash]

I hope it’s not disappointing to have to pivot slightly but I think what you’ve done is already very helpful, even if it’s just clarifying what we’re should do.

[Oliver Nash]

Besides, arguably this is Hodge’s fault for not putting the right power of -1 into the equation $\alpha \wedge \star \beta = (\alpha, \beta) vol$

[Daniel Morrison]

I don't mind pivoting, I really just want something interesting to work on while I job hunt so I'm happy to take false starts as long as there's another one right after :smile:

[Daniel Morrison]

I started work on the induced bilinear form on the exterior powers based on Sophie's work. (I have bilinearity, and symmetric bilinear form induces a symmetric bilinear form so far) Should I just merge that branch into mine or is there a better way for me to build off that work?

[Johan Commelin]

Merge sounds good to me

[Daniel Morrison]

I have a design question and would appreciate some advice. I've been working on developing the induced bilinear form based on the existing work on the basis of an exterior algebra. (I've found it requires some repair work so I've been copy-pasting sorry-ed results as needed) For those unaware, it assumes a basis Basis I R M on M where I is a Fintype with a LinearOrder on it and constructs a basis on $\bigwedge^k M$ indexed by subsets of I of cardinality k.

I then defined the induced form on $\bigwedge^k M$ by

noncomputable def inducedForm (B : LinearMap.BilinForm R M) (b : Basis I R M) :
  ⋀[R]^k M → ⋀[R]^k M → R := fun v w ↦ ∑ s : {s : Finset I // Finset.card s = k},
  ∑ t : {s : Finset I // Finset.card s = k},
  (b.exteriorPower.coord s v * b.exteriorPower.coord t w) *
  Matrix.det (fun i j ↦ B (b (Finset.orderIsoOfFin s.val s.property i))
  (b (Finset.orderIsoOfFin t.val t.property j)) )

I can then prove that this is a bilinear form, and that if B is symmetric then the induced form is symmetric. My next step was to start on the vector space case with a non-degenerate form to start going for the Hodge star, but I realized that it would be useful to use the Basis.dualBasis definition to greatly simply calculations and this would be applicable in both the inner product and symplectic cases. Then it would be convenient to have a definition of the induced form that allows inputs to use two different bases to compute, namely it looks like this:

noncomputable def inducedForm (B : LinearMap.BilinForm R M) (b₁ b₂ : Basis I R M) :
  ⋀[R]^k M → ⋀[R]^k M → R := fun v w ↦ ∑ s : {s : Finset I // Finset.card s = k},
  ∑ t : {s : Finset I // Finset.card s = k},
  (b₁.exteriorPower.coord s v * b₂.exteriorPower.coord t w) *
  Matrix.det (fun i j ↦ B (b₁ (Finset.orderIsoOfFin s.val s.property i))
  (b₂ (Finset.orderIsoOfFin t.val t.property j)) )

Specifically, expanding the right entry in the standard basis and the left entry in the dual basis simplifies a lot. Is it a good or bad idea to allow this kind of basis flexibility?

Side Question: I want to prove the definition is independent of the choice of basis but I'm not sure what would be a good way to make that happen. In particular, the odd indexing sets makes this a bit of a pain.

[Oliver Nash]

Because your definition InducedForm demands a basis, but does not in fact depend on it, we would regard it as an "auxiliary" definition. This means that it would only be used to construct a second definition which does not demand a basis, and that it would be this second definition which everyone would use. As such, you have a lot of freedom to construct your auxiliary definition according to what makes the implementation most convenient. In particular if allowing it depend on _two_ bases (which looks like a clever idea) simplifies things, then this is fine.

That's all rather abstract, to see a concrete instance of this design pattern I encourage you to look at docs#LinearMap.trace

[Oliver Nash]

Having said all that, I have to say I'm not convinced that this approach via bases is the right way to go. We definitely will want API for handling the interaction of the bilinear form and bases but it seems to me that these should be lemmas and the definition should be done by other means. Aside from the fact that we might want to use this theory for non-free modules (though we could probably live without this: I cannot think of an example) I think this will just be easier to set up.

I am acutely conscious that you have invested substantial time in this approach (not to mention the previous approach via Clifford algebras) and I begin to feel quite guilty to have guided a talented new contributor into what has turned out to be a much trickier task than I had expected. By way of compensation, I will outline an approach which I hope should prove tractable.

[Oliver Nash]

First informally, if I want a bilinear form on $\wedge^kM$ this means I want something of type $Hom(\wedge^kM, Hom(\wedge^kM, R))$. But the universal property of the exterior power is that linear maps out of it are the same as alternating maps. So this means what I really want is a map of signature $(M \times \cdots \times M) \times (M \times \cdots \times M) \to R$ which each bracket has $k$ terms and is alternating. If $B$ is a bilinear form on $M$ the definition of such a map is $((v_1, \ldots, v_k), (w_1, \ldots, w_k)) \mapsto \det B(v_i, w_j)$.

[Oliver Nash]

So that's the informal story, formally here's how things should look:

import Mathlib

namespace ExteriorAlgebra

variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
  (k : ℕ)

/-- `k`-fold alternating-linear maps are the same as linear maps from the `k`th exterior power.

Version of `ExteriorAlgebra.liftAlternatingEquiv` which respects the grading. -/
def liftAlternatingGraded :
    M [⋀^Fin k]→ₗ[R] N ≃ₗ[R] ⋀[R]^k M →ₗ[R] N :=
  sorry

variable {R M}
variable (B : LinearMap.BilinForm R M)

private def BilinFormAux :
    M [⋀^Fin k]→ₗ[R] M [⋀^Fin k]→ₗ[R] R where
  toFun v :=
    { toFun := fun w ↦ Matrix.det fun i j ↦ B (v i) (w j)
      map_add' := sorry
      map_smul' := sorry
      map_eq_zero_of_eq' := sorry }
  map_add' := sorry
  map_smul' := sorry
  map_eq_zero_of_eq' := sorry

protected def BilinForm : LinearMap.BilinForm R (⋀[R]^k M) :=
  (liftAlternatingGraded R M R k) ∘ₗ
    liftAlternatingGraded R M (M [⋀^Fin k]→ₗ[R] R) k (BilinFormAux k B)

end ExteriorAlgebra

[Oliver Nash]

I notice that while we do have docs#ExteriorAlgebra.liftAlternatingEquiv, the corresponding statement respecting the grading, liftAlternatingGraded seems to be missing. So defining this should probably be your first task. It's likely that @Eric Wieser has thought about this (and perhaps even has a version outside Mathlib somewhere) so I will ask him to comment.

[Daniel Morrison]

Okay I understand now, I was thinking AlternatingMap was literally a map $$\bigwedge^k M \to N$ so it was kind of a chicken and the egg problem, but I see now that it's just a multilinear map with the alternating property and the liftAlternating def is just telling how to use the AlternatingMap to construct a map on the exterior algebra. I agree that makes way more sense.

The SM.ExteriorPower branch has a graded version of the lift map so it would be good to get that merged.

[Eric Wieser]

The SM.ExteriorPower branch is #10654, which first needs #11155 (which is close to ready) then #11156 (which hasn't been reviewed due to the unmerged dependee making the diff very large)

[Daniel Morrison]

Ah, I see, I didn't realize the chain of pull requests goes that deep.

[Eric Wieser]

Actually, I think #10654 might be incorrectly marked as depending on the other two?

[Dean Young]

If this includes complex numbers then it is probably a good idea to add in the Hodge theory involving dz̅ᵢ and dzᵢ.

[Daniel Morrison]

Can anyone see why this code fails? I'm trying to write my matrix using Matrix.updateColumn so I can use Matrix.det_updateColumn_add, but Lean doesn't understand my rw [aux] line even though it's exactly character for character what's in the target. I've tried other ways of doing the proof I need but Lean always gets stuck on something similar.

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.LinearAlgebra.BilinearForm.Basic
import Mathlib.LinearAlgebra.BilinearForm.Properties

open ExteriorAlgebra BigOperators

namespace exteriorPower

variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
variable (B : LinearMap.BilinForm R M)
variable {k : ℕ}

section inducedForm

theorem aux (v w : Fin k → M) (x y : M) (j': Fin k) :
  (Matrix.of fun i j ↦ (B (v i)) (Function.update w j' (x + y) j)) =
  (Matrix.of fun i j ↦ (B (v i)) (w j)).updateColumn j' (fun i ↦ B (v i) (x + y)) := by
  ext i j
  rw [Matrix.of_apply, Matrix.updateColumn_apply, Function.update_apply, apply_ite (B (v i))]
  rfl

private def BilinFormAux :
    M [⋀^Fin k]→ₗ[R] M [⋀^Fin k]→ₗ[R] R where
  toFun v :=
    { toFun := fun w ↦ Matrix.det <| Matrix.of (fun i j ↦ B (v i) (w j))
      map_add' := by
        intro _ w j' x y
        dsimp
        rw [aux B v w x y j']

        sorry
      map_smul' := sorry
      map_eq_zero_of_eq' := sorry }
  map_add' := sorry
  map_smul' := sorry
  map_eq_zero_of_eq' := sorry

[Damiano Testa]

You can brute force it with

        convert_to ((Matrix.of fun i j => (B (v i)) (w j)).updateColumn j' fun i => (B (v i)) (x + y)).det = _
        congr 1
        convert aux B v w x y j'

but I suspect that a better solution involves writing some rfl lemma to make the conversion smoother.

[Eric Wieser]

Using Mayrix.submatrix instead of raw indexing should make things easier

[Daniel Morrison]

I've been fiddling with this step a bit more and I'm pretty stuck. I looked into Matrix.submatrix and I see how it might simplify things, but I'm not sure how well it'll interact with det, and it would require having an initial matrix which would likely require a basis which I think we want to avoid if we can.

What I've been trying to do is write some intermediate lemmas but that's not going anywhere either. Most recently I tried writing

theorem Matrix.bilin_det_of_updateColumn_add (v w : Fin k → M)
  (j' : Fin k) (x y : M) :
  ((Matrix.of (fun i j ↦ B (v i) (w j))).updateColumn j' (fun i ↦ B (v i) x + B (v i) y)).det =
  ((Matrix.of (fun i j ↦ B (v i) (w j))).updateColumn j' (fun i ↦ B (v i) x)).det +
  ((Matrix.of (fun i j ↦ B (v i) (w j))).updateColumn j' (fun i ↦ B (v i) y)).det := by
  rw [← Matrix.det_updateColumn_add]
  rfl

and then going

intro _ w j' x y
        dsimp
        simp only [Matrix.of_update_right]
        simp only [B.add_right]
        rw [← Matrix.bilin_det_of_updateColumn_add B v w j' x y]

inside that map_add I was working on above. But this didn't work as well and I'm really not sure how to move forward. If anyone has time to work with me to figure out a good way forward I'd greatly appreciate that!

[Oliver Nash]

I’m afraid I’m travelling for about 10 days without a laptop. I hope somebody else can help you before then.

By way of motivation I can say that Lean / Mathlib have a very steep learning curve but it does eventually level off.

[Dominic Steinitz]

Oliver Nash said:

By way of motivation I can say that Lean / Mathlib have a very steep learning curve but it does eventually level off.

I look forward to that happy day.

[Oliver Nash]

As promised, I am available to help with this work again now. Firstly, here is a sorry-free implementation:

import Mathlib

open Function

namespace ExteriorAlgebra

variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
  (k : ℕ)

variable {R M}
variable (B : LinearMap.BilinForm R M)

theorem auxCol {ι : Type*} [DecidableEq ι] (v w : ι → M) (z : M) (l : ι) :
    (Matrix.of fun i j ↦ B (v i) (Function.update w l z j)) =
    (Matrix.of fun i j ↦ B (v i) (w j)).updateColumn l (fun i ↦ B (v i) z) := by
  ext i j
  simp only [update_apply, Matrix.of_apply, Matrix.updateColumn_apply]
  aesop

theorem auxRow {ι : Type*} [DecidableEq ι] (v w : ι → M) (z : M) (l : ι) :
    (Matrix.of fun i j ↦ B (Function.update v l z i) (w j)) =
    (Matrix.of fun i j ↦ B (v i) (w j)).updateRow l (fun j ↦ B z (w j)) := by
  ext i j
  simp only [update_apply, Matrix.of_apply, Matrix.updateRow_apply]
  aesop

private def BilinFormAux :
    M [⋀^Fin k]→ₗ[R] M [⋀^Fin k]→ₗ[R] R where
  toFun v :=
    { toFun := fun w ↦ (Matrix.of fun i j ↦ B (v i) (w j)).det
      map_update_add' := fun {_i} w l x y ↦ by
        -- Nasty goal because it contains two different terms of type `DecidableEq (Fin k)`, namely
        -- `instDecidableEqFin k` in `Matrix.det` and `_i : DecidableEq (Fin k)` in
        -- `Function.update`. Similarly in other goals. Hence we need `convert` instead of `exact`.
        simp only [auxCol, map_add]
        -- If we uncomment the below rewrite then we can use `exact` instead of `convert`
        -- rw [(show instDecidableEqFin k = _i from Subsingleton.elim _ _)]
        convert Matrix.det_updateColumn_add _ l _ _
      map_update_smul' := fun {_i} w l t x ↦ by
        simp only [auxCol, map_smul]
        convert Matrix.det_updateColumn_smul _ l t _
      map_eq_zero_of_eq' := fun w l₁ l₂ hl hl' ↦ Matrix.det_zero_of_column_eq hl' <| by simp [hl] }
  map_update_add' {_i} v l x y := by
    ext w
    simp only [AlternatingMap.coe_mk, MultilinearMap.coe_mk, AlternatingMap.add_apply,
      auxRow, map_add, LinearMap.add_apply]
    convert Matrix.det_updateRow_add _ l _ _
  map_update_smul' {_i} v l t x := by
    ext w
    simp only [AlternatingMap.coe_mk, MultilinearMap.coe_mk, AlternatingMap.smul_apply, smul_eq_mul,
      auxRow, map_smul, LinearMap.smul_apply, smul_eq_mul]
    convert Matrix.det_updateRow_smul _ l t _
  map_eq_zero_of_eq' v l₁ l₂ hl hl' :=
    AlternatingMap.ext fun w ↦ Matrix.det_zero_of_row_eq hl' <| funext fun i ↦ by simp [hl]

end ExteriorAlgebra

[Oliver Nash]

The above is not Mathlib-ready but it does at least demonstrate how this can be done.

[Oliver Nash]

I suspect much, if not all, of the difficulty that @Daniel Morrison suffered was due to a somewhat rare and really horrible gotcha which arises in the above.

Specifically in several of the goals there are two different terms of type DecidableEq (Fin k). I discovered this because I was surprised that a certain rw would not fire even though the pretty-printed terms looked identical. I concluded that the two terms must contain implicit data that was unequal so I expanded terms in the infoview. There I learned that the call to Matrix.det was using instDecidableEqFin k whereas the call to Function.update was using the variable I have called _i in the code. There are several ways to deal with this but really we should try to think of ways to avoid it happening at all.

I need to cook dinner now but I'll return to see if I can think of how we might change Mathlib to rid ourselves of this pain.

[Eric Wieser]

I'm responsible for introducing this pain in the first place

[Eric Wieser]

There's a standard pattern for avoiding it when constructing multilinear maps, but perhaps we should provide an alternative constructor to encapsulate that approach

[Eric Wieser]

(I think the pattern is cases Subsingleton.elim _i _ or similar)

[Daniel Morrison]

Thank you! I was going crazy because I couldn't figure out why Lean wasn't happy with terms that appeared identical.

[Eric Wieser]

Here's the convert free spelling:

private def BilinFormAux :
    M [⋀^Fin k]→ₗ[R] M [⋀^Fin k]→ₗ[R] R where
  toFun v :=
    { toFun := fun w ↦ (Matrix.of fun i j ↦ B (v i) (w j)).det
      map_update_add' := fun {_i} w l x y ↦ by
        cases Subsingleton.elim _i (by clear _i; infer_instance)
        simpa only [auxCol, map_add] using Matrix.det_updateColumn_add _ l _ _
      map_update_smul' := fun {_i} w l t x ↦ by
        cases Subsingleton.elim _i (by clear _i; infer_instance)
        simpa only [auxCol, map_smul] using Matrix.det_updateColumn_smul _ l t _
      map_eq_zero_of_eq' := fun w l₁ l₂ hl hl' ↦ Matrix.det_zero_of_column_eq hl' <| by simp [hl] }
  map_update_add' {_i} v l x y := by
    cases Subsingleton.elim _i (by clear _i; infer_instance)
    ext w
    simp only [AlternatingMap.coe_mk, MultilinearMap.coe_mk, AlternatingMap.add_apply,
      auxRow, map_add, LinearMap.add_apply]
    exact Matrix.det_updateRow_add _ l _ _
  map_update_smul' {_i} v l t x := by
    cases Subsingleton.elim _i (by clear _i; infer_instance)
    ext w
    simp only [AlternatingMap.coe_mk, MultilinearMap.coe_mk, AlternatingMap.smul_apply, smul_eq_mul,
      auxRow, map_smul, LinearMap.smul_apply, smul_eq_mul]
    exact Matrix.det_updateRow_smul _ l t _
  map_eq_zero_of_eq' v l₁ l₂ hl hl' :=
    AlternatingMap.ext fun w ↦ Matrix.det_zero_of_row_eq hl' <| funext fun i ↦ by simp [hl]

[Eric Wieser]

This weirdness is explained in detail in the module docstring for docs#MultilinearMap

[Eric Wieser]

cases Subsingleton.elim _i (by clear _i; infer_instance) could probably be a tactic, perhaps canonicalize_instance _i

[Oliver Nash]

I was also thinking about a tactic for this situation; I like the canonicalize_instance proposal (maybe it could even not need the _i argument and run for all subsingleton instances).

[Oliver Nash]

Are we sure that option 2 from the (excellent) module doc string for docs#MultilinearMap is not the best option?

It also occurred to me that there is an option 4: instead of ∀ [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i), one could use ∃ _i : DecidableEq ι, ∀ (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i),.

However I think it's very undesirable that the user needs to interact with decidability at all in order to work with multilinear maps. If option 2 is a non-runner, could we have a non-computable version of Function.update? I'd be willing to work hard to excuse the decidability here if we could agree on a good direction.

[Eric Wieser]

I like the exists idea, I hadn't thought of that. The main downside is we lose the nice where notation, but we'd also lose that with my "alternate constructor" proposal

[Eric Wieser]

Making update noncomputable is very unappealing to me, and having a non computable copy means duplicating everything

[Oliver Nash]

Making update noncomputable is very appealing to me :upside_down:

[Oliver Nash]

I agree the solution is not clear but I think there is a problem if multilinear algebra requires thinking about decidability, and I think it is important we admit this.

[Eric Wieser]

The problem only arises when constructing maps with a constructor, which I think is often quite rare for multilinear maps. I think the Exists approach is a good one, or potentially even

structure WithDecidableEq (P : DecidableEq I -> Prop) : Prop where
  decidable : DecidableEq I := by infer_instance
  prop : P decidable

to save the user having to write inferInstance

[Oliver Nash]

The above looks nice but I'll have to think about it later as work is calling.

I stand by my remarks about there being a problem if the user ever needs to think about decidability, but I agree it's probably fairly rare that it comes up.

[Daniel Morrison]

Hello! I'm back to working on this and have a few questions on implementation.

1. I've been working on the induced form, and my aim has been to target showing the induced form is symmetric/non-degenerate if the original form is symmetric/non-degenerate. The hang-up now is that I've been working under the assumption of a basis (induced from a basis on the original space), but it seems it would be best to avoid this dependence for the sake of generality. I think I can prove symmetric from a spanning set, but non-degenerate seems more complicated due to the determinant in the definition of the induced form. What would be a reasonable general assumption to make? Similarly, what might that look like for the Hodge star? I'm used to seeing it pretty explicitly written in terms of a orthonormal basis but the impression I get is that we want a more broadly useful definition.

2. I ran into an issue where Lean could not deduce the instance instance : Fintype { s : Finset I // s.card = k } where I is itself Finite. Does this exist somewhere or how might I prove it? (this comes up since { s : Finset I // s.card = k } is the index set for the induced basis on $\bigwedge^k M$)

[Eric Wieser]

You should be able to prove this from docs#Finset.powersetCard