Exterior powers

Stream: Is there code for X?

[Sophie Morel]

What is know about exterior powers in mathlib ? So far the best I found is https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.html, which defines the exterior algebra as a graded algebra.

I asked lean to synthesize a FiniteDimensional instance on the nth exterior of a finite-dimensional vector space and got an error. That is not very hard to fix, but does this mean that mathlib doesn't have the formula for the dimension of the nth exterior power of a finite-dimensional vector space (or a free module of finite rank) ?

Still about exterior powers but unrelated, what about the NormedSpace case ? Is the topological vector space structure on exterior powers defined ?

The reason of all these questions, of course, is that I am trying to define the Plücker embedding from a Grassmannian to a projective space, and I want to do it coordinate-free. Hence exterior powers.

[Sebastien Gouezel]

I don't think we have anything serious there. Maybe @Yury G. Kudryashov or @Heather Macbeth have something more on a branch, towards de Rham cohomology, but not PRed yet if I understand correctly.

[Sophie Morel]

Okay, I can sorry the results I need about dimension of exterior powers for now.

I can also work in finite dimension so the exterior power has a canonical topological vector space structure. But now I have another question, as I don't just need a tvs structure to define the manifold structure, I need a NormedSpace instance: is there some preferred way to put a NormedSpace instance on a finite-dimensional vector space over a NontriviallyNormedField ? I have been looking at the NormedSpace files in mathlib but I haven't found anything yet. (Of course I can do it myself: use choice to pick an isomorphism with a Fin r → 𝕜 (where 𝕜 is my base field) and then transport the norm. I was just wondering is there's a better way.)

[Antoine Chambert-Loir]

Even if you choose a basis, what norm will you choose on ‘Fin r to k‘?

[Sebastien Gouezel]

I would avoid using finite-dimensionality to choose a norm and arguing that since all norms are equivalent it gives the right topology. Instead I'd rather put the correct norm on exterior products of a normed space-- whatever that is. For the exterior product of a dual space, I know what this should be: the operator norm on multilinear maps. For the exterior product of a space, maybe embed it into its bidual and use the previous sentence -- or do that in a more canonical way I am not thinking of for now, probably.

[Sebastien Gouezel]

Note that it would make sense to do that for tensor products first. There are two canonical norms on tensor products, but only one of them comes from the point of view of multilinear maps, so that's probably the one whose analogue we want to use here.

[Eric Wieser]

There's an open issue about putting an inner product space structure on the tensor product, with some links to previous work

[Eric Wieser]

Regarding exterior powers:

• we have them today as LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i, but that's obviously not very convenient
• probably we want them as a a quotient of docs#TensorPower
• I think @Amelia Livingston has some work on them in https://github.com/leanprover-community/mathlib/tree/koszul_cx

[Sophie Morel]

Antoine Chambert-Loir said:

Even if you choose a basis, what norm will you choose on ‘Fin r to k‘?

Lean does it for me, it's the sup norm:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/Basic.html#Pi.normedSpace
(And it's an instance, so if I did something else it would require extra effort.)

[Heather Macbeth]

Sebastien Gouezel said:

I don't think we have anything serious there. Maybe Yury G. Kudryashov or Heather Macbeth have something more on a branch, towards de Rham cohomology, but not PRed yet if I understand correctly.

Yury and I have avoided this issue by working with the antisymmetric k-multilinear maps from V rather than the k-th exterior power of V-dual. And FWIW, I've come to think of this not as a formalization hack but as a reflection of mathematical reality ...

[Yury G. Kudryashov]

Indeed, this way we don't have to assume [FiniteDimensional] here and there.

[Yury G. Kudryashov]

The project is on hold for now but we're going to CMU in November for a week to collaborate on it.

[Sophie Morel]

Okay, this is giving me some ideas. First, I need to generalize things a little bit from Fin r to general fintypes.

[Sophie Morel]

I think that all this really is an argument in favor of using the "algebraic geometry" Grassmannian, i.e. the set of dimension $r$ subspaces of the dual of $E$. I cannot say that I am displeased by this. :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Sophie Morel said:

Okay, this is giving me some ideas. First, I need to generalize things a little bit from Fin r to general fintypes.

I am always in favour of this!

[Sophie Morel]

So I now have a PR (#10654) introducing exterior powers and giving some of their properties, like a basis (when the module is free). I also wrote some code to define a norm on them following Sébastien's suggestion, though I am not totally satisfied with it (I don't think that one should just use multilinear maps into the base field, but into all normed vector spaces, which introduces universe issues). But maybe @Yury G. Kudryashov or @Heather Macbeth you've made progress on that ?

[Sébastien Gouëzel]

Wow, #10654 looks awesome!

[Eric Wieser]

A basic question relating to that PR; do we want ExteriorPower R n M : Type* or exteriorPower R n M : Submodule R (ExteriorAlgebra R M)?

[Eric Wieser]

Right now we have the name of the first but the type of the second :upside_down:. docs#TensorPower, for comparison, is a Type.

[Eric Wieser]

Maybe it's fine to have both?

[Richard Copley]

Re defining a norm, in case it's helpful (probably not!) I'll mention the inner product space defined on an exterior power of a finite-dimensional inner product space via the Gram determinant, as described here on Wikipedia.

[Eric Wieser]

I think whatever we do about the norm, it does not belong in #10654, to prevent that PR becoming too big!

[Ruben Van de Velde]

If it isn't yet :innocent:

[Sophie Morel]

On the one hand, I like types. On the other hand, I would like to be able to say that the exterior algebra is the direct sum of all the exterior powers, and I don't know how to do that if it's not a submodule.

[Eric Wieser]

I would like to be able to say that the exterior algebra is the direct sum of all the exterior powers,

We already have that result stated for types, it's docs#DirectSum.decomposeAlgEquiv (via docs#ExteriorAlgebra.gradedAlgebra) :)

[Eric Wieser]

Though indeed the development towards that result uses the submodule spelling

[Sophie Morel]

Richard Copley said:

Re defining a norm, in case it's helpful (probably not!) I'll mention the inner product space defined on an exterior power of a finite-dimensional inner product space via the Gram determinant, as described here on Wikipedia.

I do have a definition of the norm written down in my own project, and it works fine, but it only gives the universal property of the normed exterior powers for alternating maps into the base field, which is not good. I know how to fix this, but I will have to play with universes and I'm a bit afraid.

[Sophie Morel]

If one works over $\mathbb{R}$ (or $\mathbb{C}$), then the definition I already have and the one I want to have will give the same result, thanks to the Hahn-Banach theorem. So my real concern is things like non spherically complete fields.

[Sophie Morel]

Eric Wieser said:

I would like to be able to say that the exterior algebra is the direct sum of all the exterior powers,

We already have that result stated for types, it's docs#DirectSum.decomposeAlgEquiv (via docs#ExteriorAlgebra.gradedAlgebra) :)

You're right, I confused myself. Anyway, I should not vote, because right now I want to choose the solution that will give me less work (i.e. keeping exterior powers as submodules), but that might not be the best choice in the long term.

[Eric Wieser]

I think that's an ok answer for the context of your PR, in which case the short-term solution is to rename ExteriorPower to exteriorPower or ExteriorAlgebra.powers

[Sophie Morel]

It was initially called ExteriorAlgebra.gradedPiece...
But then, what do I do with all the notation that has ExteriorPower as a prefix, like ExteriorPower.ιMultior ExteriorPower.map ? Is it okay to call them exteriorPower.ιMultietc ? I cannot pretend that I totally understand the naming conventions.

[Eric Wieser]

I think docs#unitary is probably the best example to copy

[Sophie Morel]

Thanks ! So according to this, exteriorPower.map would definitely be allowed.

[Sophie Morel]

Still haven't figured out what's causing the timeouts in ExterirAlgebra/Grading.lean in this branch where I introduce and use the notation for exterior powers earlier. (I set the maximum number of heartbeats to 5000000 and it still timeouts, so I don't think it's just slowness, Lean really has trouble guessing something but as usual it just tells me (deterministic) timeout at 'isDefEq'.)

[Sophie Morel]

Okay, apparently the problem is that Lean can't figure out the DirectSum.GSemiring structure when I use the notation, even if I explicitely tell it that all the (Λ[R]^i) M are submodules of the exterior algebra. Now I have to figure the exact incantation to make it create that instance, but I can't even find the definition of the instance...

[Kevin Buzzard]

yeah I've been looking at this too, on the face of it it just looks like you've introduced a new notation and then randomly things break. Sounds like you've got further than me, but perhaps it's worth saying that the porting note which was there already

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in

is already an indication that something weird is going on. I remember Amelia having terrible trouble with exterior powers years ago.

[Sophie Morel]

Well I'm too tired to think about it tonight, so I'll just go to bed and hope things make more sense tomorrow.

[Kevin Buzzard]

Here's the issue on master: maybe I'm missing something obvious, but adding an abbrev for LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i stops a once-working declaration from compiling.

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.Basic

namespace ExteriorAlgebra

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

section working

open scoped DirectSum

protected def GradedAlgebra.ι :
    M →ₗ[R] ⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i) :=
  DirectSum.lof R ℕ (fun i => ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) 1 ∘ₗ
    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in
theorem GradedAlgebra.ι_sq_zero (m : M) : GradedAlgebra.ι R M m * GradedAlgebra.ι R M m = 0 := by
  sorry

end working

section this_breaks_it

abbrev ExteriorPower := (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)

end this_breaks_it

section not_working_any_more

open scoped DirectSum

protected def brokenGradedAlgebra.ι :
    M →ₗ[R] ⨁ i : ℕ, ↥(ExteriorPower R i M) :=
  DirectSum.lof R ℕ (fun i => ↥(ExteriorPower R i M)) 1 ∘ₗ
    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in
theorem brokenGradedAlgebra.ι_sq_zero (m : M) : brokenGradedAlgebra.ι R M m * brokenGradedAlgebra.ι R M m = 0 := by
  sorry -- deterministic timeout

end not_working_any_more

[Sophie Morel]

Tensor powers have an explicitely defined DirectSum.GSemiring instance on them (cf this), so maybe that's the solution here ? I just don't know if it would break other stuff.

[Sophie Morel]

For example, this gets rid of the timeout (of course it's cheating):

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.Basic

namespace ExteriorAlgebra

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

section working

open scoped DirectSum

protected def GradedAlgebra.ι :
    M →ₗ[R] ⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i) :=
  DirectSum.lof R ℕ (fun i => ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) 1 ∘ₗ
    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in
theorem GradedAlgebra.ι_sq_zero (m : M) : GradedAlgebra.ι R M m * GradedAlgebra.ι R M m = 0 := by
  sorry

end working

section this_breaks_it

abbrev ExteriorPower := (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)

end this_breaks_it

section not_working_any_more

open scoped DirectSum

protected def brokenGradedAlgebra.ι :
    M →ₗ[R] ⨁ i : ℕ, ↥(ExteriorPower R i M) :=
  DirectSum.lof R ℕ (fun i => ↥(ExteriorPower R i M)) 1 ∘ₗ
    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m

instance annoying : DirectSum.GSemiring (fun (i : ℕ)  ↦  ExteriorPower R i M) := sorry

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in
theorem brokenGradedAlgebra.ι_sq_zero (m : M) : brokenGradedAlgebra.ι R M m * brokenGradedAlgebra.ι R M m = 0 := by
  sorry -- deterministic timeout

end not_working_any_more

[Sophie Morel]

Also the doc of DirectSum/Ring says that it provides helper functions such as DirectSum.GSemiring.ofSubmodules to construct DirectSum.GSemiring instances, but I cannot locate this helper functions in mathlib (using the site search or moogle). Maybe the names changed and the doc was not updated ?

[Sophie Morel]

I found the relevant instance that Lean needs to be reminded of, it's called Submodule.nat_power_gradedMonoid. This gets rid of the timeout:

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.Basic

namespace ExteriorAlgebra

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

section working

open scoped DirectSum

protected def GradedAlgebra.ι :
    M →ₗ[R] ⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i) :=
  DirectSum.lof R ℕ (fun i => ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) 1 ∘ₗ
    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in
theorem GradedAlgebra.ι_sq_zero (m : M) : GradedAlgebra.ι R M m * GradedAlgebra.ι R M m = 0 := by
  sorry

end working

section this_breaks_it

abbrev ExteriorPower := (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)

end this_breaks_it

section not_working_any_more

open scoped DirectSum

protected def brokenGradedAlgebra.ι :
    M →ₗ[R] ⨁ i : ℕ, ↥(ExteriorPower R i M) :=
  DirectSum.lof R ℕ (fun i => ↥(ExteriorPower R i M)) 1 ∘ₗ
    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m

instance why : SetLike.GradedMonoid fun (i : ℕ) ↦ (ExteriorPower R i M) :=
  Submodule.nat_power_gradedMonoid (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in
theorem brokenGradedAlgebra.ι_sq_zero (m : M) : brokenGradedAlgebra.ι R M m * brokenGradedAlgebra.ι R M m = 0 := by
  sorry

end not_working_any_more

However, maybe there is a better way to remind Lean that the instance exists, such as what was done here:

-- Porting note: Lean needs to be reminded of this instance otherwise it cannot
-- synthesize 0 in the next theorem
attribute [instance 1100] MulZeroClass.toZero in

[Kevin Buzzard]

Oh nice catch! There is something seriously borked about these direct sums. I've seen this sort of thing before -- an import screws things up. This works fine:

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
-- import Mathlib.RingTheory.GradedAlgebra.Basic

open ExteriorAlgebra DirectSum

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

#synth Zero (⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i))

but if you uncomment the second import then the zero can't be found any more. So there's some bad instance being imported: I'll look further.

[Kevin Buzzard]

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.Basic

open ExteriorAlgebra DirectSum

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

attribute [-instance] SetLike.gcommSemiring -- :-/
attribute [-instance] SetLike.gcommRing     -- :-/

#synth Zero (⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) -- now works

[Kevin Buzzard]

These instances are used in RingTheory.MvPolynomial.Homogeneous :-/ (in an example?!) Comment out that example, and change the two instances above to defs, and mathlib compiles fine :-)

[Eric Wieser]

Those are definitely supposed to be instances!

[Kevin Buzzard]

Yes, unfortunately this is what I thought too, and right now I'm struggling to figure out why they're causing a problem, because if a typeclass search times out (as opposed to failing) then I can't work out how to see the instance trace. I'm wondering if they're causing some kind of loop?

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.Basic

open ExteriorAlgebra DirectSum

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

--attribute [-instance] SetLike.gcommSemiring -- :-/
--attribute [-instance] SetLike.gcommRing     -- :-/

#synth AddCommGroup (⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) -- works

set_option maxHeartbeats 0 in
 -- seems to hang, no trace accessible
#synth Zero (⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i))

[Eric Wieser]

I will have a lot more time to look at this next week than I do this week

[Kevin Buzzard]

I guess I will have a lot less time next week because I'll have to read your thesis?

[Matthew Ballard]

My guess: too many XClass classes are available. Is there a way to manage this in a local way?

[Kevin Buzzard]

I've disproved my loop conjecture:

set_option maxHeartbeats 0 in
set_option synthInstance.maxHeartbeats 0 in
set_option profiler true in
#synth Zero (⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) -- works

and

typeclass inference of Zero took 608s

(on my fast machine!)

[Kevin Buzzard]

I don't understand the trace at all.

[Kevin Buzzard]

import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.Basic

namespace ExteriorAlgebra

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

open scoped DirectSum

abbrev ExteriorPower := (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)

#synth Zero (⨁ i : ℕ, ↥(ExteriorPower R i M))  -- no
#synth AddCommGroup (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes
#synth NonUnitalNonAssocRing (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- no

attribute [-instance] SetLike.gcommSemiring
attribute [-instance] SetLike.gcommRing

#synth Zero (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes
#synth AddCommGroup (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes
#synth NonUnitalNonAssocRing (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- no

instance why : SetLike.GradedMonoid fun (i : ℕ) ↦ (ExteriorPower R i M) :=
  Submodule.nat_power_gradedMonoid (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))

