## Stream: Is there code for X?

### Topic: fin.rotate

#### Scott Morrison (Feb 26 2021 at 02:34):

I would like to know that fin.snoc is a permutation of fin.cons (ie. given by precomposition by some equiv). Does anyone see a cheap way to get this?

I was trying to build

def rotate : Π n, fin n ≃ fin n
| 0 := equiv.refl _
| (n+1) :=
{ to_fun := λ k, if k = last n then 0 else k + 1,
inv_fun := λ k, if h : k = 0 then last n else k - 1,
left_inv := sorry,
right_inv := sorry, }


and finding it quite painful.

#### Mario Carneiro (Feb 26 2021 at 02:43):

I would generalize to swaps of the parts of fin (m + n)

#### Adam Topaz (Feb 26 2021 at 03:15):

Isn't this \lambda i, i+1?

#### Scott Morrison (Feb 26 2021 at 03:39):

That works as well, but left_inv and right_inv don't get any easier, because we have no theorems about addition in fin n.

#### Scott Morrison (Feb 26 2021 at 03:39):

(In part because we keep considering changing the definition.)

#### Yakov Pechersky (Feb 26 2021 at 03:42):

We do have add_comm_monoid (fin (n + 1))

#### Mario Carneiro (Feb 26 2021 at 03:43):

That doesn't say anything about the invertibility of the operation though, it would be true with saturating add too

#### Scott Morrison (Feb 26 2021 at 03:46):

Hopefully we have fin (n+m) ≃ fin n \oplus fin m somewhere, which would make Mario's suggestion nice and straightforward.

#### Adam Topaz (Feb 26 2021 at 03:46):

Wait, it has a monoid instance but not a group instance?

#### Adam Topaz (Feb 26 2021 at 03:47):

Yeah that's there. I think docs#fin_sum_equiv or something like that?

#### Yakov Pechersky (Feb 26 2021 at 03:48):

docs#sum_fin_sum_equiv

#### Adam Topaz (Feb 26 2021 at 03:48):

Oh it's docs#sum_fin_sum_equiv

#### Scott Morrison (Feb 26 2021 at 05:47):

Wait, it has a monoid instance but not a group instance?

If you want the group instance you should be using zmod. It's a bit awkward that we have both, but the idea is that fin n is mostly meant to be algebraically structureless... Of course it inevitably has some.

#### Kevin Buzzard (Feb 26 2021 at 09:25):

