Zulip Chat Archive

Stream: maths

Topic: Name?


view this post on Zulip 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 ℕ.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 16:36):

@Sebastien Gouezel :point_up:

view this post on Zulip 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 ff.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 17:20):

Do we have some of these in mathlib?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 17:27):

We have an instance preorder.small_category.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 17:31):

(deleted)

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Apr 08 2020 at 17:34):

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

view this post on Zulip Sebastien Gouezel (Apr 08 2020 at 17:38):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 17:48):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 17:50):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 17:51):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 12 2021 at 00:45):

Do you mean .bilin x x?

view this post on Zulip Heather Macbeth (Mar 12 2021 at 00:48):

Perhaps affine_bilin_form?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 12 2021 at 00:59):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 12 2021 at 01:14):

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

view this post on Zulip Eric Wieser (Mar 12 2021 at 01:17):

how would you define i_need_a_name.as_tensor_algebra_linear_map?

view this post on Zulip Adam Topaz (Mar 12 2021 at 01:17):

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

view this post on Zulip Adam Topaz (Mar 12 2021 at 01:18):

I think there are problems with the above code.

view this post on Zulip Adam Topaz (Mar 12 2021 at 01:18):

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

view this post on Zulip Eric Wieser (Mar 12 2021 at 01:18):

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

view this post on Zulip Adam Topaz (Mar 12 2021 at 01:26):

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

  1. a bilinear map from E×EE \times E to EE.
  2. a linear map EEE \to E.
  3. a constant in EE.

view this post on Zulip 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)

view this post on Zulip 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 EEE^* \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.

view this post on Zulip 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