Fintype (Group G)

Stream: mathlib4

[Yakov Pechersky]

I couldn't find an instance that we have a finite number of groups over a finite type. I tried using the recently ported/rewritten %derive_fintype to magically generate the instances for Fintypes, but ran into issues over npow and zpow. Is there a way to get the deriver to work for such structures with autoParam functions? I've provided a proof that npowRec is the unique inhabitant of the relevant subtype:

import Mathlib.Tactic.DeriveFintype
import Mathlib.Data.Fintype.Pi

instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (One G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Mul G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Semigroup G) := derive_fintype% _

lemma np_inj {G : Type _} [Semigroup G] [One G]
    (np np' : ℕ → G → G) (nph0 : ∀ x, np 0 x = 1) (nph0' : ∀ x, np' 0 x = 1)
    (nph1 : ∀ n x, np (n + 1) x = x * np n x)
    (nph1' : ∀ n x, np' (n + 1) x = x * np' n x) : np = np' := by
  ext n x
  induction' n with n IH generalizing x <;>
  simp_all

instance np_unique {G : Type _} [Semigroup G] [One G] :
    Unique {np : ℕ → G → G // (∀ x, np 0 x = 1) ∧ (∀ n x, np (n + 1) x = x * np n x)} :=
  ⟨⟨npowRec, by intros; rfl, by intros; rfl⟩,
    λ f => (Subtype.ext
      (np_inj _ _ f.prop.left (by intros; rfl) f.prop.right (by intros; rfl)))⟩

instance np_fintype {G : Type _} [Semigroup G] [One G] :
    Fintype {np : ℕ → G → G // (∀ x, np 0 x = 1) ∧ (∀ n x, np (n + 1) x = x * np n x)} :=
  np_unique.fintype

instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Monoid G) := derive_fintype% _ -- fails,
-- probably because can't show that there are finite `npow`

instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Div G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Inv G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (DivInvMonoid G) := derive_fintype% _ -- fails,
-- probably because can't show that there are finite `zpow`

instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Group G) := derive_fintype% _

[Yury G. Kudryashov]

Do we have an ext lemma from Group to Mul?

[Yury G. Kudryashov]

I know nothing about derive_fintype%. As for Finite (Group G), you can easily get it from an injective map to G -> G -> G.

[Yury G. Kudryashov]

Some time ago, I started (then abandoned) a branch where I merged npow and rules into 1 structure.

[Yury G. Kudryashov]

This structure is a Subsingleton.

[Eric Wieser]

Yury G. Kudryashov said:

Do we have an ext lemma from Group to Mul?

docs4#Group.ext

[Kyle Miller]

derive_fintype% t is short for Fintype.ofEquiv _ (proxy_equiv% t), and you can see what equivalence it is generating with

#check fun G => proxy_equiv% (Monoid G)
/-
fun G ↦
  Monoid.proxyTypeEquiv
    G : (G : Type u_1) →
  (toSemigroup : Semigroup G) ×
      (toOne : One G) ×
        (_ : PLift (∀ (a : G), 1 * a = a)) ×
          (_ : PLift (∀ (a : G), a * 1 = a)) ×
            (npow : ℕ → G → G) ×
              (_ : PLift (autoParam (∀ (x : G), npow 0 x = 1) _auto✝)) ×
                PLift (autoParam (∀ (n : ℕ) (x : G), npow (n + 1) x = x * npow n x) _auto✝¹) ≃
    Monoid G
-/

It's just relying on whatever instances Mathlib has to create a Fintype instance, and there aren't any instances that can see that the ℕ → G → G is determined by the following two fields.

Potentially the proxy_equiv% elaborator could be made aware of which fields are functions of the others due to Prop fields and omit them. I don't think being aware of autoParam is sufficient though since you also need the Subsingleton proof that Yury mentioned.

[Yakov Pechersky]

Here is the full proof up to Fintype (Group), where I do provide the Unique, and thus Fintype, instances.

import Mathlib.Tactic.DeriveFintype
import Mathlib.Data.Fintype.Pi

instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (One G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Mul G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Semigroup G) := derive_fintype% _

lemma np_inj {G : Type _} [Mul G] [One G]
    (np np' : ℕ → G → G) (nph0 : ∀ x, np 0 x = 1) (nph0' : ∀ x, np' 0 x = 1)
    (nph1 : ∀ n x, np (n + 1) x = x * np n x)
    (nph1' : ∀ n x, np' (n + 1) x = x * np' n x) : np = np' := by
  ext n x
  induction' n with n IH generalizing x <;>
  simp_all

instance np_unique {G : Type _} [Mul G] [One G] :
    Unique {np : ℕ → G → G // (∀ x, np 0 x = 1) ∧ (∀ n x, np (n + 1) x = x * np n x)} :=
  ⟨⟨npowRec, by intros; rfl, by intros; rfl⟩,
    λ f => (Subtype.ext
      (np_inj _ _ f.prop.left (by intros; rfl) f.prop.right (by intros; rfl)))⟩

instance np_fintype {G : Type _} [Mul G] [One G] :
    Fintype {np : ℕ → G → G // (∀ x, np 0 x = 1) ∧ (∀ n x, np (n + 1) x = x * np n x)} :=
  np_unique.fintype

instance {G : Type _} [Semigroup G] [One G] : Fintype (@Sigma (ℕ → G → G) fun npow ↦
    (_ : PLift ((∀ (x : G), npow 0 x = 1))) ×
    PLift ((∀ (n : ℕ) (x : G), npow (n + 1) x = x * npow n x))) :=
  Fintype.ofEquiv {np : ℕ → G → G // (∀ x, np 0 x = 1) ∧ (∀ n x, np (n + 1) x = x * np n x)} {
    toFun := λ ⟨f, hf⟩ => ⟨f, PLift.up hf.left, PLift.up hf.right⟩
    invFun := λ ⟨f, hf⟩ => ⟨f, hf.fst.down, hf.snd.down⟩
    left_inv := λ ⟨f, hf⟩ => by simp
    right_inv := λ ⟨f, hf⟩ => by simp
  }

instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Monoid G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Div G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Inv G) := derive_fintype% _

lemma zp_inj {G : Type _} [Mul G] [One G] [Inv G]
    (zp zp' : ℤ → G → G) (zph0 : ∀ x, zp 0 x = 1) (zph0' : ∀ x, zp' 0 x = 1)
    (zph1 : ∀ (n : ℕ) (a : G), zp (Int.ofNat (Nat.succ n)) a = a * zp (Int.ofNat n) a)
    (zph1' : ∀ (n : ℕ) (a : G), zp' (Int.ofNat (Nat.succ n)) a = a * zp' (Int.ofNat n) a)
    (zphn : ∀ (n : ℕ) (a : G), zp (Int.negSucc n) a = (zp (Int.ofNat (Nat.succ n)) a)⁻¹)
    (zphn' : ∀ (n : ℕ) (a : G), zp' (Int.negSucc n) a = (zp' (Int.ofNat (Nat.succ n)) a)⁻¹) :
    zp = zp'
    := by
  ext n x
  induction' n with n n generalizing x
  · induction n
    · simp_all
    · simp_all
  · rw [zphn, zphn', zph1, zph1']
    congr
    induction n
    · simp_all
    · simp_all


instance zp_unique {G : Type _} [Mul G] [One G] [Inv G] :
    Unique {zp : ℤ → G → G // (∀ x, zp 0 x = 1) ∧
      (∀ (n : ℕ) (a : G), zp (Int.ofNat (Nat.succ n)) a = a * zp (Int.ofNat n) a) ∧
      (∀ (n : ℕ) (a : G), zp (Int.negSucc n) a = (zp (Int.ofNat (Nat.succ n)) a)⁻¹)} :=
  ⟨⟨zpowRec, by intros; rfl, by intros; rfl, by intros; rfl⟩,
    λ f => (Subtype.ext (zp_inj _ _ f.prop.left (by intros; rfl) f.prop.right.left (by intros; rfl)
      f.prop.right.right (by intros; rfl)))⟩

instance zp_fintype {G : Type _} [Mul G] [One G] [Inv G]:
    Fintype {zp : ℤ → G → G // (∀ x, zp 0 x = 1) ∧
      (∀ (n : ℕ) (a : G), zp (Int.ofNat (Nat.succ n)) a = a * zp (Int.ofNat n) a) ∧
      (∀ (n : ℕ) (a : G), zp (Int.negSucc n) a = (zp (Int.ofNat (Nat.succ n)) a)⁻¹)} :=
  zp_unique.fintype

instance {G : Type _} [Mul G] [One G] [Inv G] : Fintype (@Sigma (ℤ → G → G) fun zpow ↦
  (_ : PLift ((∀ (a : G), zpow 0 a = 1))) ×
    (_ : PLift ((∀ (n : ℕ) (a : G), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a))) ×
      PLift ((∀ (n : ℕ) (a : G), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) a)⁻¹))) :=
  Fintype.ofEquiv {zp : ℤ → G → G // (∀ x, zp 0 x = 1) ∧
      (∀ (n : ℕ) (a : G), zp (Int.ofNat (Nat.succ n)) a = a * zp (Int.ofNat n) a) ∧
      (∀ (n : ℕ) (a : G), zp (Int.negSucc n) a = (zp (Int.ofNat (Nat.succ n)) a)⁻¹)} {
    toFun := λ ⟨f, hf⟩ => ⟨f, PLift.up hf.left, PLift.up hf.right.left, PLift.up hf.right.right⟩
    invFun := λ ⟨f, hf⟩ => ⟨f, hf.fst.down, hf.snd.fst.down, hf.snd.snd.down⟩
    left_inv := λ ⟨f, hf⟩ => by simp
    right_inv := λ ⟨f, hf, hf', hf''⟩ => by simp
  }
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (DivInvMonoid G) := derive_fintype% _
instance {G : Type _} [Fintype G] [DecidableEq G] : Fintype (Group G) := derive_fintype% _

[Yakov Pechersky]

And, nicely, one can now "brute force":

lemma foo : Fintype.card (Group Unit) = 1 := by decide

[Yakov Pechersky]

But unfortunately, it slows to a half for me, for

lemma foo2 : Fintype.card (Group Bool) = 2 := by decide

failing with a deterministic timeout

[Eric Wieser]

I would hope there's a way of doing this that doesn't require repeating the proofs about npow in Monoid.ext

[Eric Wieser]

Something like considering the subtype

{ omi : G × (G → G → G) × (G → G) // ∃ h1 h2 ..., Group.mk ... }
  ≃ Group G

[Kevin Buzzard]

You only need the multiplication!

[Eric Wieser]

Not if you want to be constructive!

[Eric Wieser]

(sure, you can find inv and one constructively by iteration; but it's easier to just declare all three and let the fintype machinery iterate)

[Kevin Buzzard]

If I'm actually counting the number of group structures on a type of size n then surely it's easier to just loop over the multiplications the moment n>=2?

[Eric Wieser]

If you only want to count them, yes; but Fintype (Group G) asks you to construct each one too

[Eric Wieser]

Also, it's not clear to me how you check the multiplication forms a group without identifying the inverse and identity along the way

[Johan Commelin]

Wasn't there some weird 1-axiom characterisation of groups?

[Eric Wieser]

Yes, but none are in terms of solely multiplication