Conversation
|
I'm not sure if |
|
Since I intend to work more with the classification of quadratic forms in the future, I think it is a good idea to make a quadratic form folder and a new file for the classification of quadratic forms since the file is getting quite long. What do you think @eric-wieser? I can keep it in one file if you think its a bad idea. |
|
Splitting files is fine, but usually best if done in its own PR |
jcommelin
added
awaiting-author
| mk_apply smul_group_linear_independent smul_group_span_eq_top i | ||
|
|
||
| -- This lemma cannot be proved with `smul_group_linear_independent` since the action of | ||
| -- `units R` on `R` is not commutative. |
There was a problem hiding this comment.
Are you sure this comment is still true?
There was a problem hiding this comment.
I tried but failed to prove smul_group_linear_independent without the smul_comm_class instance. Though I don't know if the problem is just with my method
There was a problem hiding this comment.
I thought I provided the instance in the other PR; what instance specifically is missing?
There was a problem hiding this comment.
I don't think this instance is true: smul_comm_class (units R) R M
There was a problem hiding this comment.
I suspect smul_group_linear_independent can be proved without the smul_comm_class G R M instance though I couldn't figure out how to do it :/
There was a problem hiding this comment.
I'll have a go tomorrow to see if I missed something
There was a problem hiding this comment.
Can you just adapt the units proof to work for an arbitrary group?
There was a problem hiding this comment.
The proof of the units version uses the smul action of R on units R but we don't have the corresponding action of R on G in the group version
There was a problem hiding this comment.
The proof of the units version uses the smul action of R on units R
There can be no such action - it actually seems to be using the action of opposite (units R) on R (which is easy to make exist), which I'm having a headache trying to generalize.
| -- This lemma cannot be proved with `smul_group_linear_independent` since the action of | ||
| -- `units R` on `R` is not commutative. |
There was a problem hiding this comment.
I think the generalization we're missing here is maybe about right actions. I think the key step in the proof is solving
(g x •← w x) • v x = g x • (w x • v x)where notation a ` •← ` b := op b • a, and the action r •← u is defined using #7723 as
instance (R) [semiring R] : distrib_mul_action (units R)ᵒᵖ R :=
distrib_mul_action.comp_hom R (units.op_equiv.symm : (units R)ᵒᵖ ≃* _).to_monoid_homTo complete this generalization, we'd need a variable of smul_assoc that covers (g x •← w x) • v x = g x • w x • v x, which is definitely out of scope for this PR.
eric-wieser
left a comment
eric-wieser
left a comment
There was a problem hiding this comment.
All the units stuff looks good to me now, thanks. Perhaps @jcommelin or @Vierkantor should skim this one last time.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
| the sum of squares, i.e. `weighted_sum_squares` with weight `λ i : ι, 1`. -/ | ||
| theorem equivalent_sum_squares {M : Type*} [add_comm_group M] [module ℂ M] | ||
| [finite_dimensional ℂ M] (Q : quadratic_form ℂ M) (hQ : (associated Q).nondegenerate) : | ||
| equivalent Q (weighted_sum_squares ℂ (1 : fin (finite_dimensional.finrank ℂ M) → ℂ)) := |
There was a problem hiding this comment.
I still think that it would be nice to be able to write
equivalent Q (sum_squares ℂ (fin (finite_dimensional.finrank ℂ M)))
github-actions
Bot
added
ready-to-merge
…aw of inertia (#7416) Every nondegenerate complex quadratic form is equivalent to a quadratic form corresponding to the sum of squares.
|
Build failed (retrying...): |
…aw of inertia (#7416) Every nondegenerate complex quadratic form is equivalent to a quadratic form corresponding to the sum of squares.
|
Pull request successfully merged into master. Build succeeded: |
bors
Bot
changed the title
4 participants
Every nondegenerate complex quadratic form is equivalent to a quadratic form corresponding to the sum of squares.