API for interface of ChosenFiniteProducts and FiniteProducts

Stream: mathlib4

[Sina Hazratpour 𓃵]

I want to prove the following lemma which i had hoped simp or aesop would do, that is not the case. An extremely ugly proof which unfold everything down to the API of limits can be found, but it if that is the only proof, then that suggest some API is missing.

Here's a mwe:

import Mathlib.CategoryTheory.ChosenFiniteProducts

noncomputable section

universe v₁ u₁

namespace CategoryTheory

open Category Limits MonoidalCategory ChosenFiniteProducts

attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
attribute [local instance] monoidalOfChosenFiniteProducts

variable {C : Type u₁} [Category.{v₁} C] [HasFiniteLimits C]

lemma foo {X : C} {A A' : C} {g : A ⟶ A'} : X ◁ g = prod.map (𝟙 X) g := by
  sorry

end CategoryTheory

[Andrew Yang]

Perhaps

lemma foo {X : C} {A A' : C} {g : A ⟶ A'} : X ◁ g = prod.map (𝟙 X) g := by
  ext
  · simp only [whiskerLeft_fst]
    exact (Category.comp_id _).symm.trans (prod.map_fst (𝟙 X) g).symm
  · simp only [whiskerLeft_snd]
    exact (prod.map_snd (𝟙 X) g).symm

[Markus Himmel]

I would say that you're not supposed to be in this situation where one side has morphisms involving X ⊗ Z and the other has morphisms involving X ⨯ Z. So if possible I would say you should back up and see how you ended up in this situation.

[Sina Hazratpour 𓃵]

Interesting! The reason my proof got long was that simp [prod.map_fst] or rw [prod.map_fst (𝟙 X) g] was not working after the first line. Any idea as to why?

[Markus Himmel]

What I'm saying is you shouldn't even be talking about prod.map (𝟙 X) g, but about (𝟙 X) ⊗ g.

[Andrew Yang]

I have no idea what the actual use case is but what if the right hand side is some generic category-theoretic construct which simps to that.

[Sina Hazratpour 𓃵]

Markus Himmel said:

I would say that you're not supposed to be in this situation where one side has morphisms involving X ⊗ Z and the other has morphisms involving X ⨯ Z. So if possible I would say you should back up and see how you ended up in this situation.

i don't know about that; Sometimes you want to promote HasFiniteProduct to ChosenFiniteProduct. In particular, i am solving a TODO in CategoryTheory.Over.Pullback which asks to show if a category C is cartesian closed then star X : C ⥤ Over X
has a right adjoint sectionsFunctor. Now, star is defined by the algebras of the prodComonad which uses HasBinaryProducts while the right adjoint (the section functor) only makes sense in the cartesian closed structure coming from the following instances:

attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
attribute [local instance] monoidalOfChosenFiniteProducts

Therefore the need to have interface lemma like i mentioned.

unless we redo star and directly define it in terms of ChosenFiniteProducts! But where does the buck stop with this approach, we don't want to replace all HasFiniteProducts with ChosenFiniteProducts, do we?

[Markus Himmel]

Could you share a mathlib branch so that I can see the place in your code where you need this?

[Sina Hazratpour 𓃵]

it's in the file CategoryTheory.Comma.Over.Sections of the LCCC PR:

https://github.com/leanprover-community/mathlib4/pull/21525/files#diff-be27792f64b32cb78937c6244c8d305283c48d5c725fff684bf1dc21882a9a32

[Sina Hazratpour 𓃵]

The last line of homEquiv_naturality_left_symm in coreHomEquiv(line 173) uses

lemma whiskerLeft_prod_map {A A' : C} {g : A ⟶ A'} : I ◁ g = prod.map (𝟙 I) g := by

[Markus Himmel]

So my claim here is that the real problem is in the definition of sectionsUncurry. Here you're constructing something using Over.homMk ?_ ?_, and the first thing is supposed to be of the form ((star I).obj A).left ⟶ X.left. The dsimp-normal form of that is I ⨯ A ⟶ X.left, but you're providing something of type I ⊗ A ⟶ X.left and this leads to the problems down the line.

I claim that the correct way to fix this would be this: introduce an explicit isomorphism

def prodIsoTensorObj (X Y : C) : X ⨯ Y ≅ X ⊗ Y := Iso.refl _

which translates between the monoidal world and the binary product world, and show that under this iso, prod.fst becomes ChosenFiniteProducts.fst, prod.map becomes tensor, etc.

I have applied this to your code and I think things are working better; for example, some terminal rfl are no longer there because simp can solve goals by itself: https://github.com/leanprover-community/mathlib4/commit/b9152e80d4ed675dc691a76071f08b0a04b5e455

[Sina Hazratpour 𓃵]

Very good observation!
Now that I look back, this is also the same way we did it in LCCCs, we constructed and used a dependent version of prodIsoTensorObj.

[Sina Hazratpour 𓃵]

@Markus Himmel I'm not great with the git, what is the git command to merge your last commit on that branch?

[Markus Himmel]

git merge markus/sina should work

[Sina Hazratpour 𓃵]

I'm on the branch sina-locally-cartesian-closed-categories and git merge markus/sina results in
merge: markus/sina - not something we can merge

[Sina Hazratpour 𓃵]

ah, never mind, ofc i forgot origin haha. now it's merged, thanks!