Zulip Chat Archive

Stream: new members

Topic: Eigenproperties of symmetric matrices


Gabriel Moise (Apr 21 2021 at 08:04):

Hello! I have been working towards a file that contains properties of symmetric matrices with real coefficients, like the fact that all their eigenvalues are real and each has a corresponding real eigenvector, as I did not see them in the documentation on linear algebra. The thing is that I am not an experienced Lean programmer, and although I tried to make the code as clear as possible and with minimal repeated work, I am not sure that the code is PR-worthy. Another thing is that the whole file is 400-lines and it has a substantial amount of helping lemmas, so it would be hard to review, but I don't know if I can break it into smaller pieces, as statements follow from previous ones and so on. Should I have a "more experienced" opinion on what I wrote and maybe discuss its potential? :smile:

Johan Commelin (Apr 21 2021 at 08:06):

Sure, you can link to your code here. If some of those helper lemmas are really about something slightly more general, you can probably PR those to other files.

Johan Commelin (Apr 21 2021 at 08:06):

And then have a second PR about eigenvalues of symmetric matrices, and such

Gabriel Moise (Apr 21 2021 at 08:13):

https://github.com/gabrielmoise/Lean-work/blob/master/symm_matrix.lean
Yes, some of the lemmas are more general (delimitated them with comments) and would fit into the data.matrix.basic file

Johan Commelin (Apr 21 2021 at 08:15):

The stuff up to line 186 seems generic matrix stuff. So that would make a great first PR. You will have to scatter those lemmas into their natural places in the library, which means you'll be editing 2 or 3 files probably. You might discover some duplicates, I didn't look carefully for those though.

Johan Commelin (Apr 21 2021 at 08:16):

If you are not scared of getting 50 constructive feedback comments on your PR, then I would say "go for it!"

Kevin Buzzard (Apr 21 2021 at 08:18):

Thank you for the module docstring! There is quite a precise format which we ask is followed, and which your docstring doesn't quite match yet: it's here.

Eric Wieser (Apr 21 2021 at 08:18):

I see a number of lemmas there that are hiding in the library already (eg vec_eq_unfold' is docs#funext_iff), but the code certainly looks ready-for-mathlib-review even if not ready-for-mathlib-merge

Eric Wieser (Apr 21 2021 at 08:21):

vec_smul_zero should be covered by docs#pi.no_zero_smul_divisors but perhaps that doesn't exist yet.... You should be able to replace it with docs#smul_eq_zero

Gabriel Moise (Apr 21 2021 at 08:23):

What do you mean by ready-for-mathlib-review? That I should PR it? Btw thanks already for the feedback, it helps a lot :smile:

Eric Wieser (Apr 21 2021 at 08:27):

I meant to backup what @Johan Commelin said about going for a PR if not afraid of 50 or so comments

Kevin Buzzard (Apr 21 2021 at 08:29):

Yes, please PR it :-) And if you don't change the module docstring beforehand then this will be my first comment :-)

Gabriel Moise (Apr 21 2021 at 08:30):

I am doing that right now, hopefully it will be up to the standard.

Eric Wieser (Apr 21 2021 at 08:31):

Another quick thing to address before PRing; take a quick look at #style

Eric Wieser (Apr 21 2021 at 08:31):

Oh. That link doesn't work

Eric Wieser (Apr 21 2021 at 08:31):

Well, what jumps out now is the lack of spaces inside {} and the multiple tactics on a single line

Eric Wieser (Apr 21 2021 at 08:32):

https://leanprover-community.github.io/contribute/style.html#tactic-mode

Eric Wieser (Apr 21 2021 at 08:32):

If you fix those part-way through PRing them github will start hiding comments

Gabriel Moise (Apr 21 2021 at 08:32):

And btw how can I make a PR to an already existing file from mathlib? I should mention that I have an outdated mention of mathlib.

Eric Wieser (Apr 21 2021 at 08:33):

You can create a branch that starts on the version of mathlib you were using

Scott Morrison (Apr 21 2021 at 08:34):

