Name?

Stream: maths

[Yury G. Kudryashov]

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]

@Sebastien Gouezel :point_up:

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

Do we have some of these in mathlib?

[Kevin Buzzard]

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]

We have an instance preorder.small_category.

[Kevin Buzzard]

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]

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.

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.

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]

(deleted)

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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]

Do you mean .bilin x x?

[Heather Macbeth]

Perhaps affine_bilin_form?

[Adam Topaz]

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

[Adam Topaz]

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

[Eric Wieser]

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]

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

[Eric Wieser]

how would you define i_need_a_name.as_tensor_algebra_linear_map?

[Adam Topaz]

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]

I think there are problems with the above code.

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

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]

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]

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]

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.