Fibres of a function between fintypes

Stream: general

[Oleksandr Manzyuk]

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]

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]

We have docs#subtype.fintype but you need open_locale classical to have Lean fill in the decidable_pred automatically.

[Oleksandr Manzyuk]

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]

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]

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]

This is simply because linear_order I is before the colon.

[Yaël Dillies]

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]

If that doesn't work, try by exactI.

[Oleksandr Manzyuk]

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]

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]

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

[Oleksandr Manzyuk]

Doh. That was really hard to spot! :)

[Yaël Dillies]

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]

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

[Oleksandr Manzyuk]

Yaël Dillies said:

Also note that docs#monotone is not a 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]

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

[Yaël Dillies]

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

[Oleksandr Manzyuk]

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]

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

[Kevin Buzzard]

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

[Oleksandr Manzyuk]

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]

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]

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]

you should just be saying unbiased monoidal category

[Scott Morrison]

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]

instead use the equiv.

[Scott Morrison]

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

[Oleksandr Manzyuk]

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]

So he disagrees with nlab? weird, okay.

[Oleksandr Manzyuk]

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

[Scott Morrison]

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]

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]

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

[Oleksandr Manzyuk]

Right.

[Reid Barton]

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

[Scott Morrison]

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

[Oleksandr Manzyuk]

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

[Scott Morrison]

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

[Oleksandr Manzyuk]

OK, https://arxiv.org/pdf/math/0305049.pdf, page 67
Also, https://www.math.ksu.edu/~lub/cmcMonad.pdf, page 34

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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]

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