Is this thing useful

Stream: maths

[Chris Hughes]

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)

[Mario Carneiro]

I would call it a partial equiv

[Chris Hughes]

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⟩

[Mario Carneiro]

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

[Chris Hughes]

Nice.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Alexander Bentkamp]

@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?

[Chris Hughes]

There's no overlap.

[Alexander Bentkamp]

Ok, very good.

[Chris Hughes]

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?

[Mario Carneiro]

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

[Chris Hughes]

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)

[Mario Carneiro]

interesting

[Chris Hughes]

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)

[Chris Hughes]

I think they're the same.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

Do you mean universe polymorphic?

[Mario Carneiro]

yes

[Mario Carneiro]

Type u -> Type v monads

[Kenny Lau]

is it even well-founded

[Mario Carneiro]

of course it is, it's an inductive

[Kenny Lau]

I thought some inductives are not permissible

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

so that you get some class monad_mem

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

that doesn't typecheck, maybe you mean

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

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 $M$ into two sets $A$ and $B$, then $Mx = M_Ax_A + M_Bx_B$ (because $I_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.

[Mario Carneiro]

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

[Chris Hughes]

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.

[Chris Hughes]

rows and columns

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

$I_A$ is the matrix containing the columns of $I$ whose indices are in the set $A$.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Chris Hughes]

I'm transposing a lot.

[Chris Hughes]

I do want them to be injective as well.

[Mario Carneiro]

whatever happened to using fintypes?

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Mario Carneiro]

and then given a local equiv $E$ you can say $I_E^T = I_{E^{-1}}$

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

Yes. So $I_A^TI_A$ is what you said

[Chris Hughes]

And I think $I_AI_A^T = 1$

[Mario Carneiro]

Are you sure? My definition of I_A is rectangular

[Chris Hughes]

Yeah, sorry, yours is the same as mine.

[Chris Hughes]

Or maybe transposed.

[Mario Carneiro]

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

[Chris Hughes]

How does that help?

[Mario Carneiro]

gets rid of the if p then 1 else 0 part

[Mario Carneiro]

also known as the iverson bracket

[Chris Hughes]

I don't have an opinion on that.

[Mario Carneiro]

anyway, I approve re: using local equivs for this

[Chris Hughes]

With option or roption?

[Mario Carneiro]

option

[Mario Carneiro]

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