# Zulip Chat Archive

## Stream: maths

### Topic: Is this thing useful

#### 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)

#### Mario Carneiro (Jul 03 2019 at 15:43):

I would call it a partial equiv

#### 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⟩

#### 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`

#### Chris Hughes (Jul 03 2019 at 15:54):

Nice.

#### Mario Carneiro (Jul 03 2019 at 15:54):

might be nice to have a `has_subset`

for option to say this

#### 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

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

#### Chris Hughes (Jul 03 2019 at 15:55):

There's no overlap.

#### Alexander Bentkamp (Jul 03 2019 at 15:56):

Ok, very good.

#### 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`

?

#### 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

#### 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)

#### Mario Carneiro (Jul 03 2019 at 16:29):

interesting

#### 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)

#### Chris Hughes (Jul 03 2019 at 16:30):

I think they're the same.

#### 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`

...

#### Mario Carneiro (Jul 03 2019 at 16:31):

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

#### Chris Hughes (Jul 03 2019 at 16:32):

Do you mean universe polymorphic?

#### Mario Carneiro (Jul 03 2019 at 16:32):

yes

#### Mario Carneiro (Jul 03 2019 at 16:32):

`Type u -> Type v`

monads

#### Kenny Lau (Jul 03 2019 at 16:32):

is it even well-founded

#### Mario Carneiro (Jul 03 2019 at 16:33):

of course it is, it's an inductive

#### Kenny Lau (Jul 03 2019 at 16:33):

I thought some inductives are not permissible

#### Mario Carneiro (Jul 03 2019 at 16:33):

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

#### 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`

#### Mario Carneiro (Jul 03 2019 at 16:35):

so that you get some class `monad_mem`

#### Mario Carneiro (Jul 03 2019 at 16:35):

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

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

#### 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

#### 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

#### Mario Carneiro (Jul 03 2019 at 16:41):

that doesn't typecheck, maybe you mean

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

#### 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.

#### Mario Carneiro (Jul 03 2019 at 17:08):

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

#### 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 $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 (Jul 03 2019 at 20:17):

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

#### 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.

#### Chris Hughes (Jul 03 2019 at 20:20):

rows and columns

#### Chris Hughes (Jul 03 2019 at 20:25):

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

#### Mario Carneiro (Jul 03 2019 at 20:29):

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 (Jul 03 2019 at 20:32):

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

#### Mario Carneiro (Jul 03 2019 at 20:33):

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

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

#### 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

#### 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`

#### Chris Hughes (Jul 03 2019 at 20:37):

I'm transposing a lot.

#### Chris Hughes (Jul 03 2019 at 20:37):

I do want them to be injective as well.

#### Mario Carneiro (Jul 03 2019 at 20:41):

whatever happened to using fintypes?

#### Mario Carneiro (Jul 03 2019 at 20:42):

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

?

#### 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)`

#### Mario Carneiro (Jul 03 2019 at 20:45):

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

#### Chris Hughes (Jul 03 2019 at 20:46):

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

#### Mario Carneiro (Jul 03 2019 at 20:47):

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

#### Chris Hughes (Jul 03 2019 at 20:47):

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

#### Chris Hughes (Jul 03 2019 at 20:48):

And I think $I_AI_A^T = 1$

#### Mario Carneiro (Jul 03 2019 at 20:48):

Are you sure? My definition of `I_A`

is rectangular

#### Chris Hughes (Jul 03 2019 at 20:48):

Yeah, sorry, yours is the same as mine.

#### Chris Hughes (Jul 03 2019 at 20:49):

Or maybe transposed.

#### Mario Carneiro (Jul 03 2019 at 20:49):

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

#### Chris Hughes (Jul 03 2019 at 20:50):

How does that help?

#### Mario Carneiro (Jul 03 2019 at 20:50):

gets rid of the `if p then 1 else 0`

part

#### Mario Carneiro (Jul 03 2019 at 20:51):

also known as the iverson bracket

#### Chris Hughes (Jul 03 2019 at 20:52):

I don't have an opinion on that.

#### Mario Carneiro (Jul 03 2019 at 20:52):

anyway, I approve re: using local equivs for this

#### Chris Hughes (Jul 03 2019 at 20:53):

With `option`

or `roption`

?

#### Mario Carneiro (Jul 03 2019 at 20:53):

`option`

#### 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