# Zulip Chat Archive

## Stream: general

### Topic: Fibres of a function between fintypes

#### Oleksandr Manzyuk (Apr 08 2022 at 15:17):

I'd like to formalise lax (unbiased) monoidal categories. One way to do that is to assume that a category comes equipped with $I$-ary tensor products for any finite linearly ordered set $I$, so that for any $I$-indexed family of objects $(X_i)_{i\in I}$ we have a tensor product $\otimes^{i \in I}X_i$. Furthermore, the tensor products of different arities are connected by coherence morphisms. A nice concise way to describe them is by saying that for any monotone (or arbitrary in the case of symmetric monoidal categories) map $\phi : I \to J$ of finite linearly ordered sets we have a natural transformation $\lambda^\phi_{(X_i)_{i\in I}} : \otimes^{i\in I}X_i \to \otimes^{j\in J}\otimes^{i\in\phi^{-1}(\{j\})}X_i$ subject to certain equations.

I've started to formalise these things as follows:

```
class lax_unbiased_monoidal_category (C : Type u) [category.{v} C] :=
(tensor_obj : Π {I : Type*} [fintype I] [linear_order I] (X : I → C), C)
(tensor_hom : Π {I : Type*} [fintype I] [linear_order I] {X Y : I → C} (f : Π (i : I), X i ⟶ Y i),
tensor_obj X ⟶ tensor_obj Y)
(tensor_id : ∀ {I : Type*} [fintype I] [linear_order I] (X : I → C),
tensor_hom (λ i, 𝟙 (X i)) = 𝟙 (tensor_obj X))
(tensor_comp : ∀ {I : Type*} [fintype I] [linear_order I] {X Y Z : I → C}
(f : Π (i : I), X i ⟶ Y i) (g : Π (i : I), Y i ⟶ Z i),
tensor_hom (λ i, f i ≫ g i) = tensor_hom f ≫ tensor_hom g)
(partitioner : Π {I J : Type*} [fintype I] [linear_order I] [fintype J] [linear_order J]
(φ : I → J) [monotone φ] (X : I → C),
tensor_obj X ⟶ tensor_obj (λ j, tensor_obj (λ (i : {i // φ i = j}), X i)))
(partitioner_naturality : Π {I J : Type*} [fintype I] [linear_order I] [fintype J] [linear_order J]
(φ : I → J) [hφ : monotone φ] {X Y : I → C} (f : Π (i : I), X i ⟶ Y i),
tensor_hom f ≫ @partitioner _ _ _ _ _ _ φ hφ Y
= @partitioner _ _ _ _ _ _ φ hφ X ≫ tensor_hom (λ j, tensor_hom (λ (i : {i // φ i = j}), f i)))
```

Notice that I wrote `{i // φ i = j}`

but what I'd really like to write is `φ ⁻¹' {j}`

. The latter is a subset of `I`

but sets have a coersion to subtypes. The problem I'm running into is that Lean fails to infer an instance for `fintype ↥(φ ⁻¹' {j})`

, and I'm struggling to define such an instance (or other missing instances that would imply that instance). I was hoping there would be a quick way to do that using `fintype`

/ `finset`

API, but I don't seem to be able to find the right combination of theorems. I guess I could define some notation for `{i // φ i = j}`

and develop a bit of theory for it, but I'm curious if there is a better way and would be grateful for any pointers.

#### Reid Barton (Apr 08 2022 at 15:40):

As an aside, you probably don't really want

```
(tensor_obj : Π {I : Type*} [fintype I] [linear_order I] (X : I → C), C)
```

as this means you have an extra universe parameter in `lax_unbiased_monoidal_category`

, describing in what universe you want to take these finite types `I`

.

#### Junyan Xu (Apr 08 2022 at 16:28):

We have docs#subtype.fintype but you need `open_locale classical`

to have Lean fill in the `decidable_pred`

automatically.

#### Oleksandr Manzyuk (Apr 08 2022 at 17:07):

Junyan Xu said:

We have docs#subtype.fintype but you need

`open_locale classical`

to have Lean fill in the`decidable_pred`

automatically.

Thank you! I've overlooked it somehow. (It's a tiny bit annoying that we need `classical`

because `J`

is linearly ordered, which implies decidable equality, and hence the predicate `λ i, φ i = j`

is decidable?)

#### Oleksandr Manzyuk (Apr 08 2022 at 17:09):

Reid Barton said:

As an aside, you probably don't really want

`(tensor_obj : Π {I : Type*} [fintype I] [linear_order I] (X : I → C), C)`

