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

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.

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

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)


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?

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.

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