Groups: direct products vs category-theoretic products

Stream: Is there code for X?

[Roberto Zunino]

I am trying to prove that the product objects in AddGrpCat are isomorphic to the direct products of AddGroups.

I guess this is already available in mathlib in some form. I tried Loogle/LeanSearch/..., but I could not find anything that allowed me to conclude the proof. Perhaps it is a special case of a more general result I can't think of. (I could try constructing the Iso myself, but I'd rather exploit some existing result.)

import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.Algebra.Category.Grp.CartesianMonoidal
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

open CategoryTheory

noncomputable example (G H : Type) [AddGroup G] [AddGroup H] :
    AddGrpCat.of G ⨯ AddGrpCat.of H ≅ AddGrpCat.of (G × H) := sorry

[Aaron Liu]

Try Iso.refl _

[Roberto Zunino]

I get a type mismatch error from Iso.refl _. The two sides are not defeq.

[Kenny Lau]

in fact they can't be defeq, the lhs is the arbitrary chosen limit by docs#CategoryTheory.Limits.prod

[Kenny Lau]

@Roberto Zunino

import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.Algebra.Category.Grp.CartesianMonoidal
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

open CategoryTheory

noncomputable example (G H : Type) [AddGroup G] [AddGroup H] :
    AddGrpCat.of G ⨯ AddGrpCat.of H ≅ AddGrpCat.of (G × H) :=
  CategoryTheory.Limits.limit.isoLimitCone <| AddGrpCat.binaryProductLimitCone (.of G) (.of H)

[Kenny Lau]

i found that by Loogle AddGrpCat, "prod"

[Yaël Dillies]

May I suggest you use .of G ⊗ .of H instead? This one is defined as you expected

[Yaël Dillies]

Here is what I mean:

import Mathlib.Algebra.Category.Grp.CartesianMonoidal

open CategoryTheory MonoidalCategory

example (G H : Type) [AddGroup G] [AddGroup H] :
    .of G ⊗ .of H ≅ AddGrpCat.of (G × H) := .refl _

[Kevin Buzzard]

Yikes we have ⊗ and ⨯ on AddGrpCat and they're doing the same thing but are not defeq?

[Yaël Dillies]

They are not equal to each other, merely canonically isomorphic

[Kevin Buzzard]

Sure, but I guess I'm saying that this is perhaps counterintuitive? Usually we only have one definition of a thing. I can't make another definition of the naturals and PR it to mathlib and say "it's Ok, it's not defeq to Nat but it is canonically isomorphic".

[Joël Riou]

⨯ is the notation for the categorical product in any category (the axiom of choice is used to choose a limit), while ⊗ is the notation for the tensor product on cartesian monoidal categories, which is a definition that we have carefully chosen so that it has nice defeq (for example, in the category of types, this is the cartesian product of types).

[Joël Riou]

Basically, we should refrain from using ⨯ when working in a specific category where ⊗ is available.

[Kevin Buzzard]

Aah I see, and we cannot have "categorical product = tensor product" in general (because this isn't even true in e.g. modules over a commutative ring) so this is just a gotcha that we need to be aware of in this case. Thanks for the explanation!

[Adam Topaz]

Kevin, this is what evolved out of that old "ChosenFiniteProducts" stuff!