#style hopefully works now?

Johan Commelin (Apr 21 2021 at 08:40):

Eric Wieser said:

I meant to backup what Johan Commelin said about going for a PR if not afraid of 50 or so comments

@Gabriel Moise Note that those 50 comments are standard for everyone who makes a first PR. We all started that way :sweat_smile:

Kevin Buzzard (Apr 21 2021 at 08:43):

@Gabriel Moise to follow up what Eric was sayign abuot {} and lines, here's what your first lemma shoudl look like:

@[simp]
lemma vec_eq_unfold (x y : V  R) : (λ (i : V), x i) = (λ (i : V), y i)   (i : V), x i = y i :=
begin
  split,
  { intros hyp i,
    exact congr_fun hyp i },
  { intro hyp,
    ext i;
    simp [hyp] }
end

Gabriel Moise (Apr 21 2021 at 08:43):

Oh I really want as many comments as possible.
Now I am following some guides on how to make the first PR as I am not very experienced with GitHub either.

Kevin Buzzard (Apr 21 2021 at 08:44):

If you do those fixes (e.g. simp[ -> simp [, repeat{ -> repeat { etc) before you PR then it will save a lot of noise during the PR process.

Kevin Buzzard (Apr 21 2021 at 08:45):

{intro -> { intro. Also you have a non-terminal simp on line 119 and another on line 145 ,148 etc.

Gabriel Moise (Apr 21 2021 at 08:48):

So the goal is to only use simp only when I want to close goals, and not throughout the proof as intermediate steps as well.

Kevin Buzzard (Apr 21 2021 at 09:02):

Right, but there are tricks, eg change simp to squeeze_simp to find out what it actually did, and then do it manually yourself

Gabriel Moise (Apr 21 2021 at 09:19):

Eric Wieser said:

I see a number of lemmas there that are hiding in the library already (eg vec_eq_unfold' is docs#funext_iff), but the code certainly looks ready-for-mathlib-review even if not ready-for-mathlib-merge

This link doesn't work for me.

Johan Commelin (Apr 21 2021 at 09:19):

docs#function.funext_iff

Eric Wieser (Apr 21 2021 at 09:55):

If you're looking for a tiny first PR to practice on, your mul_vec_smul_assoc lemma looks like one that mathlib is missing, and it would go in data/matrix/basic.lean (after addressing your could not turn ℂ into general R comment)

Gabriel Moise (Apr 21 2021 at 10:01):

Eric Wieser said:

If you're looking for a tiny first PR to practice on, your mul_vec_smul_assoc lemma looks like one that mathlib is missing, and it would go in data/matrix/basic.lean (after addressing your could not turn ℂ into general R comment)

Was working on PR-ing the vec_mul_mul_vec_assoc lemma, but thanks for the advice.

Eric Wieser (Apr 21 2021 at 10:05):

That one is probably easier anyway!

Eric Wieser (Apr 21 2021 at 10:14):

Although you can prove it much more succinctly!

Gabriel Moise (Apr 21 2021 at 10:36):

Eric Wieser said:

If you're looking for a tiny first PR to practice on, your mul_vec_smul_assoc lemma looks like one that mathlib is missing, and it would go in data/matrix/basic.lean (after addressing your could not turn ℂ into general R comment)

My problem with (could not turn C into general R) was that I needed to instantiate R with [comm_semigroup R] and then (since I already had [ring R]) some weird interactions happened. Trying to understand the root of the problem, I noticed that:

lemma test_mul_comm {α : Type*} [comm_semigroup α] (a b : α) : a * b = b * a :=
begin
  exact mul_comm a b,
end

lemma test_mul_comm2 {α : Type*} [comm_semigroup α] [ring α] (a b : α) : a * b = b * a :=
begin
  exact mul_comm a b, -- no longer works
end

and this is a little confusing to me.

Kevin Buzzard (Apr 21 2021 at 10:37):

comm_semigroup alpha means "put a commutative semigroup structure on alpha". And ring alpha then means "put a totally unrelated ring structure on alpha (but use the same symbol * for the multiplication)". This is surely not what you want. Do you want comm_ring alpha?

Kevin Buzzard (Apr 21 2021 at 10:40):

If you've proved theorems about rings and then want to prove some more theorems about commutative rings, you could use sections, and have variable assumptions in the sections, e.g.

variable (R : Type*)

section ring_stuff

variable [ring R]

<ringy theorems>

end ring_stuff

section comm_ring_stuff

variable [comm_ring R]

<comm_ringy theorems>

end comm_ring_stuff

Kevin Buzzard (Apr 21 2021 at 10:41):

Alternatively you could let all your rings be called R and all your comm_rings be called A. I tend to do this when I'm doing groups, with groups called G and abelian groups called A.

Gabriel Moise (Apr 21 2021 at 10:45):

Can't I include the comm_ring_stuff section in the ring_stuff section (nesting them) or is it a bad idea?

Johan Commelin (Apr 21 2021 at 11:08):

@Gabriel Moise If you have variables {R : Type*} [ring R] [comm_ring R] then you get two completely unrelated ring structures on R and Lean will get mightily confused.

Johan Commelin (Apr 21 2021 at 11:08):

So nesting will not work.

Gabriel Moise (Apr 21 2021 at 11:30):

Can I get permission to push a branch to mathlib, please? My username is gabrielmoise

Johan Commelin (Apr 21 2021 at 11:35):

Invitation sent: https://github.com/leanprover-community/mathlib/invitations

Gabriel Moise (Apr 21 2021 at 11:54):

Thanks a lot!

Gabriel Moise (Apr 21 2021 at 14:30):

Does the continuous integration / Build mathlib (push) part of the check of a PR generally take a lot?

Eric Rodriguez (Apr 21 2021 at 14:32):

yep ^^

Bryan Gin-ge Chen (Apr 21 2021 at 14:35):

It mostly depends on how deep the changes you've made are in the import graph. A modification to a leaf file will probably compile in a few seconds, but adding stuff to a basic algebra or order file will force a recompilation of almost all of mathlib.

Patrick Massot (Apr 21 2021 at 16:28):

I'm late to the party but I'm extremely worried about trying to merge this into mathlib. Why working with matrices instead of endomorphisms? I think going down the mathematical road (first endomorphisms and then deduce results about matrices if they are needed somewhere) would be much cleaner.

Patrick Massot (Apr 21 2021 at 16:29):

We already have things in https://leanprover-community.github.io/mathlib_docs/linear_algebra/eigenspace.html

Eric Wieser (Apr 21 2021 at 16:36):

Even with that being the case, I think doing this the matrix way will have filled a bunch of lemma gaps in the existing matrix API; we don't have to merge everything to extract value out of this effort

Eric Wieser (Apr 21 2021 at 16:37):

I agree that we should use the endomorphism definitions wherever possible though

Johan Commelin (Apr 21 2021 at 17:02):

I agree with what Patrick said. We definitely don't want to do a whole lot of work on matrices that is better done for endomorphisms first. But I also think that all the helper lemmas that you found are helping to fill out the matrix API.
So when those api gaps are filled, we should discuss here on zulip what is the best way to move forward with the symmetric stuff. It should tie in well with the rest of the library (e.g. the file that Patrick linked to).

Hanting Zhang (Apr 21 2021 at 17:08):

Eric Wieser said:

I agree that we should use the endomorphism definitions wherever possible though

I've always found this weird, but is there any particular reason why docs#linear_map.trace is defined using docs#matrix.trace? It could be defined in terms of the roots of the characteristic polynomial, right? I don't know about infinite dimensional stuff though.

Kevin Buzzard (Apr 21 2021 at 17:38):

And the characteristic polynomial of an endomorphism is presumably defined using the determinant of a matrix? I don't see how you can get away from matrices here.

Hanting Zhang (Apr 21 2021 at 17:45):

Oh, true.

Hanting Zhang (Apr 21 2021 at 17:49):

Wikipedia explains a coordinate-free definition of trace (https://en.wikipedia.org/wiki/Trace_(linear_algebra)#Coordinate-free_definition), so it seems like something can be done?

Kevin Buzzard (Apr 21 2021 at 17:50):

To write down the inverse map Hom(V,V) -> V tensor V^* (necessary to do the computation) you need to pick a basis. The map V tensor V^* -> Hom(V,V) is not a bijection in the infinite-dimensional case (it's an injection, with image the finite rank maps)

Hanting Zhang (Apr 21 2021 at 17:55):

:anguish: Ooh, thanks for clarifying! The assumption is still hidden in there

Kevin Buzzard (Apr 21 2021 at 17:56):

Writing maps from tensor products is easy because of the universal property. To write down a map into a tensor product is a different story; to access all elements of the tensor product you typically need a "model", i.e. a basis for each of the vector spaces, giving you a basis for the tensor product.

Stepan Nesterov (Apr 21 2021 at 17:57):

But there is a coordinate-free definition of determinant via top exterior powers. Then det(1+tA)=1+t*tr(A) in k[t]/(t^2) does the job, right?

Kevin Buzzard (Apr 21 2021 at 17:58):

Models of objects in mathematics are fascinating and I knew nothing about this stuff until I started formalising. The universal property only gets you so far. To prove that the kernel of the canonical map RR[1/S]R\to R[1/S] is the r such that there exists s with rs=0 you don't seem to be able to get this from the universal property alone: you seem to need the explicit model of R[1/S] as R x S / ~. Picking a model for the localisation is like picking a basis for the vector space.

Johan Commelin (Apr 21 2021 at 17:59):

I guess you can push everything into the computation that nVk\bigwedge^n V \cong k if dim(V)=n\dim(V) = n. You will need to use a basis at some point.

Kevin Buzzard (Apr 21 2021 at 17:59):

Yes, in this approach the basis is hidden in the proof that the n'th wedge power is 1-dimensional.

Kevin Buzzard (Apr 21 2021 at 18:01):

Even talking about dimension is problematic if you're not allowed to pick a basis. Dimension is "size of any basis".

Kevin Buzzard (Apr 21 2021 at 18:02):

We need a constructivist to explain to us what's going on. I'll ask on Twitter.

Stepan Nesterov (Apr 21 2021 at 18:04):

We probably need bases at some point in development, but not matrices.
I was just making the point that there is a fancy definition which is independent of a basis by construction.

Stepan Nesterov (Apr 21 2021 at 18:04):

Kevin Buzzard said:

Even talking about dimension is problematic if you're not allowed to pick a basis. Dimension is "size of any basis".

Dimension is a size of a maximal flag of subspaces minus 1 ;)

Johan Commelin (Apr 21 2021 at 18:06):

Aha, and then you prove by induction that the top wedge is 1-dimensional. Sweet.

Kevin Buzzard (Apr 21 2021 at 18:12):

How do you know a maximal flag exists? Wait -- I don't even understand the question. What does it mean to say a vector space is finite-dimensional? Is the definition that it's Noetherian? In which case we might be on to something.

Johan Commelin (Apr 21 2021 at 18:12):

In mathlib finite_dimensional is in terms of noetherian, yes.

Kevin Buzzard (Apr 21 2021 at 18:13):

But how do we know that all max flags have the same size?

Stepan Nesterov (Apr 21 2021 at 18:16):

Kevin Buzzard said:

To write down the inverse map Hom(V,V) -> V tensor V^* (necessary to do the computation) you need to pick a basis. The map V tensor V^* -> Hom(V,V) is not a bijection in the infinite-dimensional case (it's an injection, with image the finite rank maps)

But we don't need to write it down, right? You can characterize the image of id uniquely as the only GL(V)-invariant vector such that the natural pairing V tensor V* sends it to 1.

Stepan Nesterov (Apr 21 2021 at 18:16):

But how do we prove it exists though

Stepan Nesterov (Apr 21 2021 at 18:17):

Developing even basics of representation theory of GL(V), which we do not know to be an algebraic group lacking (g \in GL(V) \iff det(g) \neq 0) seems challenging

Kevin Buzzard (Apr 21 2021 at 18:17):

challenging unless you pick a basis, which I thoroughly recommend doing :-)

Stepan Nesterov (Apr 21 2021 at 18:20):

Kevin Buzzard said:

But how do we know that all max flags have the same size?

Because GL(V) acts transitively on the set of all complete flags by induction

Stepan Nesterov (Apr 21 2021 at 18:20):

It suffices to prove that GL(V) acts transitively on vectors

Stepan Nesterov (Apr 21 2021 at 18:21):

Which you can reduce to the 2-dimensional case

Kevin Buzzard (Apr 21 2021 at 18:21):

I don't think we can induct. I think this is the problem. It's like trying to prove things on fintype by inducting, but not every fintype is equal to a disjoint union of two smaller fintypes.

Kevin Buzzard (Apr 21 2021 at 18:21):

I am still not convinced we can define dimension without picking a basis. For all I know in a Noetherian F-vector space there are flags of arbitrarily large finite length.

Stepan Nesterov (Apr 21 2021 at 18:21):

That's like Noetherian induction in algebraic geometry, yes

Stepan Nesterov (Apr 21 2021 at 18:22):

All proper subtypes ok => type ok

Stepan Nesterov (Apr 21 2021 at 18:23):

Maybe the right proof is to figure out exterior powers and than obtain invariance of dimension as a corollary?

Stepan Nesterov (Apr 21 2021 at 18:23):

When you define determinant by a formula, you don't use that all bases have the same size at all, you just define

Kevin Buzzard (Apr 21 2021 at 18:24):

I'm not sure how to do this in type theory. Coincidentally I was thinking about this today when formalising liquid stuff. We're supposed to be proving a theorem about fintypes by induction on size of the fintype but I realised that this was a bit terrifying because I would need to prove that the truth value of my statement about fintypes factored through the cardinality function.

Adam Topaz (Apr 21 2021 at 18:24):

Another characterization of f.d.v.s. is as the compact objects in the category of vector spaces

Kevin Buzzard (Apr 21 2021 at 18:24):

In the end I decided to switch to finsets.

Kevin Buzzard (Apr 21 2021 at 18:24):

Adam Topaz said:

Another characterization of f.d.v.s. is as the compact objects in the category of vector spaces

This still doesn't give you a well-defined dimension without picking a basis.

Adam Topaz (Apr 21 2021 at 18:25):

The dimension is the trace of the identity morphism

Adam Topaz (Apr 21 2021 at 18:27):

sorry I'm just catching up on this discussion now

Stepan Nesterov (Apr 21 2021 at 18:27):

Adam Topaz said:

The dimension is the trace of the identity morphism

does not work in char p :(

Adam Topaz (Apr 21 2021 at 18:28):

bah take Witt vectors

Adam Topaz (Apr 21 2021 at 18:28):

(obviously that's not a real suggestion, but I'm trying to come up with a basis-free definition like Kevin was asking)

Stepan Nesterov (Apr 21 2021 at 18:29):

What if we define finite-dimensional as V -> V** is surjective?

Adam Topaz (Apr 21 2021 at 18:30):

What's wrong with the compact object definition?

Adam Topaz (Apr 21 2021 at 18:38):

There's this notion of a compact closed monoidal category where objects have duals. If you have some general closed monoidal category which also happens to be locally presentable (and maybe one needs some compatibility with the monoidal structure) is it not the case that the subcategory of compact objects is compact closed monoidal? I couldn't find anything along these lines on the nLab, but I'm sure something along these lines has been written down somewhere...

Adam Topaz (Apr 21 2021 at 18:41):

Oh, and you can define the dimension of a vector space VV over kk as the Krull dimension of SymkV\mathrm{Sym}_k^*V :smile:

Adam Topaz (Apr 21 2021 at 18:41):

(again, not a serious suggestion)

Kevin Buzzard (Apr 21 2021 at 18:41):

The problem with that definition is that a general Noetherian ring might have infinite Krull dimension.

Adam Topaz (Apr 21 2021 at 18:42):

Why is that a problem?

Stepan Nesterov (Apr 21 2021 at 18:44):

The following seems to be (an overcomplicated) strategy:
Step 1. If k is the field of real numbers, and V is a finite-dimensional vector space, then V is locally compact with respect to the weak topology defined by V*. Therefore, V has a unique Haar measure up to scaling. Define for an f: V -> V its determinant to be the constant, on which it multiplies the Haar measure if f is in the connected component of GL(V), and negative that constant otherwise. Define tr(f)=d/dt det(1+tf) at 0.
Step 2. If k is a field of complex numbers, then End_k(V) is a subspace of End_R(V). Define trace over k as half the trace over the reals.
Step 3. If k is a ring Z[x1,...,xn], embed it into C and use step 2.
Step 4. If k a ring of finite type over Z, use step 4, and then pass to colimits.

Stepan Nesterov (Apr 21 2021 at 18:44):

We don't even need to care about the sign of det, I guess

Kevin Buzzard (Apr 21 2021 at 18:45):

I would be happy with a construction over the reals and I can quite believe that you can then spread out. So my instinct is to look for the sneaky basis-choosing in step 1.

Stepan Nesterov (Apr 21 2021 at 18:47):

Ok, one issue is to prove V is Hausdorff aka that linear functions separate points of V.

Kevin Buzzard (Apr 21 2021 at 18:47):

Maybe it's hard to prove that V is locally compact? My model for a "bad" V is one which has linearly independent subsets of size n for all n but which is still Noetherian.

Kevin Buzzard (Apr 21 2021 at 18:49):

If we're defining V to be finite-dimensional if it's Noetherian then we need to rule out the possibility that there are Noetherian modules with arbitrary large ascending chains all of which are finite. This is what choosing the basis does for you -- you can show the basis is a concrete bound for the length of any chain. But a random Noetherian module can I think have arbitrarily large ascending chains -- there are infinite-dimensional Noetherian rings, right?

Adam Topaz (Apr 21 2021 at 18:51):

Yeah I think there are examples by Nagata?

Stepan Nesterov (Apr 21 2021 at 18:51):

Guess you can prove existence of linear functionals by just throwing in Zorn lemma and not caring.
If we know that V* is finitely generated, then you can get a closed embedding V -> R^n, hence V is locally compact. Not sure if that counts as picking a basis, more of a usage that V is a projective R-module.

Stepan Nesterov (Apr 21 2021 at 18:52):

The thing I'm not so sure about is why det(1+tf) is differentiable

Stepan Nesterov (Apr 21 2021 at 18:54):

Well, let's say that differentiability in V makes sense somehow and that we have an access to a smooth bump function \phi with integral 1. Then det(1+tf)= \int \phi(1+tf(x)) dx, which is smooth by some Analysis 2, I guess?

Kevin Buzzard (Apr 21 2021 at 18:57):

I think that when it has got to this point it's just better to ask a constructivist/foundational person to prove that it can't be done without picking a basis, rather than trying to construct more elaborate arguments. My mental model of mathematics says that if you can't do it with easy stuff then you're never going to be doing it with Haar measure.

Stepan Nesterov (Apr 21 2021 at 19:00):

Well, it does sometimes happen that an elaborate argument for a simple fact is actually non-circular. There is a proof of the fundamental theorem of algebra using Gauss-Bonnet theorem: https://arxiv.org/abs/1106.0924
There was also the proof using stochastic integration, I believe

David Wärn (Apr 21 2021 at 19:24):

The sensible constructive definition of "V is finite dimensional" is "V is merely isomorphic to knk^n for some nn". In mathlib the type for this is trunc (Σ n : ℕ, V ≃ₗ[k] fin n → k). This is by definition a subsingleton but it still carries data. It's perfectly analogous to the definition of "A is a finite type", which is (equivalent to) "A merely bijects with fin n for some n" (even in Lean!).

So basically, as in real mathematics, if V is finite dimensional, then it has a basis, and you can use this basis in your constructions, provided that you then check that the choice of basis doesn't matter (this is part of trunc-elimination). For example if you want to define the dimension of a finite-dimensional vector space, you have to check that all bases have the same size. In other words, if kmknk^m \cong k^n then m=nm = n. This is not totally obvious but it's something we learn how to do. Again this is perfectly analogous to the cardinality of a finite type -- you have to check that [m][n][m] \cong [n] implies m=nm = n.

Returning to the definition of trace, consider the fact that if V is finite-dimensional then the evaluation map VVV \to V^{**} is an isomorphism. This is a subsingleton (a map has at most one two-sided inverse), so the second part of trunc-elimination is trivial and we can just assume VV has a finite basis. So it suffices to check it for knk^n basically, which is straightforward. Same thing with the fact that the obvious map VVHomk(V,V)V \otimes V^* \to Hom_k(V, V) is an isomorphism when VV is finite-dimensional, or the fact that nV\bigwedge^n V is one-dimensional for n=dimVn = \dim V.

David Wärn (Apr 21 2021 at 19:48):

NB there are weaker definitions of "A is a finite set" for which the cardinality of A becomes noncomputable. For example knowing that A embeds in a finite set does not let you compute the cardinality of A -- any proposition embeds in unit, but computing the cardinality of a proposition means deciding if it's true or false. (Similarly knowing that A has a surjection from a finite set does not help.) By the same token, knowing that V embeds in a finite-dimensional vector space (or doesn't have an infinite independent set or whatever) doesn't let you compute the dimension of V.

Kevin Buzzard (Apr 21 2021 at 21:38):

I see, so the issue is that we have a nonconstructive definition of finite-dimensional ("V is Noetherian") and then we're trying to do something which moves from the Prop world ("there exists a basis") to the Type world ("this is its size" / "this is a matrix").

Gabriel Moise (Apr 23 2021 at 08:21):

Patrick Massot said:

I'm late to the party but I'm extremely worried about trying to merge this into mathlib. Why working with matrices instead of endomorphisms? I think going down the mathematical road (first endomorphisms and then deduce results about matrices if they are needed somewhere) would be much cleaner.

Thanks for the suggestion! I made that file to practice solving some lemmas for a uni project I have. Clearly, my approach is clumsy, but maybe some of the simple lemmas that I use could be added to mathlib to make calculations easier (so far I am trying to add simple lemmas to the data.matrix.basic file about dot_products and stuff like that).

Gabriel Moise (Apr 23 2021 at 08:23):

I do have a question though, do you think it would something desired to also add a section about vectors on C and operations with them? Like in my file I have a definition vec_conj and some lemmas with dot_product and norm_sq? Would those help mathlib and if so, where do they fit in?

Johan Commelin (Apr 23 2021 at 08:26):

With C you mean the complex numbers?

Johan Commelin (Apr 23 2021 at 08:26):

I think there is already a bunch of stuff for an "arbitrary" field that is is_R_or_C.

Johan Commelin (Apr 23 2021 at 08:27):

But I haven't used that much. Hopefully others can chime in.

Gabriel Moise (Apr 23 2021 at 08:28):

Yes, I meant the complex numbers.

Gabriel Moise (Apr 23 2021 at 08:29):

Oh, I will have a look into that then.

Gabriel Moise (Apr 23 2021 at 08:39):

But for that I think I would need to prove that (V -> C) is an instance of is_R_or_C, with V an indexing type.

Johan Commelin (Apr 23 2021 at 08:40):

No, that won't work. The coefficients of a vector live in such a field, but the vector itself doesn't.

Eric Wieser (Apr 23 2021 at 08:54):

Does it make sense to define a pi.star_ring which would provide vec_conj as docs#star?

Eric Wieser (Apr 23 2021 at 08:55):

We already imbue pi types with most operations elementwise

Eric Wieser (Apr 23 2021 at 08:55):

So doing the same for the star "operator" doesn't seem totally unreasonable

Scott Morrison (Apr 23 2021 at 10:37):

I like it.

Eric Wieser (Apr 23 2021 at 10:46):

I'll make the quick PR

Eric Wieser (Apr 23 2021 at 11:01):

#7342

Gabriel Moise (Apr 24 2021 at 11:38):

I noticed that having a coercion from real-valued matrices to complex-valued matrices means that I need to write a lot of explicit coercions(M : matrix V V ℂ), but that makes reading difficult especially when I have equations like in line 248 from https://github.com/gabrielmoise/Lean-work/blob/master/symm_matrix.lean :

have h₁ : mul_vec (M : matrix V V ) (a  v + b  w) = mul_vec (M : matrix V V ) (a  v) + mul_vec (M : matrix V V ) (b  w),

and I would like to transform this thing into a notation. Can I create a notation that depends on an input M of a certain type (matrix V V ℝ)?

Scott Morrison (Apr 24 2021 at 11:52):

Sure --- just set up the notation, and it won't typecheck if you give it the wrong input. This is not something you really have to specify at the notation level.

Eric Wieser (Apr 24 2021 at 11:57):

Are you sure you need the coercions at all?

Eric Wieser (Apr 24 2021 at 11:57):

That is, can you state the lemmas for a more general case than \C which includes \R?

Scott Morrison (Apr 24 2021 at 12:00):

I commend is_R_or_C to you!

Gabriel Moise (Apr 24 2021 at 12:03):

Well, my proofs require the fact that I am using a matrix that is real-valued and my matrix-vector operations require that this matrix is coerced to a complex-valued operation. So that was my first idea, but I can adjust it. What I wanted to try for now is something like this: (don't mind the notation, it will probably be changed to something more appropriate)

variables {m n : Type*} [fintype m] [fintype n]
instance : has_coe (matrix m n ) (matrix m n ) := λ M, (λ i j, M i j, 0⟩)⟩

notation `$` := λ (M : matrix m n ), (M : matrix m n ) -- invalid notation declaration, contains reference to local variables

But apparently this doesn't work.

Gabriel Moise (Apr 24 2021 at 12:03):

Scott Morrison said:

I commend is_R_or_C to you!

I am exploring this idea as well, thank you! :smile:

Gabriel Moise (Apr 25 2021 at 18:54):

Gabriel Moise said:

https://github.com/gabrielmoise/Lean-work/blob/master/symm_matrix.lean
Yes, some of the lemmas are more general (delimitated them with comments) and would fit into the data.matrix.basic file

I updated the file so that now it is hopefully up to a better standard. I'll probably try to PR some lemmas from there. Thanks for the help! :smile: (any other suggestion is more than welcomed)

Eric Wieser (Apr 25 2021 at 18:59):

The star_test instance you have is provided for you if you import algebra.star.pi

Gabriel Moise (Apr 25 2021 at 19:01):

Oh thanks for the PR you did then! :smile:

Eric Wieser (Apr 25 2021 at 19:01):

Although from what I can tell you didn't end up using it anyway

Gabriel Moise (Apr 25 2021 at 19:09):

Yeah, I had two lemmas using the star instances, but I managed to avoid using them in the important theorems. But it was a good exercise.

Eric Wieser (Apr 25 2021 at 19:22):

I think there's some glue missing between is_R_or_C and has_star that might help eventually

Gabriel Moise (Apr 29 2021 at 07:53):

How can I specify that I am working on a ring structure that has (1 : R) ≠ 0 i.e. that this is not a zero ring?

lemma test [ring R] [specify (1 : R)  0] : ...

Eric Wieser (Apr 29 2021 at 07:56):

[nontrivial R]

Eric Wieser (Apr 29 2021 at 07:56):

Which gives you access to docs#zero_ne_one


Last updated: Dec 20 2023 at 11:08 UTC