Zulip Chat Archive

Stream: maths

Topic: Is this thing useful


view this post on Zulip Chris Hughes (Jul 03 2019 at 15:42):

Does this have a name. It came up because I conjecture it makes proving things about matrix minors easier. I can use it to define minors of the identity matrix (with extra zeros), and there's an equivalence of categories with matrices of this form I think.

structure inj_pfun (α : Type u) (β : Type v) :=
(to_fun : α  option β)
(inv_fun : β  option α)
(inv :  (a : α) (b : β), b  to_fun a  a  inv_fun b)

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:43):

I would call it a partial equiv

view this post on Zulip Chris Hughes (Jul 03 2019 at 15:51):

It's a semilattice_inf_bot with this order I believe. And then I have supremums on disjoint ones, which correspond to adding matrices.

instance : has_le (inj_pfun α β) :=
⟨λ f g,  a : α, (f a).is_some  f a = g a

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:53):

I guess one way you could write that is \all a b, b \in f a -> b \in g a

view this post on Zulip Chris Hughes (Jul 03 2019 at 15:54):

Nice.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:54):

might be nice to have a has_subset for option to say this

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:55):

It could be a has_le but that's more likely to conflict with domain-specific orders

view this post on Zulip Alexander Bentkamp (Jul 03 2019 at 15:55):

@Chris Hughes What are you working on? Does it have anything to do with eigenvectors? I am working on a proof of the spectral theorem (stating that every normal linear operator/matrix is diagonalizable). Is there any overlap with what you are doing?

view this post on Zulip Chris Hughes (Jul 03 2019 at 15:55):

There's no overlap.

view this post on Zulip Alexander Bentkamp (Jul 03 2019 at 15:56):

Ok, very good.

view this post on Zulip Chris Hughes (Jul 03 2019 at 16:09):

Out of interest, could pequiv be done with an arbitrary monad, and not just option (do you still get composition). Do all monads have mem?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:13):

You can define a mem via a = pure b on any applicative, but that doesn't necessarily make sense in a given monad

view this post on Zulip Chris Hughes (Jul 03 2019 at 16:28):

How about this?

inductive mem {m : Type  Type} [monad m] : Π {α : Type}, α  m α  Prop
| pure :  {α : Type} (a : α), mem a (pure a)
| bind :  {α β : Type} (a : α) (x : m α) (b : β) (f : α  m β),
    mem a x  mem b (f a)  mem b (bind x f)

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:29):

interesting

view this post on Zulip Chris Hughes (Jul 03 2019 at 16:30):

or this

inductive mem {m : Type  Type} [monad m] : Π {α : Type}, α  m α  Prop
| pure :  {α : Type} (a : α), mem a (pure a)
| join :  {α : Type} (a : α) (b : m α) (c : m (m α)), mem a b  mem b c 
  mem a (monad.join c)

view this post on Zulip Chris Hughes (Jul 03 2019 at 16:30):

I think they're the same.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:30):

clearly it's definable in any monad, and it's correct for option, roption, list, multiset, computation...

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:31):

The pure/join version doesn't work for polymorphic monads

view this post on Zulip Chris Hughes (Jul 03 2019 at 16:32):

Do you mean universe polymorphic?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:32):

yes

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:32):

Type u -> Type v monads

view this post on Zulip Kenny Lau (Jul 03 2019 at 16:32):

is it even well-founded

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:33):

of course it is, it's an inductive

view this post on Zulip Kenny Lau (Jul 03 2019 at 16:33):

I thought some inductives are not permissible

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:33):

But I think there may be monads where the mem should not be well founded

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:34):

I think it's more appropriate to say that some monads just have a mem relation, and the mem relation should satisfy a \in pure b <-> a = b and a \in bind b f <-> \ex b, a \in f b

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:35):

so that you get some class monad_mem

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:35):

By the way, this is one component of a QPF or BNF

view this post on Zulip Kenny Lau (Jul 03 2019 at 16:37):

is every inductive to Prop permissible? even if the target is on the wrong side of the arrow in an argument?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:37):

With BNFs it's usually defined as a natural transformation F => set where F : Type -> Type is the monad and set : Type -> Type is the powerset functor

