Example of proving a category has exponential

Stream: Is there code for X?

[Yiming Xu]

I am trying to familiarize myself with constructions in Lean (type classes/structures, basically) by proving a particular category has exponential. But the definition of exponential in Lean takes quite a while to decode. May I please ask if there is a formalization of a particular category to be exponentiable? It does not matter what the concrete category is (the simpler the better, actually), the main point for me is to get to know the workflow.

Thanks in advance for any attempt to help!

[Joël Riou]

You may look at https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/Rep.html#Rep.instMonoidalClosed

[Yiming Xu]

Thanks! It is very helpful!

But as a beginner, I am confused at:

class MonoidalClosed (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C] where
  closed (X : C) : Closed X := by infer_instance

May I please ask what is infer_instance doing here? If possible, I would like to hear about the workflow of infer_instance in this particular case, what does it invoke step-by-step?

[Abraham Solomon]

Yiming Xu said:

Thanks! It is very helpful!

But as a beginner, I am confused at:

class MonoidalClosed (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C] where
  closed (X : C) : Closed X := by infer_instance

May I please ask what is infer_instance doing here? If possible, I would like to hear about the workflow of infer_instance in this particular case, what does it invoke step-by-step?

https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#inferInstance

I believe in this case, it has to infer the instance of X:C -- and it will raise an error if the inferred instance does not inhabit Closed.

[Yiming Xu]

Thanks for the swift reply! I was confused why we are not required to provide an adjunction. And the reason is that there is no uniform way to construct such a function, but as long as X is closed, the instance [Closed X] should already be stored somewhere, so we just need to tell Lean to try to find it out. (Thanks for correcting me if I am wrong.)

[Yiming Xu]

I need to deal with product first. May I please then ask for a simple case where we construct the instance HasFiniteProduct in some category? The definition itself refers to limits, I would be a little bit surprised if it is necessary to prove the property of having products only by applying the definition directly.

[Abraham Solomon]

Yiming Xu said:

I need to deal with product first. May I please then ask for a simple case where we construct the instance HasFiniteProduct in some category? The definition itself refers to limits, I would be a little bit surprised if it is necessary to prove the property of having products only by applying the definition directly.

Might need an expert for that, sometimes it helps to go to the docs then go to source on github -- then at the top it tells you who wrote it.

If you happen to know they are still active on Zulip -- that could be a lead.

[Yiming Xu]

Makes sense. Thanks for sharing this strategy! If I am not lucky enough to have an expert visiting this post in one or two days I may try grabbing one.

[Kim Morrison]

Hi @Yiming Xu! Are you the Yiming who did a project on HoTT with me? Welcome! I'm offline for a day but if you haven't got answers by then I can help you find examples.

[Yiming Xu]

Yes, I am Yiming Xu, the one you know from undergraduate. Nice to meet you again on Lean Zulip! I am starting Lean4 from the user level.

[Yiming Xu]

No emergency and thanks so much for your time an patience!!! (And sorry that I have forgotten what you taught me before... It has been so many years...)

[Kevin Buzzard]

Yiming Xu said:

May I please ask what is infer_instance doing here?

:= in a class/structure definition means that if the field is not explicitly supplied by the user, then the system will attempt to supply it by running the code after the :=. Here for example, Closed is a class, so there is a chance that typeclass inference is able to fill in this field automatically; that's what infer_instance does.

[Yiming Xu]

Kevin Buzzard said:

Yiming Xu said:

May I please ask what is infer_instance doing here?

:= in a class/structure definition means that if the field is not explicitly supplied by the user, then the system will attempt to supply it by running the code after the :=. Here for example, Closed is a class, so there is a chance that typeclass inference is able to fill in this field automatically; that's what infer_instance does.

Thanks! That makes sense.

[Yiming Xu]

@Kim Morrison I think I would need some examples of how to prove a category has products in Lean. I find my lack of familiarity in type class makes it difficult for me to read all the relevant code. My particular aim would be to formalize that the category of right actions is cartesian closed. I explained my aim in this post #new members > Beginner formalizing group actions

[Yiming Xu]

I guess this is one place to look at:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/Action/Limits.html#Action.instHasFiniteProducts

[Kim Morrison]

It's a bit strange that that file even constructs the HasFiniteProducts instance, given that immediately afterwards it constructs the HasFiniteLimits instance which is more general.

[Kim Morrison]

