fin.rotate

Stream: Is there code for X?

[Scott Morrison]

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]

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

[Adam Topaz]

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

[Scott Morrison]

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]

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

[Yakov Pechersky]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Yakov Pechersky]

docs#sum_fin_sum_equiv

[Adam Topaz]

Oh it's docs#sum_fin_sum_equiv

[Scott Morrison]

Adam Topaz said:

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]

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]

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]

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]

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]

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]

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]

"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

[Mario Carneiro]

Addition wraps, subtraction saturates

[Mario Carneiro]

wtf

[Gabriel Ebner]

Indeed wtf.

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

the simplex category is on the current PR queue

[Gabriel Ebner]

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 :=
by { rw [add_comm (1 : fin (n+1)), fin.n_add_one] }

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]

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]

@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]

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

[Yakov Pechersky]

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]

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]

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]

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]

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]

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

[Adam Topaz]

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

[Yakov Pechersky]

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

[Gabriel Ebner]

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]

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]

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

[Gabriel Ebner]

Give me a second.

[Yakov Pechersky]

(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]

Lean is certainly not C.

[Gabriel Ebner]

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

[Kevin Buzzard]

Adam Topaz said:

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.

[Adam Topaz]

Oh right.

[Eric Wieser]

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