#synth Zero (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes
#synth AddCommGroup (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes
#synth NonUnitalNonAssocRing (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes

attribute [instance] SetLike.gcommSemiring
attribute [instance] SetLike.gcommRing

#synth Zero (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- no
#synth AddCommGroup (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes
#synth NonUnitalNonAssocRing (⨁ i : ℕ, ↥(ExteriorPower R i M)) -- yes

[Matthew Ballard]

This looks quite unpleasant. I will take a closer look tomorrow (or on the flight to SF tonight maybe)

[Kevin Buzzard]

What's frustrating is that I cannot extract a trace in the failing cases. Note that some of the no's might become yes's if you leave lean on for ten minutes with all heartbeats on +infty, but I don't know how to get a trace even in that situation.

[Sophie Morel]

By the way, the definition of exterior powers (and notation for them) is now split off in PR #10744.

[Antoine Chambert-Loir]

I didn't take the time to have a look at Sophie's file, but with @María Inés de Frutos Fernández , we managed to prove that for the divided power algebra (which has one advantage on the exterior algebra, namely it is commutative). You can have a look on github, in case it helps…
DividedPowers/DPAlgebra/Graded/Basic.lean

[Eric Wieser]

@Antoine Chambert-Loir, the grading of the exterior algebra is already in mathlib at docs#ExteriorAlgebra.gradedAlgebra, and has been for some time!

