## Stream: maths

### Topic: Is there code for X already somewhere?

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

#### Juho Kupiainen (Dec 18 2019 at 10:09):

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

#### Johan Commelin (Dec 18 2019 at 10:15):

We have tensor products, but nothing beyond that

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

#### Kevin Buzzard (Dec 18 2019 at 13:12):

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

#### Patrick Massot (Dec 18 2019 at 13:13):

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

(deleted)

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


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

#### Johan Commelin (Dec 19 2019 at 08:07):

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

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

#### Johan Commelin (Dec 19 2019 at 08:37):

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

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

function.update?

Thanks!

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

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

#### Mario Carneiro (Dec 19 2019 at 09:01):

oh, I see Marc already found it

#### Juho Kupiainen (Dec 19 2019 at 17:28):

This topic should probably actually be a stream.

#### Juho Kupiainen (Dec 19 2019 at 17:29):

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

#### Patrick Massot (Dec 19 2019 at 17:30):

This category is overrated.

#### Patrick Massot (Dec 19 2019 at 17:30):

The relevant one is Type.

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

#### Kevin Buzzard (Dec 19 2019 at 17:31):

equiv

#### Kevin Buzzard (Dec 19 2019 at 17:31):

is the type of bijections of types.

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

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

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

#### Kevin Buzzard (Dec 19 2019 at 17:36):

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

#### Kevin Buzzard (Dec 19 2019 at 17:37):

there should be an equiv of them ;-)

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

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

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