It only has some because some pesky people want to talk about 37 : fin 3 (even though they don't know what they want it to mean ;-) ).

#### Kevin Buzzard (Feb 26 2021 at 09:38):

Why use evil addition on fin n? Haven't we got some "next" and "prev" structure on fin n?

I am one of these terrible people who has never got involved with fin n but just watches from the sidelines thinking "why is this such a mess"? For me fin n is some finite totally ordered set, and given any nonempty finite totally ordered set at all (including fin n with its nightmare dependently typed definition and its two definitions of +) there should be functions like "bottom", "top", "next" and "previous" and a cute little API for them which does not ever get tangled up with this pathological fin + question (which is as bad as nat subtraction as far as I'm concerned and as far as I can see the only reason we have it so that we can use numerals). However I moan about all this and then don't actually ever do anything about it :-(

#### Kevin Buzzard (Feb 26 2021 at 09:42):

At least this point of view abstracts away the whole + issue because the API writes itself -- if x!=top then previous(next x)=x, if x!=bottom then next(previous x)=x, next(top) can be 37 for all I care, the only assumption should be a finite nonempty total order and then we have the advantage that it applies more generally.

#### Kevin Buzzard (Feb 26 2021 at 09:44):

Is there such a thing as a discrete total order? I mean a total order such that everything other than "top" has a "next" and everything other than "bottom" has a "previous"? I guess I'm saying I want all nonempty bounded-above sets to have a max and all non-empty bounded-below sets to have a min.

#### Mario Carneiro (Feb 26 2021 at 09:46):

At least this point of view abstracts away the whole + issue because the API writes itself -- if x!=top then previous(next x)=x, if x!=bottom then next(previous x)=x, next(top) can be 37 for all I care, the only assumption should be a finite nonempty total order and then we have the advantage that it applies more generally.

Unfortunately, the fact that fin 0 is empty is a recurring thorn in your side if you want to totalize everything

#### Gabriel Ebner (Feb 26 2021 at 09:46):

fin n is some finite totally ordered set [...] including fin n with its nightmare dependently typed definition and its two definitions of +

I feel like fin has been repurposed for stuff it wasn't meant to do, and now people complain that it doesn't fit their vision.

1. fin n is not some abstract totally ordered set, it is literally the naturals less than n.
2. "nightmare dependently typed definition" please use go-to-definition. It's literally a subtype. It's literally the natural numbers less than n...
3. "two definitions of +". There is one definition of + on fin n, it's addition modulo n and this is the right choice.

#### Mario Carneiro (Feb 26 2021 at 09:47):

"two definitions of +". There is one definition of + on fin n, it's addition modulo n and this is the right choice.

If that's the case, then subtraction should also be modulo n

wtf

Indeed wtf.

#### Gabriel Ebner (Feb 26 2021 at 09:48):

Finally one argument for changing + that I can get behind. Although I'd prefer both to be modulo.

#### Mario Carneiro (Feb 26 2021 at 09:49):

I think part of the confounding issue is that zmod exists, in part because fin subtraction was broken during the core freeze

#### Mario Carneiro (Feb 26 2021 at 09:49):

since zmod exists now, people want fin n to not just be a poor man's zmod

#### Gabriel Ebner (Feb 26 2021 at 09:51):

I'm so happy that Lean 4 gets this right:

protected def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩


#### Kevin Buzzard (Feb 26 2021 at 10:05):

Gabriel's point is interesting. I am always thinking of fin n in terms of simplicial sets because at the back of my mind I have things like simplicial homology in Lean. That particular fin n is equipped with a structure which is well-defined within that sphere, there is the total order, the maps fin n -> fin (n+1) which "miss out i", and the maps fin (n+1) -> fin n which "identify j and j+1" and that's it, other than the obvious lemmas about what happens if you compose these maps. Once we have this right (and maybe we have it right already) we can do algebraic topology and this would be really cool. It would be crazy to introduce another type which played this role, but the problem is that the naive definitions of these maps use addition, which for me is a dangerous function because there's more than one definition of it (saturating or wrapping). Scott is probably thinking about something else, so he is somehow using fin n in a different way, but again he's using addition. Maybe there are better functions that one needs on fin n, like "next" and "previous" (on fin n.succ at least).

#### Kevin Buzzard (Feb 26 2021 at 10:06):

My point is that I'm realising I have a different mental model of fin n to others, and am wondering whether all these different mental models can coexist. Probably they should.

#### Gabriel Ebner (Feb 26 2021 at 10:16):

If you only care about two functions fin.next and fin.prev, then why does it matter if addition is defined or not? (In any case, I didn't see any addition on fin in this thread, only addition of natural numbers.)

#### Kevin Buzzard (Feb 26 2021 at 10:32):

It matters to Scott because he defined them using addition, which is intuitively the way to define them, and then got into a mess. I think my only worthwhile contribution to this thread is suggesting that these functions should be defined (or are perhaps defined already) and a little API made for them and Scott should be using these instead.

#### Johan Commelin (Feb 26 2021 at 10:38):

@Kevin Buzzard which maps are you talking about now? We have the face/degeneracy maps + the simplicial identities now.

#### Johan Commelin (Feb 26 2021 at 10:39):

of course, for the simplicial identities you need an ordering on fin n

#### Kevin Buzzard (Feb 26 2021 at 10:42):

Yes, I thought we would have them by now. Are they in mathlib? For Scott we need "next" and "prev" but I am arguing that these could be defined as "min of {x : x > a}" and "max of {x : x < a}" (which clearly exist for an arbitrary finite totally ordered set) and this would remove dependence on + which might be a good thing.

#### Johan Commelin (Feb 26 2021 at 10:46):

the simplex category is on the current PR queue

#### Gabriel Ebner (Feb 26 2021 at 11:03):

To answer the original question of the thread, it is straightforward to build rotate because we have modulo arithmetic:

import data.fin

@[simp] lemma fin.n_add_one {n : ℕ} : (n + 1 : fin (n + 1)) = 0 :=
by { ext, simp [fin.coe_add, fin.coe_one'] }

@[simp] lemma fin.one_add_n {n : ℕ} : (1 + n : fin (n + 1)) = 0 :=

def rotate : Π n, fin n ≃ fin n
| 0 := equiv.refl _
| (n+1) := ⟨(+1), (+n), λ _, by simp [add_assoc], λ _, by simp [add_assoc]⟩


(It would be even easier if fin (n+1) had a ring instance.)

#### Kevin Buzzard (Feb 26 2021 at 11:40):

Aah, one could also do this by proving rotate for zmod n (true even without the case split!) and then deducing it for fin n using our HoTT substitution tool (equiv.trans).

#### Adam Topaz (Feb 26 2021 at 14:19):

@Kevin Buzzard The point about simplicial sets is interesting! But if we ever want to do cyclic homology, we would need fin.rotate :)

#### Adam Topaz (Feb 26 2021 at 14:20):

I just think it's strange to give fin (n+1) an add_monoid structure which is not an add_group structure.

#### Yakov Pechersky (Feb 26 2021 at 14:31):

The add_monoid would hold even if addition was redefined. The add_group could be misleading because the - isn't what the add_group would suggest.

#### Adam Topaz (Feb 26 2021 at 14:34):

Kevin Buzzard said:

Is there such a thing as a discrete total order? I mean a total order such that everything other than "top" has a "next" and everything other than "bottom" has a "previous"? I guess I'm saying I want all nonempty bounded-above sets to have a max and all non-empty bounded-below sets to have a min.

I'm not sure "discrete" is the correct word for this. Doesn't $\{0\} \cup \{1/2^n \ | \ n \in \mathbb{N}\}$ satisfy these conditions?

#### Adam Topaz (Feb 26 2021 at 14:35):

Yakov Pechersky said:

The add_monoid would hold even if addition was redefined. The add_group could be misleading because the - isn't what the add_group would suggest.

Yeah, I see what you mean here.

#### Yakov Pechersky (Feb 26 2021 at 14:39):

Rob said in the PR (#5010) where I added add_monoid:

Although you could argue that cleaning things up encourages people to use the controversial operations...

#### Adam Topaz (Feb 26 2021 at 14:43):

Here is how things are organized in my mind (for better or worse):

1. fin n could be endowed with the usual abelian groups structure, while zmod n is a commutative ring.
2. fin n can be endowed with the usual order structure, with the understanding that this is really a cyclic order which is compatible with the additive group structure. If you just want the non-cyclic order, just don't use the additive group structure.

I was under the impression that this controversy about arithmetic operations in fin n arose from some coercion fin n -> \N

#### Yakov Pechersky (Feb 26 2021 at 14:46):

Re 1, given that fin n has a has_mul, do we just ignore that?

#### Adam Topaz (Feb 26 2021 at 14:47):

Oh I wasn't aware it had a has_mul. I would say to remove that completely.

#### Yakov Pechersky (Feb 26 2021 at 14:47):

Ah, but all those operations are defined in core. Because it's a shortcut to getting unsigned working.

#### Gabriel Ebner (Feb 26 2021 at 14:50):

I want to repeat that in Lean 4, subtraction will be defined correctly on Fin (i.e. as an inverse to addition). We can (should?) backport this change to Lean 3.

#### Yakov Pechersky (Feb 26 2021 at 14:51):

The coercion of fin n -> \N, if it is the coe_subtype, that is fine. The other coercion comes from nat.cast, which relies on has_add. The reverse direction \N -> fin (n + 1) comes from core docs#fin.of_nat

#### Yakov Pechersky (Feb 26 2021 at 14:53):

Gabriel, would you then separate the unsigned.has_sub from fin.has_sub?

#### Gabriel Ebner (Feb 26 2021 at 14:54):

Give me a second.

#### Yakov Pechersky (Feb 26 2021 at 14:58):

(Relatedly, does it make sense for unsigned ints that subtraction is saturating? According to the C spec,

A computation involving unsigned operands can never overflow, because a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type)

#### Gabriel Ebner (Feb 26 2021 at 15:00):

Lean is certainly not C.

#### Gabriel Ebner (Feb 26 2021 at 15:02):

lean#541
I think this worth it just for the fact that this is how Lean 4 does it.

#### Kevin Buzzard (Feb 26 2021 at 17:06):

Kevin Buzzard said:

Is there such a thing as a discrete total order? I mean a total order such that everything other than "top" has a "next" and everything other than "bottom" has a "previous"? I guess I'm saying I want all nonempty bounded-above sets to have a max and all non-empty bounded-below sets to have a min.

I'm not sure "discrete" is the correct word for this. Doesn't $\{0\} \cup \{1/2^n \ | \ n \in \mathbb{N}\}$ satisfy these conditions?

No, because 0 is not top and doesn't have a next.

Oh right.

#### Eric Wieser (Mar 24 2021 at 17:40):

Coming back to this: should we make docs#fin.comm_ring a global instance now? @Gabriel Ebner suggested that would be reasonable in #6848, and I'd be loosely in favor too

Last updated: May 16 2021 at 05:21 UTC