[Sophie Morel]

Yes, the problem is, as far as I can tell, that once you introduce a notation for the graded pieces Lean becomes unable to synthesize some instances. But the grading was already there.

[Kevin Buzzard]

And the meta-problem is that it's also (at least as far as I'm concerned) extremely difficult to see why Lean becomes unable to synthesize them, because it won't give out traces on failures.

[Matthew Ballard]

branch#mrb/ext_alg_testing has something that is close to the cutoff. It’s still over because the search space is too big.

[Matthew Ballard]

Synthesizing Zero is down to 21000 heartbeats and the instance why is necessary because Lean only has GradedRing.toGradedMonoid in the cache for a SetLike.GradedMonoid. Some foApprox and constApprox errors have popped up.

[Matthew Ballard]

Maybe unrelated but every diamond test around this part of the library of the form

example : (algebraNat : Algebra ℕ (FreeAlgebra S X)) = instAlgebra _ _ := rfl

fails with with_reducible_and_instances

[Eric Wieser]

Presumably due to the use of RingHom.comp in the definitions?

[Yury G. Kudryashov]

Should we drop cast from Algebra definition to reduce diamonds?

[Eric Wieser]

I don't understand the question

[Yury G. Kudryashov]

Currently docs#Algebra has a RingHom in its definition. We can drop it, formulate axioms in terms of SMul, then define a RingHom projection as a • 1 and prove (non-defeq) lemmas about equality to Nat.cast etc.