as this means you have an extra universe parameter in

`lax_unbiased_monoidal_category`

, describing in what universe you want to take these finite types`I`

.

Thanks. I'm new to Lean and don't have much experience with these kinds of issues. What would be the right way to address it? Introduce a third universe parameter `w`

and explicitly annotate all finite sets as terms of `Type w`

?

#### Junyan Xu (Apr 08 2022 at 17:28):

Oleksandr Manzyuk said:

Junyan Xu said:

We have docs#subtype.fintype but you need

`open_locale classical`

to have Lean fill in the`decidable_pred`

automatically.Thank you! I've overlooked it somehow. (It's a tiny bit annoying that we need

`classical`

because`J`

is linearly ordered, which implies decidable equality, and hence the predicate`λ i, φ i = j`

is decidable?)

I think it's because `φ`

may not be computable? I'd guess if you replace `φ`

by an explicit function defined without the `noncomputable`

prefix, then Lean might happily come up with the `decidable_pred`

instance.

#### Yaël Dillies (Apr 08 2022 at 17:29):

This is simply because `linear_order I`

is before the colon.

#### Yaël Dillies (Apr 08 2022 at 17:30):

What does this do?

```
(partitioner_naturality {I J : Type*} [fintype I] [linear_order I] [fintype J] [linear_order J]
(φ : I → J) [hφ : monotone φ] {X Y : I → C} (f : Π (i : I), X i ⟶ Y i) :
tensor_hom f ≫ @partitioner _ _ _ _ _ _ φ hφ Y
= @partitioner _ _ _ _ _ _ φ hφ X ≫ tensor_hom (λ j, tensor_hom (λ (i : {i // φ i = j}), f i)))
```

#### Yaël Dillies (Apr 08 2022 at 17:30):

If that doesn't work, try `by exactI`

.

#### Oleksandr Manzyuk (Apr 08 2022 at 19:57):

Yaël Dillies said:

This is simply because

`linear_order I`

is before the colon.

Sorry, I don't understand. Could you elaborate this?

#### Oleksandr Manzyuk (Apr 08 2022 at 20:04):

Yaël Dillies said:

What does this do?

`(partitioner_naturality {I J : Type*} [fintype I] [linear_order I] [fintype J] [linear_order J] (φ : I → J) [hφ : monotone φ] {X Y : I → C} (f : Π (i : I), X i ⟶ Y i) : tensor_hom f ≫ @partitioner _ _ _ _ _ _ φ hφ Y = @partitioner _ _ _ _ _ _ φ hφ X ≫ tensor_hom (λ j, tensor_hom (λ (i : {i // φ i = j}), f i)))`

This is a type class field that expresses one of the axioms, naturality of the coherence morphism. For some reason, if I write `partitioner φ Y`

and `partitioner φ X`

, Lean complains that it cannot synthesise instance of `monotone φ`

, which I don't understand and which I worked around as above. (If you have an idea what's going on, I'd be happy to hear it.)

#### Yaël Dillies (Apr 08 2022 at 20:06):

Note that I didn't just copy and paste your snippet. I moved the colon (`:`

) around.

#### Oleksandr Manzyuk (Apr 08 2022 at 20:07):

Doh. That was really hard to spot! :)

#### Yaël Dillies (Apr 08 2022 at 20:08):

Your error is that when you do `Π [foo], bar`

, `bar`

doesn't have access to `foo`

