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 -ary tensor products for any finite linearly ordered set , so that for any -indexed family of objects we have a tensor product . 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 of finite linearly ordered sets we have a natural transformation 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 thedecidable_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 typesI
.
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 thedecidable_pred
automatically.Thank you! I've overlooked it somehow. (It's a tiny bit annoying that we need
classical
becauseJ
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 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 (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 and are two functions of sets. Then for any , the function induces a map and the preimage of under this map is .
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:
and
,
where is the induced map, and in mathematics we implicitly replace with 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 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 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: Dec 20 2023 at 11:08 UTC