view this post on Zulip Chris Hughes (Jul 03 2019 at 16:38):

is every inductive to Prop permissible? even if the target is on the wrong side of the arrow in an argument?

No

inductive contradiction : Prop  Prop
| mk :  {p : Prop}, (contradiction p  false)  contradiction p

view this post on Zulip Mario Carneiro (Jul 03 2019 at 16:41):

that doesn't typecheck, maybe you mean

inductive contradiction : Prop
| mk : (contradiction  false)  contradiction

view this post on Zulip Chris Hughes (Jul 03 2019 at 17:07):

I could do it with roption. Then inf is computable. That would be kind of annoying for matrices though.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 17:08):

I'm not quite clear on how this construction helps with matrices

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:15):

I'm doing a bunch of stuff that involves minors of matrices. I reckon it's easiest to handle this by writing minors as multiplying by some minor of the identity matrix. I need to prove a load of stuff about minors of the identity matrix, I have to prove that under some circumstances you get zero, sometimes you get a single entry of one, sometimes you get the identity matrix. I have to add them at some point as well, if you partition the columns of a matrix MM into two sets AA and BB, then Mx=MAxA+MBxBMx = M_Ax_A + M_Bx_B (because IAIAT+IBIBT=1I_AI_A^T + I_BI_B^T = 1). I think the easiest way to handle this is to use these pequivs to express the closure under multiplication of the minors of the identity matrix.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:17):

Isn't the closure condition for minors of the identity just IAIB=IABI_AI_B=I_{A\cap B}?

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:19):

That doesn't type check. You need to multiply by the transpose. But then you get rows of zeros, so you're no longer dealing with minors of the identity.

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:20):

rows and columns

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:25):

I'm using the current Lean definition of minor, which includes reorderings by the way.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:29):

I was making the guess that IAI_A is a matrix on α×α\alpha\times\alpha which is only 1 at (i,i)(i,i) where iAαi\in A\subseteq \alpha and 0 elsewhere

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:32):

IAI_A is the matrix containing the columns of II whose indices are in the set AA.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:33):

so it's a rectangular matrix? Is A a type or a set?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:33):

If it's a type then shouldn't there be a function somewhere to define what the diagonal is?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:36):

I think I see what you want partial equivs for. I think you can do a lot with just partial functions though, you don't need the inverse except for transposing

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:36):

morally A is a subset of fin n of cardinality m. But to make things type check it will have to be some function fin m -> fin n

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:37):

I'm transposing a lot.

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:37):

I do want them to be injective as well.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:41):

whatever happened to using fintypes?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:42):

So I_A i j := if A i = j then 1 else 0?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:45):

And this has to be generalized to allow zeros, hence I_A i j := if j \in A i then 1 else 0 where A : fin m -> option (fin n)

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:45):

and then given a local equiv EE you can say IET=IE1I_E^T = I_{E^{-1}}

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:46):

No if A={0,2}A=\{0,2\} then IA=100001I_A = \begin{matrix} 1 && 0 \\ 0 && 0 \\ 0 && 1 \end{matrix}

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:47):

I assume you mean A(0)=0A(0)=0 and A(1)=2A(1)=2?

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:47):

Yes. So IATIAI_A^TI_A is what you said

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:48):

And I think IAIAT=1I_AI_A^T = 1

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:48):

Are you sure? My definition of I_A is rectangular

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:48):

Yeah, sorry, yours is the same as mine.

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:49):

Or maybe transposed.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:49):

we need a function boole [has_zero A] [has_one A] : bool -> A

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:50):

How does that help?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:50):

gets rid of the if p then 1 else 0 part

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:51):

also known as the iverson bracket

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:52):

I don't have an opinion on that.

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:52):

anyway, I approve re: using local equivs for this

view this post on Zulip Chris Hughes (Jul 03 2019 at 20:53):

With option or roption?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:53):

option

view this post on Zulip Mario Carneiro (Jul 03 2019 at 20:53):

We can look at refactoring later, for now do the thing that makes sense in your application


Last updated: May 06 2021 at 18:20 UTC