defeq diamond with MonoidalCategory ofFiniteLimits

Stream: mathlib4

[Edward van de Meent]

while trying to prove that elementary topoi have finite colimits, i've run into the following defeq-diamond issue:

import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

universe v u
namespace CategoryTheory
open Limits

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

example : (monoidalOfHasFiniteProducts C) =
    (CartesianMonoidalCategory.ofHasFiniteProducts (C := C)).toMonoidalCategory := by
  try rfl -- fails
  dsimp [monoidalOfHasFiniteProducts, CartesianMonoidalCategory.ofHasFiniteProducts,
    CartesianMonoidalCategory.ofChosenFiniteProducts]
  congr
  · sorry
  · sorry
  · congr! 6
    rename_i X₁ X₂ X₃ X₄ f g
    sorry
  all_goals sorry

end CategoryTheory

it appears the issue is that prod.map f g = CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom (fun x1 x2 ↦ getLimitCone (pair x1 x2)) f g is not rfl...

[Aaron Liu]

with this much choice I'm not really surprised

[Edward van de Meent]

it's not that terribly different though, this should just be defeq? they assume the same Nonempty structures

[Edward van de Meent]

down the line the difference is exactly where you match on Discrete WalkingPair (i.e. how you create the relevant cone)

[Aaron Liu]

after unfolding everything and applying congr I get

import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

universe v u
namespace CategoryTheory
open Limits

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

theorem CategoryTheory._example.extracted_1 {C : Type u} [inst : Category.{v, u} C] [inst_1 : HasFiniteLimits C]
    (X₁ X₂ X₃ X₄ : C) (f : X₁ ⟶ X₂) (g : X₃ ⟶ X₄) :
    (fun X => (getLimitCone (pair X₁ X₃)).cone.π.app X ≫
      WalkingPair.rec (motive := fun x =>
          (pair X₁ X₃).obj (Discrete.mk x) ⟶ (pair X₂ X₄).obj (Discrete.mk x))
        f g X.as) =
    (fun x =>
      WalkingPair.rec
        ((getLimitCone (pair X₁ X₃)).cone.π.app (Discrete.mk WalkingPair.left) ≫ f)
        ((getLimitCone (pair X₁ X₃)).cone.π.app (Discrete.mk WalkingPair.right) ≫ g) x.as) := by
  try rfl -- fails
  sorry

end CategoryTheory

[Edward van de Meent]

exactly

[Aaron Liu]

I guess it's not the choice's fault

[Andrew Yang]

I think monoidalOfHasFiniteProducts is not meant to be used. See the todo in the file containing that construction. cc @Yaël Dillies

[Edward van de Meent]

sure, but then what should i do now? because that means that right now, we don't have that the monoidal category structure of CartesianMonoidalCategory.ofHasFiniteLimits is symmetric? and i think it still would be nice to have these things be defeq?

[Yaël Dillies]

Every cartesian-monoidal category structure is symmetric. All you need to do is to show it's braided (which is data, so that shouldn't be inferred automatically)

[Aaron Liu]

@loogle "braided", "cartesian"

[loogle]

:search: CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory, CategoryTheory.CartesianMonoidalCategory.instNonemptyBraidedCategory, and 1 more

[Aaron Liu]

well it's nonempty and subsingleton

[Aaron Liu]

@loogle "symmetric", "cartesian"

[loogle]

:search: CategoryTheory.CartesianMonoidalCategory.instSubsingletonSymmetricCategory, CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory

[Aaron Liu]

oh there's an instance inferring symmetric from braided called docs#CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory

[Yaël Dillies]

Indeed, this is what I was referring to by "All you need to do is to show it's braided"

[Edward van de Meent]

ok. So then the question becomes: is it sensible to (for now) change the defeq of the CartesianMonoidalCategory instance to lign up with the generic one?

[Yaël Dillies]

Which CartesianMonoidalCategory instance and what's the "generic one"?

[Edward van de Meent]

the ones mentioned in my first MWE?

[Yaël Dillies]

Which is which?

[Edward van de Meent]

by generic, i meant the instance for just MonoidalCategory, i.e. monoidalOfHasFiniteProducts

[Yaël Dillies]

You know what, it's easier to bust monoidalOfHasFiniteProducts than to have this discussion. Give me 10min :runner:

[Joël Riou]

