Zulip Chat Archive

Stream: maths

Topic: Is there code for X already somewhere?


view this post on Zulip Juho Kupiainen (Dec 18 2019 at 10:06):

I'm starting this topic so people have a place to ask questions of the form "has someone already coded X, or something close to it?" All such questions are welcome even if you could probably find the answer on your own fairly quickly..

view this post on Zulip Juho Kupiainen (Dec 18 2019 at 10:09):

Is there code for symmetric algebras https://en.wikipedia.org/wiki/Symmetric_algebra

view this post on Zulip Johan Commelin (Dec 18 2019 at 10:15):

We have tensor products, but nothing beyond that

view this post on Zulip Patrick Massot (Dec 18 2019 at 10:34):

Multilinear algebra is pretty high on the TODO list, but not done yet. We'll almost need the alternating and anti-symmetric parts of the story.

view this post on Zulip Kevin Buzzard (Dec 18 2019 at 13:12):

There's the question of whether we're allowed to divide by k!k! as well (the theory can be simplified in characteristic zero).

view this post on Zulip Patrick Massot (Dec 18 2019 at 13:13):

I guess the mathlib answer is pretty clear, we should follow Bourbaki and never divide anything.

view this post on Zulip Chris Hughes (Dec 18 2019 at 18:07):

(deleted)

view this post on Zulip Sebastien Gouezel (Dec 19 2019 at 07:52):

I need the function changing the value of a function at a given point. Something like

/-- `replace_at f i₀ x` is the function equal to `f`, except at `i₀` where it is equal to `x`. -/
def replace_at (f : ι  α) (i₀ : ι) (x : α) (i : ι) : α :=
if i = i₀ then x else f i

Is this already in mathlib?

view this post on Zulip Johan Commelin (Dec 19 2019 at 08:07):

We really need to be able to write

import kitchen_sink

/-- `replace_at f i₀ x` is the function equal to `f`, except at `i₀` where it is equal to `x`. -/
def replace_at (f : ι  α) (i₀ : ι) (x : α) (i : ι) : α :=
by library_search

in some scratch file.

view this post on Zulip Johan Commelin (Dec 19 2019 at 08:07):

Don't these mk_all.sh scripts allow us to do that?

view this post on Zulip Sebastien Gouezel (Dec 19 2019 at 08:11):

Except that here library_search will not help, because it doesn't know what I want to do. For instance, suggest could give me the answer f i. Or x. Or f i₀. This is really a question where automated tools will not help you, and where you need human beings.

view this post on Zulip Johan Commelin (Dec 19 2019 at 08:37):

Well, a list of all existing terms of that type would still be helpful, right?

view this post on Zulip Sebastien Gouezel (Dec 19 2019 at 08:45):

Of that exact type (i.e., using the same parameters and not a subset of them), up to permutation, yes this would definitely be useful.

view this post on Zulip Marc Huisinga (Dec 19 2019 at 08:46):

function.update?

view this post on Zulip Sebastien Gouezel (Dec 19 2019 at 08:58):

Thanks!

view this post on Zulip Sebastien Gouezel (Dec 19 2019 at 09:00):

Do you know the name of the following lemma in the library?

lemma lt_of_lt_succ_ne {j n} (h₁ : j < n + 1) (h₂ : j  n) : j < n

It is called array.push_back_idx. Thanks library_search!

view this post on Zulip Mario Carneiro (Dec 19 2019 at 09:01):

I believe there is something like that in data.function, I think it is called function.write

view this post on Zulip Mario Carneiro (Dec 19 2019 at 09:01):

oh, I see Marc already found it

view this post on Zulip Juho Kupiainen (Dec 19 2019 at 17:28):

This topic should probably actually be a stream.

view this post on Zulip Juho Kupiainen (Dec 19 2019 at 17:29):

Is there the category Set defined somewhere? And set isomorphisms.

view this post on Zulip Patrick Massot (Dec 19 2019 at 17:30):

This category is overrated.

view this post on Zulip Patrick Massot (Dec 19 2019 at 17:30):

The relevant one is Type.

view this post on Zulip Juho Kupiainen (Dec 19 2019 at 17:31):

I really don't know anything about category theory. I'm just thinking there should be a definition of bijection somewhere..

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:31):

equiv

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:31):

is the type of bijections of types.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:32):

and if you don't know the difference between a set and a type (which is fine, e.g. most mathematicians don't) then what Patrick is saying is that in type theory, we call sets types, and the category you're looking for is indeed called Type

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:33):

To give a term of type equiv X Y you have to give functions X->Y and Y->X, and proofs that both composites are the identity function.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:35):

There is also bijective f, a predicate for a function between types to be bijective, but in practice equiv works better.

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:36):

There are maps in both directions so you can move from one to the other

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:37):

there should be an equiv of them ;-)

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 17:46):

import data.equiv.basic

open function

noncomputable example (X Y : Type) : {f : X  Y // bijective f}  (X  Y) :=
{ to_fun := λ f, equiv.of_bijective f.2,
  inv_fun := λ e, e, e.bijective,
  left_inv := λ f, subtype.ext.2 rfl,
  right_inv := λ e, equiv.ext _ _ (λ x, rfl)  }

There's the two definitions of bijection, and a proof that they biject with each other ;-)

view this post on Zulip Kevin Buzzard (Dec 19 2019 at 18:54):

I guess you could now apply the theorem to itself and deduce that they biject with each other in the other way too.

view this post on Zulip Johan Commelin (Dec 19 2019 at 18:57):

And then there is iso for the category Type. That's a third option.


Last updated: May 12 2021 at 08:14 UTC