Finitary scalar product

Stream: Is there code for X?

[Yaël Dillies]

Is there anything to scalar multiply something by finitely many scalars not necessarily living in the same domain?

import data.finset.basic
import group_theory.group_action.defs

variables {ι β : Type*} {α : ι → Type*} [Π i, has_scalar (α i) β]
  [Π i j, smul_comm_class (α i) (α j) β]

-- Morally `(∏ i in s, a i) • b`
def finset.scalar_prod (s : finset ι) (a : Π i, α i) : β → β := sorry

[Yaël Dillies]

This is probably a question for you, @Eric Wieser

[Anne Baanen]

i don't recall this one, but you should be able to build this out of docs#finset.fold, right?

[Yaël Dillies]

Can I? My ops are α i → β → β, not β → β → β.

[Anne Baanen]

Ah right, it's not quite as easy because it has to be commutative too.

[Anne Baanen]

But something like this should still work: (s.map (λ i, (• a i))).fold (∘))

[Anne Baanen]

Except of course you can't use finset.map because you can't prove that the a is are distinct.

[Yaël Dillies]

But (∘) isn't commutative either :thinking:

[Anne Baanen]

Good point, it is commutative on the image but not on the whole of its domain which is what fold requires.

[Anne Baanen]

My suggestion is then to define it using list.foldr and manually lift it through multiset to finset.

[Yaël Dillies]

Let me drop this missing instance here

instance {α : Type*} : is_associative (α → α) (∘) := ⟨λ f g h, rfl⟩

[Yaël Dillies]

But does that not mean that our finset.fold is not general enough? Or is the additional generality a pain to take care of?

[Yaël Dillies]

Is it the same story as docs#finset.noncomm_prod? Should we define finset.noncomm_fold?

[Yaël Dillies]

cc @Yakov Pechersky then

[Anne Baanen]

Yaël Dillies said:

But does that not mean that our finset.fold is not general enough? Or is the additional generality a pain to take care of?

We need to add a version of docs#left_commutative which is restricted to a {fin,multi,}set. Then we should be able to state it in the required generality.

[Yaël Dillies]

set.left_commutative?

[Anne Baanen]

Or set.left_comm_on, cf. docs#set.inj_on

[Yakov Pechersky]

Does it work for you if you use multiset.noncomm_foldr?

[Yaël Dillies]

Would be happy with this.

[Yaël Dillies]

Oh, do we have all missing ingredients except the finset lift restriction?

[Yakov Pechersky]

Since you're folding, you can use multiset

[Yaël Dillies]

Why so?

[Yakov Pechersky]

Except of course you can't use finset.map because you can't prove that the a is are distinct.

You don't have to prove so when you're folding a multiset

[Yakov Pechersky]

Regarding the associativity though, that is a generalization you'd need

[Anne Baanen]

Yaël Dillies said:

Why so?

Since finset is a subtype of multiset.

[Yakov Pechersky]

multiset.nonassoc_foldr

[Yakov Pechersky]

But right now, multiset.noncomm_foldr makes no typeclass assumptions on the domain or codomain

[Yakov Pechersky]

It just requires a proof obligation of left commutativity

[Yaël Dillies]

Ah right, docs#is_associative is annoyingly restricted to α → α → α.

[Yaël Dillies]

Anne Baanen said:

Yaël Dillies said:

Why so?

Since finset is a subtype of multiset.

Sorry, I should have made it clearer. Why not defining the finset version when we have a bunch of duplicates already, like docs#finset.prod.

[Anne Baanen]

Ah yes, please also define it for finset!

[Yaël Dillies]

Okay so what is there to do?

• Define set.left_comm_on
• Lift multiset.noncomm_fold to finset.noncomm_fold (and same for _right)

[Yaël Dillies]

Yakov Pechersky said:

Regarding the associativity though, that is a generalization you'd need

I don't understand this, though.

[Yaël Dillies]

Do you mean generalizing is_associative?

[Eric Wieser]

import data.finset.noncomm_prod

variables {ι β : Type*} {α : ι → Type*} [Π i, has_scalar (α i) β]
  [Π i j, smul_comm_class (α i) (α j) β]

/-- As endomorphisms with multiplication as composition, `((•) a)` and `((•) b)` commute. -/
lemma smul_End_commute {α β γ} [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ]
  (a : α) (b : β) :
  @commute (function.End γ) _ ((•) a) ((•) b) :=
funext (smul_comm _ _)

-- Morally `(∏ i in s, a i) • b`
def multiset.scalar_prod (s : multiset ι) (a : Π i, α i) : β → β :=
show function.End β, from
multiset.noncomm_prod (s.map (λ i, ((•) (a i)))) $ λ x hx y hy, begin
  rw multiset.mem_map at hx hy,
  obtain ⟨x, _, rfl⟩ := hx,
  obtain ⟨y, _, rfl⟩ := hy,
  exact smul_End_commute _ _,
end

-- Morally `(∏ i in s, a i) • b`
def finset.scalar_prod (s : finset ι) (a : Π i, α i) : β → β :=
s.val.scalar_prod a

[Eric Wieser]

You can play a huge number of tricks by working in endomorphism monoids