Proposal: Symmetric Tensor Power

Stream: mathlib4

[Kenny Lau]

In the process of thinking about generalisations of affine space and projective space, it has occurred to me that perhaps defining the symmetric tensor powers of a module might be beneficial.

If M is an R-module and n is a natural number (perhaps can be an arbitrary fintype), then Sym^n(M) is the n-th tensor power of M, quotient out by the relation that x1 ⊗ₜ x2 ⊗ₜ ... ⊗ₜ xn = that but reorder the indices. (Do we have generalisation of quotients to monoids yet? I've deliberately avoided the use of subtraction.) (Sym^0(M) = R.)

Then, ⊕_n Sym^n(M) has the structure of a graded R-algebra. It is actually the left adjoint of the forgetful functor R-Alg ⥤ R-Mod.

Currently MvPolynomial σ R is actually a special case of this, for M = free module generated by σ. Note that this grading agrees with the homogeneous grading.

Typing this, I realised that it is possible to do this by passing through MvPolynomial σ R, since any module is a quotient of a free module. So I suppose I would like to also discuss the merits of this alternative construction. (Actually, I've heard that this pathway would depend on a pending PR?)

This thread also serves to gauge the interest of the community in this construction. If enough people are interested, then I'll try to come up with the basic definition and make a small PR.

[Kenny Lau]

I'll split the part about quotient of a monoid to a separate thread.

[Anatole Dedecker]

Is this docs#SymmetricAlgebra ?

[Anatole Dedecker]

docs#SymmetricAlgebra.lift is the universal property you want

[Kenny Lau]

@Anatole Dedecker aha, that is indeed the "global" version, but I suspect that by throwing away some work, it might be harder to recover a grading from the algebra... unless there's a smart trick somehow

[Kenny Lau]

by global I mean that you have sidestepped the Sym^n(R) construction and went directly for the graded algebra

[Kenny Lau]

I suspect we can still do this by first showing that the commutativity relation on the tensor algebra (which is the version for R-Alg without commutativity condition) is "homogeneous"...

[Anatole Dedecker]

I don’t know the state of the grading API, but in theory you should be able to just say that the ideal is homogeneous right ? That said maybe it’s not ideal in some setups when we need one fixed n

[Kenny Lau]

there's also a universal property satisfied by Sym^n(M): maps from that is equivalent to symmetric n-linear functions

[Kenny Lau]

there is also a "sanity check" that Sym^k(R^n) is a free module of dimension (n+k-1) choose k

[Kenny Lau]

it is also functorial and respects base change

[Kenny Lau]

Anatole Dedecker said:

I don’t know the state of the grading API, but in theory you should be able to just say that the ideal is homogeneous right ? That said maybe it’s not ideal in some setups when we need one fixed n

What's the generalisation of ideal called? If we're working with monoids

[Kenny Lau]

I guess I could call it "congruence"

[Kenny Lau]

I don't know, it's theoretically possible since the definition is mathematically correct, but I feel like we might have thrown too much work away.

[Kenny Lau]

Honestly, everything could indeed work out, but I'm not very confident that this is the "correct" approach... whatever "correct" even means

[Junyan Xu]

It's also the approach taken by ExteriorAlgebra and the universal property is available as ExteriorAlgebra.liftAlternatingEquiv exteriorPower.alternatingMapLinearEquiv; maybe you can mimic the proof. Bases of the exterior powers is at #18771.

Homogeneous relations were PR'd as #22279.

[Kenny Lau]

aha that's the pending PR, i'll wait for that PR then

[Notification Bot]

Kenny Lau has marked this topic as resolved.

[Kenny Lau]

@Junyan Xu actually, what do you think? which pathway is better? a direct construction, or via the grading and homogeneous quotient?

[Kenny Lau]

I suspect it wouldn't actually be hard to construct it by hand, i could probably do it in 20 lines

[Kenny Lau]

import Mathlib

universe u v

open TensorProduct Equiv

variable (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ)

inductive SymmetricPower.Rel : ⨂[R]^n M → ⨂[R]^n M → Prop
  | perm : (e : Perm (Fin n)) → (f : Fin n → M) → Rel (⨂ₜ[R] i, f i) (⨂ₜ[R] i, f (e i))

def SymmetricPower (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M]
    (n : ℕ) : Type max u v :=
  AddCon.Quotient (addConGen (SymmetricPower.Rel R M n))

[Kenny Lau]

This is the direct construction.

[Notification Bot]

Kenny Lau has marked this topic as unresolved.

[Junyan Xu]

I think both have their own advantages and make different things easier to prove. It's nice that the "indirect" approach via RingCon only requires relations in degree 2, for example.

[Joël Riou]

Whichever approach we end up choosing, we should try to have a coherent API. The way I am personaly thinking about the symmetric algebra is as the direct sum of the symmetric powers (defined as you suggest), and there, using the universal property of each symmetric power as a module, we can deduce that the symmetric algebra satisfies a universal property as a graded algebra. I do not know how to prove the universal property of the individual symmetric powers if we start from the full symmetric algebra.

[Kenny Lau]

@Joël Riou (the symmetric algebra is already in mathlib using the "indirect" approach)

[Joël Riou]

Yes, so the question is: if we keep this definition, and define the symmetric nth power as the submodule generated by n-uple products, how do we show that it satisfies the universal property it should satisfy as a module. If we cannot, we may consider changing the definitions?

[Junyan Xu]

You coauthored #18590 and you think the symmetric power version is much different from the exterior power version?

[Kenny Lau]

import Mathlib

universe u v

open TensorProduct Equiv

variable (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (n : ℕ)

inductive SymmetricPower.Rel : ⨂[R]^n M → ⨂[R]^n M → Prop
  | perm : (e : Perm (Fin n)) → (f : Fin n → M) → Rel (⨂ₜ[R] i, f i) (⨂ₜ[R] i, f (e i))

def SymmetricPower (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M]
    (n : ℕ) : Type max u v :=
  AddCon.Quotient (addConGen (SymmetricPower.Rel R M n))

namespace SymmetricPower

instance foo : AddCommMonoid (SymmetricPower R M n) := AddCon.addCommMonoid _

lemma smul (r : R) (x y : ⨂[R]^n M) (h : addConGen (Rel R M n) x y) :
    addConGen (Rel R M n) (r • x) (r • y) := by
  induction h with
  | of x y h => cases h with
    | perm e f => cases n with
      | zero => convert (addConGen (Rel R M 0)).refl _
      | succ n =>
          convert AddConGen.Rel.of _ _ (Rel.perm (R := R) e (Function.update f 0 (r • f 0)))
          · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
          · simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul,
              ← Function.update_comp_equiv, Function.update_eq_self]; rfl
  | refl => exact AddCon.refl ..
  | symm => apply AddCon.symm; assumption
  | trans => apply AddCon.trans <;> assumption
  | add => rw [smul_add, smul_add]; apply AddCon.add <;> assumption

def smul' (r : R) : SymmetricPower R M n →+ SymmetricPower R M n :=
  AddCon.lift _ (AddMonoidHom.comp (AddCon.mk' _) {
      toFun := (r • ·)
      map_zero' := smul_zero r
      map_add' := smul_add r })
    (fun x y h ↦ Quotient.sound (smul R M n r x y h))

end SymmetricPower

[Kenny Lau]

I've written more code in case it's useful later

[Kenny Lau]

The module stuff should be generalised first (see #mathlib4 > Proposal: Quotient of monoid)

[Kenny Lau]

/poll Which pathway would you prefer?
Direct construction: pending smul on congruence
Indirect construction via symmetric algebra: pending homogeneous quotient

[Kenny Lau]

Let's put it to a vote.

[Joël Riou]

Junyan Xu said:

You coauthored #18590 and you think the symmetric power version is much different from the exterior power version?

Then, I only deduced the categorical formulation from the unbundled formulation (the proof of which I did not study...).

[Kenny Lau]

#26192 created

[Scott Carnahan]

Why not define symmetric powers as in your PR and the symmetric algebra as the quotient of the tensor algebra, then construct the (natural) isomorphism?

[Kenny Lau]

Scott Carnahan said:

Why not define symmetric powers as in your PR and the symmetric algebra as the quotient of the tensor algebra, then construct the (natural) isomorphism?

How do you construct the map from the other side?

[Scott Carnahan]

Do you mean the map from the degree n part of the symmetric algebra to the nth symmetric power? My guess for a first step would be to show that both are quotients of the degree n part of the tensor algebra, on one hand identifying it with the nth tensor power and on the other using the homogeneity of the quotient map of algebras.

[Wang Jingting]

Kenny Lau said:

Scott Carnahan said:

Why not define symmetric powers as in your PR and the symmetric algebra as the quotient of the tensor algebra, then construct the (natural) isomorphism?

How do you construct the map from the other side?

I think that can be directly constructed from a graded ringHom from the tensor algebra to the symmetric powers, then take the (graded) RingQuot by the homogeneous relation (defined as xy-yx)? I think that many things still need to done for graded objects (e.g. graded ringHom), but of course we can try to add that.

[Kenny Lau]

@Scott Carnahan @Wang Jingting that's why i said above, this is pending the "homogeneous quotient" PR (#22279)

[Kenny Lau]

#26192 (symmetric tensor power) is now a month old, can we decide if we want Fin n or arbitrary fintype? The latter would likely require a refactor of tensor power as well, and I don't think this PR should be held up by a future refactor.

[Kim Morrison]

It doesn't look like you use TensorPower here at all, so it's not relevant that this is indexed over a Nat. You're already using PiTensorProduct, which is arbitrarily indexed.

[Kenny Lau]

@Kim Morrison ⨂[R]^n M in L41 is TensorPower

[Eric Wieser]

I guess if we really wanted to go nuts here we could have the elements dependently-typed and pass around a family of isomorphisms between every pair too

[Eric Wieser]

(I doubt that's actually a good idea!)

[Eric Wieser]

I think Kim's point is that you could swap that for PiTensorProduct and everything would keep working

[Matthew Ballard]

People happy now?