How to define functions over known cardinality Fintypes?

Stream: lean4

[Valentin Robert]

How should I go about defining a function over some Fintype whose cardinality I know?

For instance, if I have [Fintype T] and Fintype.card T = 3, supposedly I ought to be able to define a function from Fin 3, and package it up unambiguously as a function from T. I'm just not sure what machinery to use to make this the least painful possible.

It seeems Fintype.truncEquivFinOfCardEq might be important, but I feel like I might have to do a lot of juggling.

In my real use case, I'm trying to define a function C2 × C2 → C3 where C2 is a cyclic group of order 2, and C3 is a cyclic group of order 3. Ideally I'd want to write a function Fin 2 × Fin 2 → Fin 3, and just roll with it.

[Aaron Liu]

Can you describe mathematically what you want to do?

[Aaron Liu]

right now my guess is "define a function Fin 2 × Fin 2 → Fin 3, obtain arbitrary bijections C2 ≃ Fin 2 and C3 ≃ Fin 3, then transfer the function across the bijections to get C2 × C2 → C3"

[Valentin Robert]

Zooming out, I'm trying to prove that a group with certain properties will be isomorphic to C3 ⋊[φ] (C2 × C2), for some φ I need to define. But I couldn't find concrete cyclic groups in Mathlib, so instead I'm using abstract cyclic groups, where all I know is they are abstract, supported by a finite type, cyclic, and of the expected cardinality.

So I need to define φ over this abstraction layer.

I don't know yet what φ will need to be for my actual problem, but we can just pick something arbitrary.
Say (0, 0) ↦ 0, (0, 1) ↦ 1, (1, 0) ↦ 2, (1, 1) ↦ 2.

[Jireh Loreaux]

What do you mean by "concrete cyclic groups"? There's Fin itself.

[Valentin Robert]

Maybe I'm just missing some imports, but I get "failed to synthesize Group (Fin 2 × Fin 2) when I use Fin instead of my abstract group.

[metakuntyyy]

That's because Fin is not a Group.

import Mathlib

#synth AddGroup (Fin 2 × Fin 2)

This works though.

[Jireh Loreaux]

You can also use docs#Multiplicative to turn it into one.

[Aaron Liu]

I think usually the cyclic groups are ZMod n and Multiplicative (ZMod n)

[Aaron Liu]

this also gets you the infinite cyclic group with ZMod 0

[metakuntyyy]

Here's the definition by the way. You can also use ZMod, they are definitionally equal.

import Mathlib

def isThisWhatYouWant (x : Fin 2 × Fin 2) : Fin 3 :=
  ⟨ x.1.val + x.2.val, by grind⟩

#eval isThisWhatYouWant ⟨ ⟨ 0, by grind ⟩ , ⟨ 0, by grind ⟩ ⟩ -- 0
#eval isThisWhatYouWant ⟨ ⟨ 0, by grind ⟩ , ⟨ 1, by grind ⟩ ⟩ -- 1
#eval isThisWhatYouWant ⟨ ⟨ 1, by grind ⟩ , ⟨ 0, by grind ⟩ ⟩ -- 1
#eval isThisWhatYouWant ⟨ ⟨ 1, by grind ⟩ , ⟨ 1, by grind ⟩ ⟩ -- 2