[Eric Wieser]

I think setting toFun manually to avoid diamonds is probably a better solution

[Eric Wieser]

At some point we'll find we want a casting function for non-unital semirings, and then the smul approach fails

[Matthew Ballard]

Eric Wieser said:

Presumably due to the use of RingHom.comp in the definitions?

I think so but I couldn’t completely isolate it with the time I had

[Sophie Morel]

Okay, any advice on what I should do about PR #10744 ? That's the PR where I introduce the ExteriorPower abbreviation (and notation for it) as early as possible, it broke some stuff in LinearAlgebra/ExteriorAlgebra/Grading for some reasons that, to be quite frank, I still don't understand, I fixed the broken stuff by manually defining an instance that before was automatically synthesized by Lean, but I don't know if that was The Right Way to do it, because all that instances stuff is basically black magic to me.
And now that PR is blocking PR #10654 that was actually doing things with exterior powers, so I'm kind of regretting the fact that I created it at all.

[Patrick Massot]

@Eric Wieser ?

[Eric Wieser]

I'll look at this in a few hours. Shortcut instances are fairly benign for fixing typeclass issues, so the workaround you describe is probably fine

[Matthew Ballard]

I think it is ok. We really need a global tag or issue or something for “why do I need this instance?”

[Eric Wieser]

