feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp

[hrmacbeth]

A "matrix" of bilinear forms on M on a type α (possibly infinite) induces a bilinear form on α →₀ M, and thence (via bilin_form.to_quadratic_form a quadratic form. In particular, define the "Euclidean" (sum-of-squares) quadratic form on α →₀ M.

Zulip

---

• depends on: [Merged by Bors] - feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' #6565
• depends on: [Merged by Bors] - feat(linear_algebra/bilinear_form): generalize some constructions to the noncomm case #6824

[eric-wieser]

I wonder if a finsupp.sum₂ definition would be useful here - It could be used here too:

https://github.com/leanprover-community/mathlib/blob/07fc9821f41bd369d930fa9ff8e83e56935e7594/src/algebra/monoid_algebra.lean#L72-L73

and maybe would share some lemmas

[gebner]

Now that we have a better big operator library, I would rather get rid of sum entirely:

instance : has_mul (monoid_algebra k G) :=
⟨λ f g, ∑ i in f.support, ∑ j in g.support, single (i * j) (f i * g j)⟩

maybe would share some lemmas

This is the reason why I'd rather have one definition, and a third of the lemmas.

[Vierkantor]

I agree that finsupp.sum could be profitably replaced with finset.sum, or even finsum. Let's stick to finsupp.sum in this PR, since the linear algebra library uses it consistently throughout (for now).

[eric-wieser]

You might get the add proofs for free if instead of sum you used lift_add_hom, something like:

Suggested change

	{ bilin := λ p q, p.sum (λ i x, q.sum (λ j y, A i j x y)),
	bilin_add_left := bilin_add_left' (λ i j x, ((A i j).left x).to_add_monoid_hom),
	bilin_smul_left := bilin_smul_left' (λ i j x, (A i j).left x),
	bilin_add_right := bilin_add_right' (λ i j x, ((A i j).right x).to_add_monoid_hom),
	bilin_smul_right := bilin_smul_right' (λ i j x, (A i j).right x) }
	{ bilin := λ p q, p.lift_add_hom (λ i, q.lift_add_hom (λ j, (A i j : M →+ M →+ R)),
	bilin_add_left := sorry,
	bilin_smul_left := bilin_smul_left' (λ i j x, (A i j).left x),
	bilin_add_right := sorry,
	bilin_smul_right := bilin_smul_right' (λ i j x, (A i j).right x) }

where A i j : M →+ M →+ R is some missing definition that is really just a weaker version of (A i j).to_lin.

[eric-wieser]

The name of this lemma seems a bit weird, since there's no mention of linearity at all in the statement or proof. Since this is just an auxiliary lemma to build bilin_form_of, can you mark it private, so that the name doesn't matter?

[Vierkantor]

I agree: I would go with either:

Suggested change

	lemma bilin_add_left' (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :
	private lemma bilin_add_left' (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :

or

Suggested change

	lemma bilin_add_left' (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :
	lemma bilin_form_of_add_left_aux (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :

[Vierkantor]

bors d+

[Vierkantor]

I agree: I would go with either:

Suggested change

	lemma bilin_add_left' (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :
	private lemma bilin_add_left' (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :

or

Suggested change

	lemma bilin_add_left' (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :
	lemma bilin_form_of_add_left_aux (A : α → β → N → (M' →+ R)) (p q : α →₀ M') (r : β →₀ N) :

[Vierkantor]

Suggested change

	lemma bilin_add_right' (A : α → β → N → (M' →+ R)) (p : α →₀ N) (q r : β →₀ M') :
	p.sum (λ i x, (q + r).sum (λ j y, A i j x y))
	= p.sum (λ i x, q.sum (λ j y, A i j x y)) + p.sum (λ i x, r.sum (λ j y, A i j x y)) :=
	private lemma bilin_add_right' (A : α → β → N → (M' →+ R)) (p : α →₀ N) (q r : β →₀ M') :
	p.sum (λ i x, (q + r).sum (λ j y, A i j x y))
	= p.sum (λ i x, q.sum (λ j y, A i j x y)) + p.sum (λ i x, r.sum (λ j y, A i j x y)) :=

[Vierkantor]

Suggested change

	lemma bilin_smul_left' (A : α → β → N → (M →ₗ[R] R)) (a : R)
	private lemma bilin_smul_left' (A : α → β → N → (M →ₗ[R] R)) (a : R)

[Vierkantor]

Suggested change

	lemma bilin_smul_right' (A : α → β → N → (M →ₗ[R] R)) (a : R)
	private lemma bilin_smul_right' (A : α → β → N → (M →ₗ[R] R)) (a : R)

[Vierkantor]

Suggested change

	lemma finsupp.is_sym_to_bilinear_form {α : Type*} (A : α → α → (bilin_form R M))
	lemma finsupp.is_sym_bilin_form_of {α : Type*} (A : α → α → (bilin_form R M))

[Vierkantor]

Suggested change

	@[simp] lemma to_quadratic_form_polar_apply (A : α → α → (bilin_form R M))
	@[simp] lemma quadratic_form_of_polar_apply (A : α → α → (bilin_form R M))

[Vierkantor]

I agree that finsupp.sum could be profitably replaced with finset.sum, or even finsum. Let's stick to finsupp.sum in this PR, since the linear algebra library uses it consistently throughout (for now).

[Vierkantor]

I would have expected this proof to be shorter, but can't find an easy way to golf it. So we can keep it as is.

[bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[tb65536]

@hrmacbeth Do you have plans to return to this at some point?

[jcommelin]

@hrmacbeth 🏓

[github-actions]

This PR/issue depends on:

• [Merged by Bors] - feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map' #6565
• [Merged by Bors] - feat(linear_algebra/bilinear_form): generalize some constructions to the noncomm case #6824
  By Dependent Issues (🤖). Happy coding!