Is that the situation for what you are trying to do?

[Kim Morrison]

What exactly do you mean by "the category of right actions"?

[Yiming Xu]

Kim Morrison said:

What exactly do you mean by "the category of right actions"?

I mean the category of right $M$-sets, where $M$ is a monoid. Objects are sets $X$ with an action $X\times M\to X$, and arrows are $M$-equivarient maps.

[Yiming Xu]

Kim Morrison said:

Is that the situation for what you are trying to do?

Let me check. I just found it this morning. But I am suspicious. What is a MonCat and why it is used here?

[Yiming Xu]

I see, MonCat just mean that G is a monoid.

[Yiming Xu]

So what are the missing argument in:

 (Action.functorCategoryEquivalence _ _).functor

in

instance [HasFiniteProducts V] : HasFiniteProducts (Action V G) where
  out _ :=
    Adjunction.hasLimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

?

[Yiming Xu]

And, this instance is obtained by transporting a previous instance, is there any example of proving, say, some category correspond to "the category of sets", has product, without transporting an existing instance of HasFiniteProduct from another category?

[Kim Morrison]

In some sense at least what you are asking for already exists:

import Mathlib

open CategoryTheory Limits

example {G : Type} [Monoid G] : HasFiniteProducts (Action (Type) (MonCat.of G)) := by infer_instance

[Yiming Xu]

Kim Morrison said:

In some sense at least what you are asking for already exists:

import Mathlib

open CategoryTheory Limits

example {G : Type} [Monoid G] : HasFiniteProducts (Action (Type) (MonCat.of G)) := by infer_instance

This is an instance off "the type of actions on Type has products", but may I please ask how do we prove, not by something black-boxed with infer-instance, that Type has finite product? How do we express the limit (i.e. what does the explicit construction of proof term look like?)? (So I am not asking for an instance to use, but trying to figure out how these sort of things work.)

[Yiming Xu]

I traced back to
https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/CategoryTheory/Closed/Types.lean#L44-L45
"Category of types has finite products"
https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/CategoryTheory/Limits/Shapes/Types.lean#L53-L53
"Category of types has product"

but everything is "infer_instance" only. How does Lean infer why does the category of types has products according to the definition?

[Markus Himmel]

Limits in the category of types are constructed here. You can scroll up a bit to see the actual construction. It is based on docs#CategoryTheory.Functor.sections.

[Yiming Xu]

Thanks for the quick reply! Let me have a look!

[Kevin Buzzard]

You can use #synth to see the instances which inferInstance is finding.

[Yiming Xu]

Kevin Buzzard said:

You can use #synth to see the instances which inferInstance is finding.

Thanks! This seems to be very useful. But I searched "synth lean4" and cannot find any documentation of that, searched zulip history and it seems like I should write #synth infer_instance, but still not able to put it anywhere in the code to get it work. May I please ask for an example piece of code of how to use it?

[Yiming Xu]

Kim Morrison said:

In some sense at least what you are asking for already exists:

import Mathlib

open CategoryTheory Limits

example {G : Type} [Monoid G] : HasFiniteProducts (Action (Type) (MonCat.of G)) := by infer_instance

Yes, and as a special case I have:

instance : HasFiniteProducts ((Action (Type u_1) (MonCat.of (MulOpposite M)))) := by infer_instance

But

instance : CartesianClosed ((Action (Type u_1) (MonCat.of (MulOpposite M)))) := by infer_instance

Reports error, This is actually the final thing I want to prove these days. Let me try this.

[Yiming Xu]

How would I refer to an object in the category ((Action (Type u_1) (MonCat.of (MulOpposite M))))?

I should be able to state the goal as something like:

instance : Exponentiable (A : (Action (Type u_1) (MonCat.of (MulOpposite M)))) :=

I am quite messed up with type classes.

[Ruben Van de Velde]

You can write something like #synth LinearOrder Nat

[Yiming Xu]

Ruben Van de Velde said:

You can write something like #synth LinearOrder Nat

Thanks! Then maybe what I should write is:

instance : HasFiniteProducts ((Action (Type u_1) (MonCat.of (MulOpposite M)))) := by infer_instance


#synth HasFiniteProducts ((Action (Type u_1) (MonCat.of (MulOpposite M))))

[Yiming Xu]

But the window only shows:
image.png

it seems not to be readable to me (or maybe I just do not know how to read it...). How can I get something useful from that?