I pushed some changes, notably fixing the notation to be Λ[R]^n M not (Λ[R]^n) M

[Eric Wieser]

#11062 makes the same change for docs#TensorPower

[Richard Copley]

Should it be a \bigwedge rather than a \Lambda? (Same question for AlternatingMap.)

[Richard Copley]

One example (wikipedia)

The {{math|''k''}}th '''exterior power''' of {{tmath|V}}, denoted {{tmath|{\textstyle\bigwedge}^{\!k}(V)}}, [...]

(The $k$​th exterior power of $V$, denoted $\bigwedge^k V$, [...])

[Eric Wieser]

Oh nice catch

[Eric Wieser]

So ⋀ not Λ?

[Richard Copley]

Yes

[Richard Copley]

People do use \Lambda, but it's a solecism in my opinion. Not the worst I've seen (there's a textbook that uses a script S for powerset).

[Richard Copley]

Annoying thing to bring up, sorry. Shall I make a PR?

[Richard Copley]

so hard to grep

[Richard Copley]

#11064

[Edit: to denote AlternatingMap R M N ι by M [⋀^ι]→ₗ[R] N (with \bigwedge)]

[Richard Copley]

Ah, silly me: that's only AlternatingMap (ExteriorPower doesn't exist on master yet). I'll edit the description, and I will see if I can edit #10744 (for ExteriorPower). It's probably good to do those two changes separately anyway.