as an instance because Lean updates the instance cache when going through the colon (I believe that's not fully accurate, but explains the behavior well enough). So usually `[foo] : bar`

will fix it.

#### Yaël Dillies (Apr 08 2022 at 20:09):

Also note that docs#monotone is **not** a class, so you can't use it as `[monotone f]`

.

#### Oleksandr Manzyuk (Apr 08 2022 at 20:11):

Yaël Dillies said:

Also note that docs#monotone is

nota class, so you can't use it as`[monotone f]`

.

Facepalm. I was sure it was and didn't even bother to check.

#### Oleksandr Manzyuk (Apr 08 2022 at 20:12):

It would be nice if Lean could produce a more helpful error message in this case.

#### Yaël Dillies (Apr 08 2022 at 20:14):

I believe it does. Lean might have been confused by the other errors.

#### Oleksandr Manzyuk (Apr 09 2022 at 08:25):

I must be lacking experience working with sets in Lean because what I'm trying to do seems mathematically trivial but somehow I'm struggling to express it concisely in Lean.

Suppose that $\phi : I \to J$ and $\psi : J \to K$ are two functions of sets. Then for any $k \in K$, the function $\phi$ induces a map $\phi_k : (\psi \circ \phi)^{-1}\{k\} \to \psi^{-1}\{k\}$ and the preimage of $j \in \psi^{-1}\{k\}$ under this map is $\phi^{-1}\{j\}$.

My attempt:

```
section
parameters (I J K : Type w) (φ : I → J) (ψ : J → K) (k : K)
```

How do I define the induced map between preimages? `(ψ ∘ φ) ⁻¹' {k}`

and `ψ ⁻¹' {k}`

are sets, terms of types `set I`

and `set J`

respectively, and we cannot define a function between sets, we need to first coerce them to types:

```
def preimage_map (i : ↥((ψ ∘ φ) ⁻¹' {k})) : ↥(ψ ⁻¹' {k}) := ⟨φ i.val, i.property⟩
```

So `preimage_map`

is now a function `↥(ψ ∘ φ ⁻¹' {k}) → ↥(ψ ⁻¹' {k})`

. If

```
parameter (j : ↥(ψ ⁻¹' {k}))
```

then I'm willing to say `preimage_map ⁻¹' {j} = φ ⁻¹' {j}`

, but that's not correct because these are terms of different types:

```
#check preimage_map ⁻¹' {j} -- set ↥(ψ ∘ φ ⁻¹' {k})
#check φ ⁻¹' {j} -- set I
```

Hmm, ok. `(ψ ∘ φ) ⁻¹' {k}`

is a term of type `set I`

, so `↥((ψ ∘ φ) ⁻¹' {k})`

should have an inclusion into `I`

, right? And perhaps we can take the image of that set under the inclusion to get a term of the right type. Well, `(ψ ∘ φ) ⁻¹' {k}`

is a subset of `@set.univ I`

by means of `(@set.subset_univ I ((ψ ∘ φ) ⁻¹' {k}))`

, so `set.inclusion (@set.subset_univ I ((ψ ∘ φ) ⁻¹' {k}))`

is a function of type `↥(ψ ∘ φ ⁻¹' {k}) → ↥set.univ`

. Still not quite there yet because `↥set.univ`

is not the same thing as `I`

, but there is a function from the former to the latter, namely `subtype.val`

. This finally makes the proposition

```
example : (subtype.val ∘ set.inclusion (@set.subset_univ I _)) '' (preimage_map ⁻¹' {j}) = φ ⁻¹' {j} := sorry
```

well-typed and I can prove it.

This is quite a mouthful and I'm not sure yet how to fit it into the following bigger story. Namely, I want to write the coherence condition in a lax monoidal category, which says that the following compositions are equal:

$\otimes^{i\in I}X_i\xrightarrow{\lambda^\phi_{(X_i)_{i\in I}}}\otimes^{j\in J}\otimes^{i\in \phi^{-1}j}X_i\xrightarrow{\lambda^\psi_{(\otimes^{j\in \phi^{-1}j}X_i)_{j\in J}}}\otimes^{k\in K}\otimes^{j\in \psi^{-1}j}\otimes^{i\in \phi^{-1}j}X_i$

and

$\otimes^{i\in I}X_i\xrightarrow{\lambda^{\psi\circ\phi}_{(X_i)_{i\in I}}}\otimes^{k\in K}\otimes^{i\in (\psi\circ\phi)^{-1}k}X_i\xrightarrow{\otimes^{k\in K}\lambda^{\phi_k}_{(X_j)_{j\in \psi^{-1}k}}}\otimes^{k\in K}\otimes^{j\in \psi^{-1}k}\otimes^{i\in \phi_k^{-1}j}X_i$,

where $\phi_k : (\psi\circ\phi)^{-1}k \to \psi^{-1}k$ is the induced map, and in mathematics we implicitly replace $\phi_k^{-1}j$ with $\phi^{-1}j$ to make the targets of the two morphisms match. I'm not sure how to translate this to Lean because the translation of the theorem $\phi_k^{-1}j = \phi^{-1}j$ has extra fuff, so I'm not quite sure how to ensure that two compositions have the matching types before I can add a field to the definition of the class expressing the fact that the two compositions are equal.

I need to think more about this. Perhaps this whole approach is not a good way to formalise lax monoidal categories.

#### Kevin Buzzard (Apr 09 2022 at 09:38):

Instead of trying to make the target types equal, just carry around the isomorphism?

#### Kevin Buzzard (Apr 09 2022 at 09:39):

Independent of this, I think generally people use variables not parameters (parameters are essentially unused in mathlib)

#### Oleksandr Manzyuk (Apr 09 2022 at 10:21):

I used parameters just for the sake of example -- they make types more concise (e.g., `preimage_map`

doesn't have to carry `I`

, `J`

, `K`

etc.), which makes thisngs easier to explore.

#### Oleksandr Manzyuk (Apr 09 2022 at 10:29):

Kevin Buzzard said:

Instead of trying to make the target types equal, just carry around the isomorphism?

Hmm. But they *are* equal, we can prove that, it's that I don't quite understand yet how to incorporate that proof into the type signature of the coherence axiom. I guess I need to use `eq.subst`

(`▸`

) to make the types equal, but I don't see yet how because of the extra stuff (`subtype.val ∘ set.inclusion (@set.subset_univ I _)`

).