[Ruben Van de Velde]

Can you ctrl-click on the inst....... message?

[Yiming Xu]

It gives me this:
image.png

[Yiming Xu]

And the cursor jumps to

instance : HasFiniteProducts ((Action (Type u_1) (MonCat.of (MulOpposite M)))) := by infer_instance

[Yiming Xu]

For #synth LinearOrder Nat I tried the same i.e. to ctrl-click on it. It takes me to the instance and does not output anything.

[Kevin Buzzard]

I thought the question you were asking was "the proof of something is by infer_instance but this doesn't tell me the actual proof, I want to see the actual proof" and my response about #synth is telling you how to locate the proof which by infer_instance is using.

[Yiming Xu]

Yes, thank you! You did get my question. And my trouble is to see how to use #synth.

[Yiming Xu]

I attempted to see how to use it through simpler examples, say "#synth LinearOrder Nat". I expect it to tell me how the system infers that Nat is a linear order.

import Mathlib
#synth LinearOrder Nat

These two lines does not report any error, but I do not know how get any helpful information out of that.

If that takes long to tell or the workflow of using that could be a bit involved then also no worries! I can try to ask some Lean colleagues to see if they know.

[Kevin Buzzard]

import Mathlib

#synth LinearOrder Nat -- Nat.instLinearOrder

Now ctrl-click on Nat.instLinearOrder in the infoview (i.e. on the output of #synth) and it jumps to

instance instLinearOrder : LinearOrder ℕ where
  le := Nat.le
  le_refl := @Nat.le_refl
  le_trans := @Nat.le_trans
  le_antisymm := @Nat.le_antisymm
  le_total := @Nat.le_total
  lt := Nat.lt
  lt_iff_le_not_le := @Nat.lt_iff_le_not_le
  decidableLT := inferInstance
  decidableLE := inferInstance
  decidableEq := inferInstance

in Mathlib.Data.Nat.Defs.

[Yiming Xu]

Thanks a lot! For your example, it does the right thing on my machine.

[Yiming Xu]

I am copying this workflow to check:

import Mathlib
open CategoryTheory Limits
universe u
variable {X : Type*} {Y:Type*}
         {V : Type (u + 1)} [LargeCategory V]
         {M : MonCat.{u}}

instance : Category (Action V (MonCat.of (MulOpposite M))) := inferInstance
#synth Category (Action V (MonCat.of (MulOpposite M)))

[Yiming Xu]

The output on my machine is:

instCategoryActionOfMulOppositeαMonoid_actionExponential

and

instCategoryActionOfMulOppositeαMonoid

On web version of Lean.

[Yiming Xu]

If I ctrl-click on my machine, then it takes me to the instance I just wrote

instance : Category (Action V (MonCat.of (MulOpposite M))) := inferInstance

only.

[Ruben Van de Velde]

Oh, I didn't realize that that was the issue. Put the #synth above your instance

[Yiming Xu]

Ruben Van de Velde said:

Oh, I didn't realize that that was the issue. Put the #synth above your instance

Thanks! This solves my problem and now the click works!

[Kevin Buzzard]

Your instance makes a (unnecessary) second copy of the instance, names it, and adds it to the (typeclass inference) system. The system then finds your instance first.

[Yiming Xu]

Kevin Buzzard said:

Your instance makes a (unnecessary) second copy of the instance, names it, and adds it to the (typeclass inference) system. The system then finds your instance first.

Therefore, should I omit it? In the case that such an instance is needed, Lean will then figure out the instance itself, right?

Say, if I would like to prove

instance : CartesianClosed ((Action (Type u_1) (MonCat.of (MulOpposite M)))) := sorry

Then I do not have to write the instances that the type ((Action (Type u_1) (MonCat.of (MulOpposite M))) is a category, has products etc explicitly, and Lean automatically do it using infer_instance. I will just need to provide instances when Lean reports error and tell me that it cannot infer some instance.

Thanks for correcting me if I am wrong here!

[Ruben Van de Velde]

Yeah, if you can prove an instance with inferInstance, it's redundant (but it can help lean find the instance faster - though you should not worry about it unless your code is noticeably slow)

[Yiming Xu]

Ruben Van de Velde said:

Yeah, if you can prove an instance with inferInstance, it's redundant (but it can help lean find the instance faster - though you should not worry about it unless your code is noticeably slow)

I see. Thanks for the clarification!