product of morphisms in product category

Stream: mathlib4

[Notification Bot]

Raphael Douglas Giles has marked this topic as unresolved.

[Raphael Douglas Giles]

Yaël Dillies said:

docs#CategoryTheory.prod says you are right. Try doing #check F.map (Prod.mk f1 f2 : (X1, X2) ⟶ (Y1, Y2))

Why do we need to provide the type annotations here? We can't tell from reading the docs why that should be necessary

[Yaël Dillies]

because X ⟶ Y isn't reducibly defeq to (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)

[Fernando Chu]

Yaël Dillies said:

because X ⟶ Y isn't reducibly defeq to (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)

It seems to me that we need something weaker, i.e. that (X1, X2) ⟶ (Y1, Y2) = (X1 ⟶ Y1) × (X2 ⟶ Y2), and this is is the case:

  let a := (X1, X2) ⟶ (Y1, Y2)
  let b := (X1 ⟶ Y1) × (X2 ⟶ Y2)
  have : a = b := by
    unfold a b
    dsimp

So we're unsure of what's going on here.

[Yaël Dillies]

Can you provide a #mwe ?

[Fernando Chu]

import Mathlib
import Mathlib.CategoryTheory.Products.Basic
open CategoryTheory

def hom_product {C: Type u} [Category.{v} C] {F: Functor (C × C) C} {X1 X2 Y1 Y2: C} {f1: X1 ⟶ Y1} {f2: X2 ⟶ Y2}:
  (X1, X2) ⟶ (Y1, Y2) := by

  let a := (X1, X2) ⟶ (Y1, Y2)
  let b := (X1 ⟶ Y1) × (X2 ⟶ Y2)
  have : a = b := by
    unfold a b
    dsimp
  simp at a

[Yaël Dillies]

Here is the solution:

import Mathlib.CategoryTheory.Products.Basic

open CategoryTheory

def hom_product {C: Type u} [Category.{v} C] {X1 X2 Y1 Y2: C} {f1: X1 ⟶ Y1} {f2: X2 ⟶ Y2}:
    (X1, X2) ⟶ (Y1, Y2) :=
  ⟨f1, f2⟩

[Yaël Dillies]

Now what is your question, exactly? :sweat_smile:

[Fernando Chu]

We want to understand why we can't apply F.map to the morphism ⟨f1, f2⟩; the original question mentioned that:

check F.map (Prod.mk f1 f2) -- error

gives an error.

As you suggested then, giving type annotations work. But we don't understand why this is needed, since (X1, X2) ⟶ (Y1, Y2) = (X1 ⟶ Y1) × (X2 ⟶ Y2) definitionally. Lean knows the type of ⟨f1, f2⟩ is the rhs of the equation, so it should be able to infer that what we mean by F.map (Prod.mk f1 f2), but it doesn't.

Always giving type annotations is quite cumbersome when dealing with a lot of profunctors, this is furthermore a context where currying is not always possible.

[Yaël Dillies]

In the mean time, I reverse-engineered your MWE to the following:

import Mathlib.CategoryTheory.Products.Basic

open CategoryTheory

variable {C : Type*} [Category C] {X₁ X₂ Y₁ Y₂ : C} {F : C × C ⥤ C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂}

#check F.map (Prod.mk f₁ f₂)
/-
Application type mismatch: In the application
  (?m.297, f₂)
the argument
  f₂
has type
  X₂ ⟶ Y₂ : Type ?u.117
but is expected to have type
  ?m.264.2 ⟶ ?m.265.2 : Type ?u.117
-/

[Yaël Dillies]

(In the future, please provide a MWE that actually displays the error you want people to see!)

[Fernando Chu]

Sorry for being unclear, my questions were meant to be a continuation of the original question, so I was talking about that specific MWE.

[Yaël Dillies]

Since X ⟶ Y for X Y : C × C is defined as (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2), when trying to solve for Prod.mk f₁ f₂ : ?X ⟶ ?Y, Lean unfolds this to Prod.mk f₁ f₂ : (?X.1 ⟶ ?Y.1) × (?X.2 ⟶ ?Y.2)

[Yaël Dillies]

It then tries to match X₁ with ?X.1, Y₁ with ?Y.1, X₂ with ?X.2, Y₂ with ?Y.2

[Robin Carlier]

My experience with morphisms in product categories is also that they’re a pain, and that you have to provide annotations at random places.

Should they be refactored to be a two-field struct that would let us write ⟨f₁, f₂⟩? I don’t think we gain much by wanting the homs to be defeq to a product, just that it "behaves like a product".

[Yaël Dillies]

This is where the algorithm gets stuck, since it doesn't know it can set ?X := (X₁, X₂), ?Y := (Y₁, Y₂)

[Yaël Dillies]

Robin Carlier said:

Should they be refactored to be a two-field struct that would let us write ⟨f₁, f₂⟩? I don’t think we gain much by wanting the homs to be defeq to a product, just that it "behaves like a product".

That wouldn't fix anything here, cf my explanation before and after your message

[Yaël Dillies]

What you need is a constructor of the form (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → ((X₁, X₂) ⟶ (Y₁, Y₂)), as opposed to the current Prod.mk : (X.1 ⟶ Y.1) → (X.2 ⟶ Y.2) → (X ⟶ Y)

[Yaël Dillies]

docs#CategoryTheory.Over.homMk is painful to use for the same reason

[Yaël Dillies]

docs#MulEquiv.toCommGrpIso also follows the bad pattern

[Yaël Dillies]

In contrast, docs#CommRingCat.ofHom is well-designed

[Robin Carlier]

Welp, if the solution is that easy, #26206, and I guess there’ll be a second PR to use it instead of type annotations everywhere, but this will be more of a pain to write.

[Fernando Chu]

Yaël Dillies said:

This is where the algorithm gets stuck, since it doesn't know it can set ?X := (X₁, X₂), ?Y := (Y₁, Y₂)

Thanks for the clear explanation! I don't understand why it gets stucked here but the proposed solution works, so all is great now :)