[Richard Copley]

done.

[Edit: edited #10744 to denote exteriorPower R n M by ⋀[R]^n M (with \bigwedge)]

[Richard Copley]

... fixing ...

[Richard Copley]

Richard Copley said:

#11064

[Edit: to denote AlternatingMap R M N ι by M [⋀^ι]→ₗ[R] N (with \bigwedge)]

Build succeeded, lint failed. I touched it, so I need to add a docstring.

[Richard Copley]

Where "it" is ContinuousAlternatingMap (in "Mathlib.Topology.Algebra.Module.Alternating.Basic"). The linter error is

/- The docBlame linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
Error: ./././Mathlib/Topology/Algebra/Module/Alternating/Basic.lean:46:1: error: term_[⋀^_]→L[_]_ definition missing documentation string

I don't understand this. I'll keep looking.

[Richard Copley]

No, I don't get it, and it's too late at night for me to think about it now.

State of affairs: #10744 (exteriorPower) is :green:, and no one needs to rush to think about #11064 (AlternatingMap).

[Patrick Massot]

@Richard Copley I just pushed a commit that should fix this issue.

[Sophie Morel]

Eric Wieser said:

I pushed some changes, notably fixing the notation to be Λ[R]^n M not (Λ[R]^n) M

Thanks ! I wanted to do that but didn't know how to (I just copied the notation from the tensor power file, because I don't know how to define this kind of notation myself).