## Stream: maths

### Topic: Name?

#### Yury G. Kudryashov (Apr 08 2020 at 16:34):

What are the proper names of the following two construction?

1. Given a map f : α → α, consider the space of sequences x : ℕ → α such that x n = f (x (n + 1)); the left shift is an injective map on this space, and it is bijective if f was surjective.
2. Given a map f : α → α, consider the quotient of ℕ × α by (n, x) ~ (n + 1, f x); if f was injective, then we have an embedding of α into this quotient and f lifts to a bijective map.

Of course, both constructions can be generalized to an action of a monoid different from multiplicative ℕ.

#### Yury G. Kudryashov (Apr 08 2020 at 16:36):

@Sebastien Gouezel :point_up:

#### Kevin Buzzard (Apr 08 2020 at 17:15):

The sequences in 1 are the usual model for the (projective) limit of $\cdots\to\alpha\to\alpha\to\alpha$, with all the maps being $f$.

#### Kevin Buzzard (Apr 08 2020 at 17:17):

and the type in 2 is the usual model for the colimit $\alpha\to\alpha\to\alpha\to\cdots$.

#### Yury G. Kudryashov (Apr 08 2020 at 17:20):

Do we have some of these in mathlib?

#### Kevin Buzzard (Apr 08 2020 at 17:23):

I guess we might well have general limits and colimits now, so perhaps the question reduces to (a) do we have the small category with objects indexed by nat and Hom(a,b)=(a<=b) (or more generally do we have the small category associated to a preorder) and (b) do we have the machinery to define a functor from this nat category to an arbitrary category (e.g. Type) by just saying where the maps associated to a proof of a<=succ(a) go.

#### Yury G. Kudryashov (Apr 08 2020 at 17:27):

We have an instance preorder.small_category.

#### Kevin Buzzard (Apr 08 2020 at 17:28):

So it would be an amusing exercise to define a functor from nat to Type sending all objects to alpha, and sending h:a<=b to f^{b-a}, but whether this is in already I don't know.

#### Sebastien Gouezel (Apr 08 2020 at 17:30):

Yury G. Kudryashov said:

What are the proper names of the following two construction?

1. Given a map f : α → α, consider the space of sequences x : ℕ → α such that x n = f (x (n + 1)); the left shift is an injective map on this space, and it is bijective if f was surjective.

In general, one considers instead the space of sequences y : \Z → αsuch that y (n + 1) = f (y n) for all n. Noting that the values of such a sequence for n > 0 are completely determined by y 0, it suffices to fix the values y nfor n \le 0, so this is clearly equivalent to you definition. This is called the natural extension of the original system.

1. Given a map f : α → α, consider the quotient of ℕ × α by (n, x) ~ (n + 1, f x); if f was injective, then we have an embedding of α into this quotient and f lifts to a bijective map.

I don't know a name for this one. It is a cousin of the suspension of f with roof function r, i.e., taking the quotient of ℕ × α by (x, n + r(x)) ~ (f x, n).

(deleted)

#### Sebastien Gouezel (Apr 08 2020 at 17:33):

1. is not really well behaved as it does not respect compatness. For instance, if α has two points and f is constant.

#### Sebastien Gouezel (Apr 08 2020 at 17:34):

Sorry, you are assuming f is injective, so forget my comment.

#### Sebastien Gouezel (Apr 08 2020 at 17:38):

What does it look like if α = [0, 1] and f (x) = x / 2?

#### Kevin Buzzard (Apr 08 2020 at 17:48):

1. looks like the inductive limit $[0,1]\subset[0,2]\subset[0,4]\subset\cdots$ so it's $\mathbb{R}_{\geq0}$.

#### Kevin Buzzard (Apr 08 2020 at 17:50):

I'm assuming alpha isn't a list here ;-)

#### Kevin Buzzard (Apr 08 2020 at 17:51):

I'm also assuming that things which are the same, are equal.

#### Yury G. Kudryashov (Mar 12 2021 at 00:41):

How would you call the following object?

structure i_need_a_name (k E : Type*) [field k] [vector_space k E] :=
(bilin : bilin_form k E)
(lin : E →ₗ[k] E)
(c : E)

instance : has_coe_to_fun (f : i_need_a_name k E) :=
⟨_, λ x, f.bilin x + f.lin x + f.c⟩


#### Eric Wieser (Mar 12 2021 at 00:45):

Do you mean .bilin x x?

#### Heather Macbeth (Mar 12 2021 at 00:48):

Perhaps affine_bilin_form?

#### Adam Topaz (Mar 12 2021 at 00:58):

You wouldn't call this anything, because it should be more generally defined using the tensor algebra.

#### Adam Topaz (Mar 12 2021 at 00:59):

But if I had to choose a name, I think Heather's suggestion is good!

#### Eric Wieser (Mar 12 2021 at 01:14):

I guess the tensor version would look something like(⨁ n : fin 3, ⨂[k] _ : fin n, E) →ₗ[k] E, composed with a function mapping x to 1 + x + x ⊗ x

#### Adam Topaz (Mar 12 2021 at 01:14):

I mean, this is a special case of a linear map from the tensor algebra of $E$ to $E$

#### Eric Wieser (Mar 12 2021 at 01:17):

how would you define i_need_a_name.as_tensor_algebra_linear_map?

#### Adam Topaz (Mar 12 2021 at 01:17):

Wait, not it's not. And I'm confused anyway. A bilinear form on $E$ takes values in $k$. How do you add that to an element of $E$?

#### Adam Topaz (Mar 12 2021 at 01:18):

I think there are problems with the above code.

#### Adam Topaz (Mar 12 2021 at 01:18):

I assume Yuri wanted a bilinear map, not a bilinear form.

#### Eric Wieser (Mar 12 2021 at 01:18):

I guess I'd call it "rejected by the typechecker"

#### Adam Topaz (Mar 12 2021 at 01:26):

The tensor algebra up to degree 2 looks like this:
$k \oplus E \oplus E \otimes_k E$
So a linear map from this to $E$ consists of the following data:

1. a bilinear map from $E \times E$ to $E$.
2. a linear map $E \to E$.
3. a constant in $E$.

#### Adam Topaz (Mar 12 2021 at 01:26):

That's exactly what i_need_a_name is (or at least I assume it should be, if one replaces bilin_form with bilin_map or something like that)

#### Sebastien Gouezel (Mar 12 2021 at 06:34):

Note that the identification between bilinear forms and the tensor product only works in finite dimension. For instance, on a Hilbert space the scalar product is not an element of $E^* \otimes E^*$ (because the elements of the tensor product have finite rank). So, if you want to do this in more general situations, the tensor product approach is not a good choice.

#### Yury G. Kudryashov (Mar 12 2021 at 06:46):

Eric Wieser said:

I guess I'd call it "rejected by the typechecker"

I'm sorry for the typos. Fixed now. #xy: I'm going to rewrite some of theorems about inner product in a Hilbert space in terms of this object. This is useful, e.g., to show (some day in the future) that the Dirichlet problem in the disc has a solution in the appropriate Sobolev space. In this case you have f x = q x + l x + c where q is a quadratic form (not necessarily the one coming from the inner product) and you need to minimize it. Another goal is to use theorems like is_local_min_on.has_fderiv_within_at_eq_zero instead of manually choosing εs.

Last updated: May 19 2021 at 02:10 UTC