Yes, this is a TODO https://github.com/leanprover-community/mathlib4/blob/5c98c223ad372ac3992aa23bd2a4a67cd6a9b13f/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean#L24-L25

[Yaël Dillies]

#30684

[Edward van de Meent]

great, so you just worsen mathlib without replacement. excellent idea

[Yaël Dillies]

What do you mean? I have just spent 30min of my life documenting the replacements to declarations that are now completely unused in mathlib!

[Yaël Dillies]

Maybe the question I should have started with: How did you end up with monoidalOfHasFiniteProducts in your goal?

[Edward van de Meent]

symmetricOfHasFiniteProducts uses it for the MonoidalCategoryStruct, iirc

[Yaël Dillies]

How did you end up with symmetricOfHasFiniteProducts in your goal?

[Edward van de Meent]

elementary topoi (cartesian closed categories with finite limits and subobject classifier) are finitely cocomplete because the (contravariant) functor mapping an object X to the object (exp X).obj Ω is monadic. showing this requires us to construct a map X -> (exp ((exp X).obj Ω)).obj Ω, which is precisely induced by evaluating after braiding

[Edward van de Meent]

i.e. this diagram

[Joël Riou]

Do not use monoidalOfHasFiniteProducts. Add a CartesianMonoidalCategory assumption instead.

[Edward van de Meent]

are you saying i shouldn't be working with HasFiniteLimits then?

[Andrew Yang]

Can you please unxy yourself by providing a mwe or at least some pointer to some existing code?

[Andrew Yang]

The intended way to equip a concrete category with HasFiniteLimits with a symmetric monoidal category structure is

import Mathlib

open CategoryTheory Limits

universe v u

noncomputable section

def MyCat : Type u := sorry
instance : Category.{v} MyCat := sorry
instance : HasFiniteLimits MyCat := sorry
instance : CartesianMonoidalCategory MyCat := .ofHasFiniteProducts
instance : BraidedCategory MyCat := .ofCartesianMonoidalCategory
example : SymmetricCategory MyCat := inferInstance

The intended way to assume you have an arbitrary symmetric monoidal cartesian category is via

import Mathlib

open CategoryTheory Limits

variable {C : Type*} [Category C] [CartesianMonoidalCategory C] [BraidedCategory C]

[Edward van de Meent]

right, and what is the intended way to assume a category is an elementary topos?

[Edward van de Meent]

personally i was feeling (𝒞 : Classifier C) [HasFiniteLimits C] [CartesianClosed C]

[Edward van de Meent]

(find my project here)

[Edward van de Meent]

the finitely cocomplete is necessary to prove that there is a heytingalgebra structure on morphisms into a subobject classifier from a specific object

[Andrew Yang]

I think (𝒞 : Classifier C) [HasFiniteLimits C] [CartesianMonoidalCategory C] [CartesianClosed C]

[Edward van de Meent]

that looks very weird to me, tbh. you're doubling your finite products for whatever reason

[Yaël Dillies]

Doesn't CartesianMonoidalCategory imply HasFiniteLimits?

[Andrew Yang]

But the point is CartesianMonoidalCategory contains a choice of defeqs for the product. I mean you can also do HasEqualizers C instead of HasFiniteLimits C but I don't see the point.

[Yaël Dillies]

Andrew, are you saying it doesn't mathematically imply it, or that we are missing the instance in mathlib?

[Edward van de Meent]

i think the first

[Andrew Yang]

CartesianMonoidalCategory only implies has finite products

[Andrew Yang]

Andrew Yang said:

But the point is CartesianMonoidalCategory contains a choice of defeqs for the product. I mean you can also do HasEqualizers C instead of HasFiniteLimits C but I don't see the point.

If both CartesianClosed and Classifier were prop valued I can see an argument that we would prefer the prop valued HasFiniteLimits too but I think if we are fixing the choice of internal homs and classifiers then fixing the product is also reasonable.

[Edward van de Meent]

(classifier contains data)

[Andrew Yang]

So is CartesianClosed. That's precisely my point.

[Edward van de Meent]

so then i guess we need a way to fix all finite limits?

[Edward van de Meent]

(if that's a thing you can do)

[Andrew Yang]

I think [HasFiniteLimits C] [CartesianMonoidalCategory C] is fine for now?

[Yaël Dillies]

Ah yes sorry, I clearly can't read