Is there code for X already somewhere?

Stream: maths

[Juho Kupiainen]

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]

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

[Johan Commelin]

We have tensor products, but nothing beyond that

[Patrick Massot]

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]

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]

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

[Chris Hughes]

(deleted)

[Sebastien Gouezel]

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?

[Johan Commelin]

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]

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

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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.

[Marc Huisinga]

function.update?

[Sebastien Gouezel]

Thanks!

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

oh, I see Marc already found it

[Juho Kupiainen]

This topic should probably actually be a stream.

[Juho Kupiainen]

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

[Patrick Massot]

This category is overrated.

[Patrick Massot]

The relevant one is Type.

[Juho Kupiainen]

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

[Kevin Buzzard]

equiv

[Kevin Buzzard]

is the type of bijections of types.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

there should be an equiv of them ;-)

[Kevin Buzzard]

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]

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]

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