theorem direct_product_abelian_iff_factor_abelian

Stream: maths

[Move fast]

image.png

import Mathlib

instance direct_product_abelian_of_factor_abelian
  {n : ℕ} {G : Fin n → Type*} [∀ i, CommGroup (G i)] :
  CommGroup (Π i, G i) := by
  refine { toGroup := Pi.group ,
           mul_comm := by
            intro x y
            ext i
            exact mul_comm (x i) (y i) }

instance factor_abelian_of_direct_product_abelian
    {n : ℕ} {G : Fin n → Type*} [∀ i, Group (G i)]
    (hc : CommGroup (Π i, G i)) :
    ∀ i, CommGroup (G i) :=
  fun i =>
    { toGroup := inferInstance
      mul_comm := fun x y => by
        let f : Π j, G j := fun j => if h : j = i then cast (congrArg G (Eq.symm h)) x else 1
        let g : Π j, G j := fun j => if h : j = i then cast (congrArg G (Eq.symm h)) y else 1
       }

How can I get the result? I try some ways but I couldn't solve it.
And then I want to use them to show:

/-- The direct product of groups is abelian if and only if each factor group is abelian. -/
theorem direct_product_abelian_iff_factor_abelian {n : ℕ} {G : Fin n → Type*} [∀ i, Group (G i)] :
  (∀ i : Fin n, CommGroup (G i)) ↔ CommGroup (Π i : Fin n, G i) := by sorry

But I meet a problem:
image.png

[Kevin Buzzard]

Did an LLM write this code? Where did the question come from? Why do you want to solve this question?

[Move fast]

Yes, I asked the LLM but I could't understand it. The question is from my textbook：A direct product of groups is abelian if and only if each of the factors is abelian. I want to try to solve it by Lean 4. In fact, I show it by

import Mathlib
variable {n : ℕ}
variable {G : Fin n → Type*} [∀ i, Group (G i)]
theorem direct_product_abelian_iff_factor_abelian :
    (∀ f g : (i : Fin n) → G i, ∀ j, (f * g) j = (g * f) j) ↔
    (∀ i : Fin n, ∀ x y : G i, x * y = y * x)
     :=
by
  apply Iff.intro
  -- (⇒) If the direct product is abelian, then each factor group is abelian.
  · intro h_direct
    intros i x y
    let f : (i : Fin n) → G i := fun j => if h : j = i then by
      rw [h]; exact x
    else 1
    -- For indices other than `i`, set `f` to the identity element `1`.
    let g : (i : Fin n) → G i := fun j => if h : j = i then by
      rw [h]; exact y
    else 1
    have hfj : f i = x := by
      simp [f]
    have hgj : g i = y := by
      simp [g]
    specialize h_direct f g i
    change x * y = y * x
    have eq1 : (f * g) i = f i * g i := rfl
    have eq2 : (g * f) i = g i * f i := rfl
    rw [eq1, eq2] at h_direct
    rw [hfj, hgj] at h_direct
    exact h_direct
  -- (⇐) If each factor group is abelian, then the direct product is abelian.
  · intro h_factors
    intros f g j
    dsimp [(· * ·)]
    exact h_factors j (f j) (g j)

However, I want to try to show it by using the type like

instance direct_product_abelian_of_factor_abelian (hc : ∀ i : Fin n, CommGroup (G i)) :
CommGroup (Π i : Fin n, G i) := by sorry

instance factor_abelian_of_direct_product_abelian (hc :CommGroup (Π i : Fin n, G i) ) :
∀ i : Fin n, CommGroup (G i) := by sorry

[Kevin Buzzard]

I would strongly discourage the use of an LLM. Your first instance does not prove that the product of commutative groups is commutative, it proves something which looks like this but in fact says something else. None of your other code in your original post compiles. So I would say that the LLM output is worse than useless; everything is wrong and misleading.

[Kevin Buzzard]

The Lean thing you need to understand is that CommGroup X does not say "the group X is commutative". So all the stuff you're writing like

instance direct_product_abelian_of_factor_abelian (hc : ∀ i : Fin n, CommGroup (G i)) :
CommGroup (Π i : Fin n, G i) := by sorry

is not correct at all, and an LLM will not teach you this. I would strongly recommend that you read #mil or some other textbook. LLMs are not ready to teach you Lean in 2025 unfortunately.

[Kevin Buzzard]

A term of type CommGroup X is a commutative group structure on X which can be completely unrelated to any group structure already on X. CommGroup is not a Prop, it's a Type, it contains a new multiplication.

[Move fast]

OK, thank you for your suggestion. I am ready to read #mil.