# Zulip Chat Archive

## Stream: maths

### Topic: Name?

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

What are the proper names of the following two construction?

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

- 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 n`

for `n \le 0`

, so this is clearly equivalent to you definition. This is called the natural extension of the original system.

- 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)`

.

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

(deleted)

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

- 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):

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

- a bilinear map from $E \times E$ to $E$.
- a linear map $E \to E$.
- 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