Symbolic square matrices

Stream: new members

[Robert Maxton]

Switching gears from my other project... I'd like to use Lean to check my work with/potentially automate operator arithmetic. Things like quantum mechanics, where I would like to be able to be sure I haven't dropped a commutator somewhere

[Robert Maxton]

It seems like I can do this by declaring a generic, noncommutative star_ring and using it to make a star_algebra, maybe? Of whatever operators over C

[Robert Maxton]

but my operators need to be "square", when I take their transpose/star they should be the same kind of object

[Robert Maxton]

I think this means somehow telling lean that mul_opposite A is not just equiv to but actually equal to A, but I'm not entirely sure how to do that safely/rigorously...

[Frédéric Dupuis]

This should be pretty straightforward actually: square matrices have a ring instance on them, so things like addition and multiplication will just work out of the box.

[Frédéric Dupuis]

If you want a more abstract setting, you can see in analysis/normed_space/star/basic how to declare a C*-algebra, and all those operations should also just work.

[Jireh Loreaux]

Yeah, this should "just work". Be aware of tactic#noncomm_ring which can help you proving some of the arithmetic.

[Frédéric Dupuis]

Actually we do have an example from quantum mechanics that might be relevant: docs#CHSH_inequality_of_comm.

[Robert Maxton]

ooh, I'll have to take a look

[Robert Maxton]

and yeah my worry is that the "matrices" I'm working with are continuous-indexed/uncountably infinite, and that can blow things up sometimes

[Robert Maxton]

notably anything to do with traces and determinants

[Jireh Loreaux]

oh, hold on, can you be more specific about exactly what you want to do? Indexing matrices by arbitrary types is fine, but I'm pretty sure we only have traces and determinants if the index types are fintypes.

[Robert Maxton]

I probably wouldn't be doing anything with them, I just don't have an encyclopedic knowledge of what results depend on them

[Robert Maxton]

though it would be cool if Lean could magic up a definition for functional determinants out of nowhere :V

[Jireh Loreaux]

I think we're rather a long way off before we can define functional determinants.

[Eric Wieser]

Right now docs#matrix.has_mul requires a finite index type, as does docs#matrix.det

[Robert Maxton]

well, I'm going the C* route for now

[Robert Maxton]

but unfortunately it doesn't seem to recognize that 1 • 1 = 1 when 1: ℂ

[Robert Maxton]

okay, it looks like it was because I had extraneous information/multiple copies of various typeclasses

[Robert Maxton]

weird way of telling me tho