#### Scott Morrison (Apr 09 2022 at 10:35):

btw, I don't like calling these things lax monoidal categories. In my mind a lax monoidal category is one in which the associators aren't necessarily invertible: https://ncatlab.org/nlab/show/lax+monoidal+category

#### Scott Morrison (Apr 09 2022 at 10:35):

you should just be saying unbiased monoidal category

#### Scott Morrison (Apr 09 2022 at 10:36):

and I'm with Kevin: don't talk about equalities of types, ever, even if they are the coercions of equal sets to types.

#### Scott Morrison (Apr 09 2022 at 10:36):

instead use the `equiv`

.

#### Scott Morrison (Apr 09 2022 at 10:37):

anything you think you are saving by using an equality will just come back to torment you in the form of unexpected ` eq.rec`

s later.

#### Oleksandr Manzyuk (Apr 09 2022 at 10:37):

Scott Morrison said:

you should just be saying unbiased monoidal category

Leinster calls them lax monoidal categories. (Well, actually, what I'm trying to define here Leinster would call oplax monoidal categories, and I think so would Day and Street.)

#### Scott Morrison (Apr 09 2022 at 10:41):

So he disagrees with nlab? weird, okay.

#### Oleksandr Manzyuk (Apr 09 2022 at 10:41):

Would it be easier perhaps to carry around sets and have "bounded" tensor products similarly to `bUnion`

?

#### Scott Morrison (Apr 09 2022 at 10:42):

but maybe I'm not understanding what you're doing, because in what I imagined you are doing there isn't room for a difference between lax and oplax :-)

#### Oleksandr Manzyuk (Apr 09 2022 at 10:43):

Well, you can have a coherence morphism that inserts parentheses or one that removes them? It's just the direction of the arrow.

#### Reid Barton (Apr 09 2022 at 10:43):

The $\lambda$ not being an isomorphism is what makes it (op)lax and not an ordinary monoidal category

#### Oleksandr Manzyuk (Apr 09 2022 at 10:44):

Right.

#### Reid Barton (Apr 09 2022 at 10:44):

Oh wait--Scott said the *associators* aren't necessarily invertible

#### Scott Morrison (Apr 09 2022 at 10:45):

I'd only ever heard people talking about lax or oplax *biased* monoidal categories

#### Oleksandr Manzyuk (Apr 09 2022 at 10:45):

That's a different notion of "lax monoidal category", one that I wasn't actually familiar with.

#### Scott Morrison (Apr 09 2022 at 10:45):

in which case lax or oplax means you can push parentheses either to the left or the right

#### Oleksandr Manzyuk (Apr 09 2022 at 10:46):

OK, https://arxiv.org/pdf/math/0305049.pdf, page 67

Also, https://www.math.ksu.edu/~lub/cmcMonad.pdf, page 34

#### Scott Morrison (Apr 09 2022 at 10:46):

but in the unbiased world I can understand now how you could choose to either coarsen or refine the partition

#### Reid Barton (Apr 09 2022 at 10:47):

I would have called all the versions with associators "skew"

#### Reid Barton (Apr 09 2022 at 10:50):

but then, I didn't realize there were all these variants involving the unitors

#### Scott Morrison (Apr 09 2022 at 10:53):

What are they all for? I'm skeptical. :-) I would love to see "strong" unbiased monoidal categories in mathlib, however, even just as a demo it can be done. :-)

#### Oleksandr Manzyuk (Apr 09 2022 at 10:53):

Unbiased lax monoidal categories is warmup before multicategories (and the former provide a source of examples for the latter).

Last updated: Aug 03 2023 at 10:10 UTC