Zulip Chat Archive

Stream: kbb

Topic: merging into mathlib

Johan Commelin (Sep 24 2018 at 16:02):

Clearly some parts of kbb are not mathlib-ready, but other parts are.

Johan Commelin (Sep 24 2018 at 16:02):

I think we should try to get those merged into mathlib.

Johan Commelin (Sep 24 2018 at 16:03):

For example, the remainder of the file on matrices. The monoid stuff, and determinants should also be merge-ready, I think.

Johan Commelin (Sep 24 2018 at 16:04):

I'll try to work on this when I'm back home. This is a mental note for me, and a hint for others to possible help with this (-;

Johannes Hölzl (Sep 24 2018 at 17:09):

I will merge the PID -> UFD part

Kevin Buzzard (Sep 25 2018 at 07:20):

Just to note here that Chris defined log as the unique inverse of exp yesterday, and proved exp log = id, log exp = id on the appropriate domains. @Chris Hughes Is this file publically accessible?

Mario Carneiro (Sep 25 2018 at 07:22):

Nice! Is this the real version or the complex version?

Kevin Buzzard (Sep 25 2018 at 07:23):

real single-valued log from positive reals to reals

Chris Hughes (Sep 25 2018 at 19:20):

@Kevin Buzzard Yes it is, on the exp branch of community mathlib.

Johan Commelin (Sep 27 2018 at 07:17):

@Scott Morrison Do you want to PR the category of matrices? Or would you like me to do it (from community mathlib)?

Johan Commelin (Sep 27 2018 at 07:17):

@Kenny Lau Do you want to PR determinants? Or would you like me to do it (from community mathlib)?

Scott Morrison (Sep 27 2018 at 07:18):

I'm certainly happy if you want to do it. :-) I have a lot of open PRs at the moment...

Scott Morrison (Sep 27 2018 at 07:31):

I do kind of like the 

def free_module (α : Type v) [semiring α] : Type := ℕ
instance : category (free_module α) :=
{ hom  := λ m n, matrix (fin m) (fin n) α, ... }

It's somehow alien and familiar at the same time.

Mario Carneiro (Sep 27 2018 at 07:34):

I changed it to a large category over fintypes, what do you think?

Johan Commelin (Sep 27 2018 at 08:12):

@Mario Carneiro You also deleted a bunch of stuff on diagonal matrices, I think. Was that intentional?

Mario Carneiro (Sep 27 2018 at 08:12):

it all moved to mathlib

Johan Commelin (Sep 27 2018 at 08:19):

Hmmm, but not community mathlib...

Mario Carneiro (Sep 27 2018 at 08:21):

huh? just update master in that case

Chris Hughes (Sep 27 2018 at 08:23):

Or update the matrix branch

Johan Commelin (Sep 27 2018 at 09:10):

Aaah, I see what went wrong (and I was afk for 30 minutes)

Johan Commelin (Sep 27 2018 at 09:10):

@Mario Carneiro Is there a reason why you didn't merge scalar matrices?

Johan Commelin (Sep 27 2018 at 09:10):

Do you think they are not useful enough, because diagonal easily covers those cases?

Kenny Lau (Sep 27 2018 at 18:17):

@Kenny Lau Do you want to PR determinants? Or would you like me to do it (from community mathlib)?

please do it

Johan Commelin (Sep 27 2018 at 18:18):

I'll do it tomorrow

Mario Carneiro (Sep 27 2018 at 21:47):

Aren't there two different definitions of permutation sign (one over fin n, one over a fintype) right now? I think one was developed in kbb by Kenny and the other was in a mathlib PR by Chris

Kenny Lau (Sep 28 2018 at 04:47):

I'll do it tomorrow

the same time as when everyone does everything :p

Johan Commelin (Sep 28 2018 at 05:10):

I promise!

Johan Commelin (Sep 28 2018 at 08:20):

@Kenny Lau Done.

Chris Hughes (Sep 28 2018 at 09:02):

@Johan Commelin @Kenny Lau fintype perm is in mathlib now by the way, I imagine you need that.

Johan Commelin (Sep 28 2018 at 09:06):

Aah, I just dumped Kenny's sym into the PR. Does this mean that stuff is duplicated?

Chris Hughes (Sep 28 2018 at 09:07):

Probably

Chris Hughes (Sep 28 2018 at 09:08):

Kenny did sign and stuff, which is also in mathlib.

Last updated: Dec 20 2023 at 11:08 UTC