condensed abelian groups

Stream: condensed mathematics

[Kevin Buzzard]

@Calle Sönne and @Kenny Lau and @Bhavik Mehta have been working on defining condensed sets. A natural goal here would be to prove that the category of condensed abelian groups is an abelian category with all the extra stuff too (e.g. arbitrary products). This is Theorem 1.10 of http://www.math.uni-bonn.de/people/scholze/Condensed.pdf .

[Kevin Buzzard]

Reid has suggested that we initially ignore the cardinal bounds; we can come back to them later (they are in some sense not the point of the challenge)

[Reid Barton]

More precisely, taking Type 1-sized sheaves on tiny (:= Type 0-sized) profinite sets

[Kevin Buzzard]

This will be a nice test of the abelian category machinery, so this has great value independent of the application to the challenge.

[Bhavik Mehta]

@Adam Topaz's effort towards ind-objects seem relevant as well, if we need to show that the category Pro-Fintype is the same as Profinite

[Adam Topaz]

My plan was to define profinite sets as Pro(FinType) :rofl:

[Adam Topaz]

But I got stuck with the details, tbh.

[Bhavik Mehta]

I think regardless of the definition, the equivalence between the two categories ought to be there

[Adam Topaz]

Yes absolutely.

[Bhavik Mehta]

Do you have a branch where you're working on this out of interest?

[Adam Topaz]

I haven't started anything seriously, just playing around.

[Adam Topaz]

For example, I tried making some crazy inductive-quotient style definition, which works out fine, except for universe problems.

[Adam Topaz]

And I tried the "direct" way where you define hom sets as

$$\operatorname{lim}_j \operatorname{colim}_i \operatorname{Hom}(F(i),G(j))$$

but even defining the identity morphisms seems to be a major pain...

[Adam Topaz]

I'm still not sure what definition would be best here...

[Bhavik Mehta]

import category_theory.limits.functor_category
import category_theory.full_subcategory
import category_theory.limits.types

namespace category_theory
namespace limits

universes v u
variables {C : Type u} [small_category C]

structure as_inductive (P : Cᵒᵖ ⥤ Type u) :=
(D : Type u)
[𝒟 : small_category D]
[hD : is_filtered D]
(α : D ⥤ C)
(i : P ≅ colimit (α ⋙ (yoneda : C ⥤ Cᵒᵖ ⥤ Type u)))

structure is_inductive (P : Cᵒᵖ ⥤ Type u) : Prop :=
(mk' : nonempty (as_inductive P))

@[derive category]
def ind := {P : Cᵒᵖ ⥤ Type u // is_inductive P}

end limits
end category_theory

this works but I don't know if making C a small category is too restrictive

[Adam Topaz]

Right, so this is the presentation of filtered colimits of representables in presheves. That's the right category.

[Bhavik Mehta]

Yeah, but Fintype isn't a small category, so with this definition we don't get Ind(Fintype) \iso Type

[Adam Topaz]

There's a nice skeleton for FinType, already in mathlib :)

[Bhavik Mehta]

Sure but I don't see any maths reason why Ind is only defined for small categories

[Bhavik Mehta]

Ah this looks better:

import category_theory.limits.functor_category
import category_theory.full_subcategory
import category_theory.limits.types
import category_theory.Fintype

namespace category_theory
namespace limits

universes v u
variables {C : Type u} [category.{v} C]

structure as_inductive (P : Cᵒᵖ ⥤ Type v) :=
(D : Type*)
[𝒟 : small_category D]
[hD : is_filtered D]
(α : D ⥤ C)
(c : cocone (α ⋙ yoneda))
(hc : is_colimit c)
(i : P ≅ c.X)

structure is_inductive (P : Cᵒᵖ ⥤ Type v) : Prop :=
(mk' : nonempty (as_inductive P))

variable (C)

@[derive category]
def ind := {P : Cᵒᵖ ⥤ Type v // is_inductive P}

def thing : ind Fintype.{u} ≌ Type u :=
sorry

end limits
end category_theory

[Bhavik Mehta]

some stuff building on that here: https://github.com/leanprover-community/mathlib/tree/ind-object

[Calle Sönne]

Kevin Buzzard said:

This will be a nice test of the abelian category machinery, so this has great value independent of the application to the challenge.

I didnt know this existed!

[Calle Sönne]

Looks great

[Calle Sönne]

So where have people been working on this? I have just been (slowly) trying to build upon @Kevin Buzzard s definition of Profinite sets on the branch Profinite2. So far I proved they have limits, so now I guess that the pretopology can be defined.

[Kevin Buzzard]

Abelian categories are now in mathlib!

[Kevin Buzzard]

docs#category_theory.abelian

[Kevin Buzzard]

The first goal is to show that the category of sheaves of abelian groups on Profinite is an abelian category.

[Adam Topaz]

It may be worthwhile to prove that this is true for abelian sheaves on any site.

[Adam Topaz]

But this requires sheafification, which I don't think we have yet in mathlib for a general grothendieck topology

[Bhavik Mehta]

Adam Topaz said:

It may be worthwhile to prove that this is true for abelian sheaves on any site.

@Kevin Buzzard tells me this isn't true in general

[Bhavik Mehta]

(unless I'm misunderstanding something which is more than likely)

[Adam Topaz]

Condensed abelian groups satisfy stronger axioms than just an abelian category that do not hold true in for general abelian sheaves. Maybe this is what he means?

[Bhavik Mehta]

Probably, assume that I understood something wrong rather than that he said something wrong though :)

[Adam Topaz]

https://stacks.math.columbia.edu/tag/03CN

[Bhavik Mehta]

was just about to ask for that, thanks

[Bhavik Mehta]

Looking through that it seems like it splits up quite nicely: https://stacks.math.columbia.edu/tag/03A3 is just a statement on abelian categories, it requires that the category of abelian presheaves is abelian: https://stacks.math.columbia.edu/tag/03A6, and what's left then is that the abelian sheaves are a reflective subcategory where the reflector is left exact

[Bhavik Mehta]

To get here of course we need to define abelian presheaves and sheaves, which I talked a bit about here: https://github.com/leanprover-community/mathlib/pull/5255#issuecomment-740065209

[Adam Topaz]

We also need the sheafification functor, but I'm sure you already have plans for that :)

[Bhavik Mehta]

I do :)

[Bhavik Mehta]

Coming soon to a mathlib near you

[Bhavik Mehta]

Is Profinite as in mathlib a small category? The results in stacks are stated only for small categories, as is the result I put in the link above

[Reid Barton]

It might be necessary to ulift the morphisms of Profinite to make it small in the next universe

[Bhavik Mehta]

Do you think just doing that will solve the universe issues?

[Reid Barton]

It is the correct way to solve them in this context

[Bhavik Mehta]

By the way do you have any suggestions for making the category of ind-objects? I had a go here: https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/condensed.20abelian.20groups/near/219247857 but it doesn't seem like the best way to me

[Reid Barton]

If I recall correctly, it's not that easy to prove that objects of this form are closed under filtered colimits

[Reid Barton]

which is the one property you'd hope would be obvious from this definition

[Reid Barton]

also the definition seems to indicate we lack a version of a colimit cocone indexed on the vertex

[Reid Barton]

I have a construction of the closure under a certain class of colimits somewhere, but I'm not sure it is very useful either

[Reid Barton]

oh but that was mostly to avoid enlarging the universe, which isn't an issue here

[Reid Barton]

Typically I'd assume that C is small and has finite colimits and take the full subcategory on the guys that send those to limits

[Reid Barton]

If C doesn't have finite colimits then I guess you can take flat functors?

[Reid Barton]

let's see what LPAC does

[Reid Barton]

it proves that being a filtered colimit of representables is equivalent to the corresponding colimit-preserving functor preserving finite limits

[Bhavik Mehta]

Do you know how difficult that proof is to formalise?

[Reid Barton]

it doesn't look especially hard

[Reid Barton]

Lemma 2.24

[Adam Topaz]

What's LPAC?

[Reid Barton]

Locally Presentable and Accessible Categories

[Bhavik Mehta]

Oh yeah that looks very manageable

[Reid Barton]

at least if you replace "directed" in the statement by "filtered"

[Kevin Buzzard]

Bhavik Mehta said:

Probably, assume that I understood something wrong rather than that he said something wrong though :)

Apologies for the confusion -- this was a conversation we had on the discord and I'm pretty sure it was me who got it wrong -- I'd misremembered something. Arbitrary products are exact for condensed abelian groups (a product of epis is epi), and this is not true for sheaves of abelian groups on a general site, but all the axioms for an abelian category hold for sheaves of abelian groups on a general site (Bhavik I think I told you that arbitrary products might not exist in general).

[Bhavik Mehta]

Yup, as you mentioned Scholze says something along these lines:
"This makes Cond(Ab) exceptionally well-behaved, even more well-behaved than the category of abelian sheaves on a usual topos: Usually, infinite products fail to be exact."

[Reid Barton]

Your thing is an interesting test case, I feel like it will probably be pretty hard to prove directly

[Bhavik Mehta]

I'm not sure if it'll make that easier but I do suspect the definition would be nicer as saying the corresponding colimit-preserving functor preserving finite limits

[Adam Topaz]

@Calle Sönne https://github.com/leanprover-community/mathlib/blob/1f1ba587f272d203a40801c6b21af453f7de6ee3/src/topology/subset_properties.lean#L1305

[Bhavik Mehta]

Getting back to the ind-objects stuff, I've got a workable definition of flat functor on an arbitrary category (ie, not necessarily small and with no assumptions on limits/colimits), together with a proof that it's the same notion as preserving finite limits if they exist in the category, and almost got that the category of flat functors (ie ind-objects) is closed under filtered colimits (if the category is small), so I'm not far off from formally showing they're the ind-completion

[Bhavik Mehta]

The real tests here though are showing that ind Fintype = Type, and ind Fintype^op = Profinite^op

[Peter Scholze]

@Bhavik Mehta Those would be great to have, yes.

[Bhavik Mehta]

If anyone's interested in joining, I'm having a go at showing ind Fintype = Type in Kevin's discord!

[Bhavik Mehta]

Does anyone know if this result will explicitly be helpful? Specifically Calle has shown the topology version without an explicit equivalence of categories, is that good enough for the liquid project or is the actual category theory helpful too

[Adam Topaz]

I think the equivalence Pro (FinType) \equiv Profinite is actually useful because there are a lot of arguments that work with some functor on Profinite where you reduce to the finite case using this equivalence.

[Kevin Buzzard]

So after several months away doing other things I've now got some time to work on some research-level Lean (which is a very welcome state of affairs). Adam suggested that I look at the proof that condensed abelian groups are an abelian category. I've been watching the chat but not reading closely.

I see we have src/condensed/ab.lean :D Some of the imports have sorrys though. The first one is in for_mathlib/Profinite/disjoint_union.lean and it's

lemma is_preconnected.preimage [topological_space α] [topological_space β] {s : set β}
  (hs : is_preconnected s) {f : α → β} (hf : continuous_on f (f ⁻¹' s)) (hsf : s ⊆ set.range f) :
  is_preconnected (f ⁻¹' s) := sorry

which seems wrong to me -- a counterexample would be beta=s={*} and alpha is an arbitrary (non-preconnected) topological space. The sorried lemma is used in the proof of sigma.is_connected_iff. Have I made a mistake here or is something fishy going on?

The next sorried lemma is finite_product_condition_iff_empty_condition_product_condition in src/condensed/is_proetale_sheaf.lean and it's basically the statement that something works for finite products iff it works for empty products and binary products. I could imagine ploughing through this but it being looong. Is there some category theory miracle which would make this less painful?

My impression from the comments in condensed.basic is that Bhavik is in the middle of removing the sorries there. Comments like "I'm 90% sure this is true as stated" by a sorried lemma are a bit scary though!

Should we sort out these sorries before going for the proof that condensed abelian groups are an abelian category?

[Kevin Buzzard]

pre: preimage of connected is connected; it seems like the only times these dubious sorried lemmas are used in the project is to (correctly) classify connected subsets of sigma types and binary sums, so maybe I'll just have a go at proving these results (sigma.is_connected_iff and sum.is_connected_iff)

[Adam Topaz]

@Kevin Buzzard Bhavik's sorry'd lemma is essentially proven

[Adam Topaz]

See is_proetale_sheaf_tfae in the other file

[Kevin Buzzard]

The application of "pre-image of connected is connected" is in a situation where the map is injective and open (and the connected subset is in the image of the map), and in that case I think it's OK.

[Johan Commelin]

I agree that it would be good to take care of these sorries :thumbs_up:

[Johan Commelin]

It will be reassuring to know that we got the category right.

[Adam Topaz]

structure condensed_type_condition : Prop :=
(empty : nonempty X.preserves_terminal)
(bin_prod : nonempty X.preserves_binary_products)
(pullbacks : ∀ {S S' : Profinite.{u}} (f : S' ⟶ S) [epi f],
  nonempty (is_limit (natural_fork X f)))

-- (BM): I'm 90% sure this is true as stated, the forward direction is about halfway done.
lemma sheaf_condition_iff :
  presieve.is_sheaf proetale_topology X ↔ condensed_type_condition X :=
sorry

is essentially the equialence between 1 and 4 in

theorem is_proetale_sheaf_tfae [limits.has_terminal C] [limits.has_binary_products C]
  [limits.has_equalizers C] :
  [ presheaf.is_sheaf proetale_topology Q,
    Q.is_proetale_sheaf,
    Q.is_proetale_sheaf_pullback,
    Q.empty_condition' ∧ Q.product_condition' ∧ Q.equalizer_condition'
  ].tfae :=

[Adam Topaz]

Well, modulo a technicality about the equalizer condition vs. the pullback condition that's easy to see

[Adam Topaz]

Oh, and note that the tfae statement works for presheaves taking values in any category, not just Type* whichh is the context of sheaf_condition_iff

[Adam Topaz]

Once #10169 is merged ( :wink: ) I'll be able to add another characterization of sheaves similar to what appears in the following file
https://github.com/leanprover-community/lean-liquid/blob/sheafification_stuff/src/for_mathlib/sheafification/multifork_sheaf_condition.lean

[Adam Topaz]

Kevin Buzzard said:

The application of "pre-image of connected is connected" is in a situation where the map is injective and open (and the connected subset is in the image of the map), and in that case I think it's OK.

I don't really know where the is_preconnected.preimage came from. It's only needed in the case where the map is an open embedding.

[Kevin Buzzard]

yeah I'm fixing it up right now

[Kevin Buzzard]

lol the unused argument linter tells me that I never assumed f was continuous ;-)

[Kevin Buzzard]

I love it when Lean does that

[Kevin Buzzard]

lemma is_preconnected.preimage [topological_space α] [topological_space β] {s : set β}
  (hs : is_preconnected s) {f : α → β}   (hfinj : function.injective f) (hfopen : is_open_map f)
  (hsf : s ⊆ set.range f) : is_preconnected (f ⁻¹' s) := λ u v hu hv hsuv hsu hsv,
begin
  specialize hs (f '' u) (f '' v) (hfopen u hu) (hfopen v hv) _ _ _,
  { have := set.image_subset f hsuv,
    rwa [set.image_preimage_eq' hsf, set.image_union] at this },
  { obtain ⟨x, hx1, hx2⟩ := hsu,
    exact ⟨f x, hx1, x, hx2, rfl⟩ },
  { obtain ⟨y, hy1, hy2⟩ := hsv,
    exact ⟨f y, hy1, y, hy2, rfl⟩ },
  { obtain ⟨b, hbs, hbu, hbv⟩ := hs,
    obtain ⟨a, rfl⟩ := hsf hbs,
    rw function.injective.mem_set_image hfinj at hbu hbv,
    exact ⟨a, hbs, hbu, hbv⟩ }
end

[Kevin Buzzard]

So I just pushed straight to master -- is that OK? I'll keep going -- this is a nice warm-up, I can probably get for_mathlib/Profinite/disjoint_union.lean sorry-free this evening (everyone else has gone out :D )

[Adam Topaz]

Master is fine!

[Adam Topaz]

What sorry's arre left?

[Kevin Buzzard]

Just a couple of topological trivialities which Yael skipped

[Kevin Buzzard]

Basically if you're connected and in a disjoint union (either a pair or a sigma type) then you're in one of them

[Adam Topaz]

@Kevin Buzzard I pushed a complete mathlib bump to the LTE branch bump-2021-11-05. I didn't want to bump master directly, in case you're still working on this, so we should merge this to master when convenient.

[Kevin Buzzard]

feel free to merge to master; I can't imagine that you'll break any of my local work

[Adam Topaz]

Okay, done. Make sure to refresh your oleans!

[Kevin Buzzard]

nothing broke :D

[Kevin Buzzard]

OK that's me done for the day -- for_mathlib.Profinite.disjoint_union is now sorry-free. @Yaël Dillies you seem to have written a bunch of that file -- I added in some extra assumptions to make "pre-image of connected is connected" true and also added a few more lemmas (see the longish proofs in lines <= 90), maybe you want to golf them? I did my best.

[Yaël Dillies]

How come I have written a bunch of any file?

[Kevin Buzzard]

oh you were git blamed for that file

[Yaël Dillies]

The only thing I could do was isolate 3 or 4 lemmas and fill in easy sorries.

[Kevin Buzzard]

You made a commit "prove sigma.compact_space" from two weeks ago. You left some sorries, I just filled them in.

[Yaël Dillies]

Oh okay, yeah that's what I did.

[Kevin Buzzard]

I wondered whether you wanted to be a perfectionist about the proofs

[Yaël Dillies]

How can you wonder about that? :stuck_out_tongue_closed_eyes:

[Adam Topaz]

Once you enter the Profinite namespace in that file, it become much more category-heavy (and that's my fault)

[Kevin Buzzard]

If I filled in a sorry in a file Patrick wrote I suspect he'd want to have a look at it and tidy up the mess I'd made

[Kevin Buzzard]

he has some principles ;-) (i.e. he's very good at writing short topology proofs)

[Kevin Buzzard]

Adam I think it will be very good for me to engage with some of the category theory stuff again. I've done it twice in my life before and both times poor Scott has had to endure a huge amount of whingeing from me about how it is so hard to do category theory in Lean, followed slowly by me getting the hang of it a bit more, so I'm looking forward to learning more about it.

[Kevin Buzzard]

I'm less sure that Scott will be, although maybe there are other people I can whinge to nowadays :D

[Adam Topaz]

When you can comment out some field in some structure in some abstract nonsense category-theoretic structure because you know that tidy can solve it, and it works after 37 seconds, it makes all the pain completely worth it.

[Kevin Buzzard]

I have some dumb questions related to "a functor preserves finite products iff it preserves binary products and terminal objects", another sorry on the way to the definition of condensed abelian groups.

1) Where do things like "if C is a category, X and Y are objects, and f : X -> Y is an isomorphism, then f^{op} : Y^{op} -> X^{op} is an isomorphism" and "if F : C -> D is a functor, and F : X -> Y is an isomorphism, then F.map f is an isomorphism" live? I guess these will be definitions rather than theorems.

2) Do we have a nonconstructive singleton? i.e. a Prop-valued "I have precisely one term"?

[Adam Topaz]

1) docs#category_theory.iso.op

[Adam Topaz]

And docs#category_theory.functor.map_iso

[Adam Topaz]

I think docs#unique for 2?

[Adam Topaz]

Oh that's not Prop valued.

[Adam Topaz]

For 1, the links above work if you are using docs#category_theory.iso but if you want to use docs#category_theory.is_iso then there should be some similarly named lemmas that accomplish the same thing

[Kevin Buzzard]

ooh thanks a lot for these tips and links!

[Kevin Buzzard]

@Adam Topaz you've made things like category_theory.functor.finite_product_condition (in is_proetale_sheaf.lean) be Prop-valued (asserting a function is bijective rather than asserting the data of an inverse) so I guess I'll stick with this convention

[Adam Topaz]

We should have a lemma saying that a morphism in Type* has is_iso if it's bijective.

[Kevin Buzzard]

you mean "it should be there" or "I should make it right now"?

[Adam Topaz]

The reason I used plain properties of functions as opposed to category theoretic notions is because I later apply these to the values of some yoneda functors, and it's much easier to apply the conditions in this case

[Kevin Buzzard]

I'm still not up to speed :-)

[Adam Topaz]

I think it should be there...

[Adam Topaz]

Somewhere :grimacing:

[Adam Topaz]

docs#category_theory.is_iso_iff_bijective

[Kevin Buzzard]

Thanks so much

[Adam Topaz]

That file has all of the lemmas relating categorical notions in Type* to the usual properties of functions

[Kevin Buzzard]

I'll try and get somewhere with the remaining sorry. It's not going to be fun but I think I'm thinking about it in the right way. On paper it's easy but in lean it's delicate. Take "the empty profinite space" for example. In my mind there is one such object. But lean knows about the empty type, or a sigma type over the empty type, or the product of the empty type and another type etc etc -- these are all types and who knows, they're probably not provably equal in Lean anyway, however of course they're isomorphic as profinite spaces and now one has to do some diagram chasing which is elementary and not hard to write down on paper -- the insight is realising that these empty types aren't equal and so you have to be careful drawing the diagrams :-)

[Adam Topaz]

I think for that finite product sorry, the first step is to prove an analogue of docs#fintype.induction_empty_option for docs#Fintype

[Yaël Dillies]

Kevin Buzzard said:

OK that's me done for the day -- for_mathlib.Profinite.disjoint_union is now sorry-free. Yaël Dillies you seem to have written a bunch of that file -- I added in some extra assumptions to make "pre-image of connected is connected" true and also added a few more lemmas (see the longish proofs in lines <= 90), maybe you want to golf them? I did my best.

Oh wow! The final proofs aren't ending up much longer than where I left them.

[Kevin Buzzard]

OK so I started on finite_product_condition_iff_empty_condition_product_condition (morally "if P is a presheaf on Profinite then P (X1 disjoint union X2 disjoint .. disjoint Xn) = P X1 x P X2 x ... x P Xn iff this is true for n=0 and n=2"). The issue is that the n=0 case is stated with empty and the n=2 case with binary products, whereas the general n case uses things like sigma types.

Today I've managed to prove that the general n case implies the n=0 case. It doesn't sound like much but actually I learnt something about the kind of tools which were required to do this kind of proof in category theory. Thanks for the pointers yesterday Adam, they made things easier.

[Kevin Buzzard]

OK so the next step is the following. We have P a contravariant functor from profinite types to types, and we have two profinite types S and T. Let X denote the map from fin 2 to Profinite with X 0 = S and X 1 = T. Notation : a is always a : fin 2.

We are given that the obvious map from P (Σ a, X a) (think of the sigma type as just a disjoint union) to Π a, P (X a) (coming from the inclusions of the factors X a into the sigma type) is a bijection. We need to prove that the obvious map from P (S ⊕ T) to P S × P T is a bijection.

Easy and useful: one can construct S ⊕ T ≃ Σ a, X a commuting with the obvious maps from S = X 0 and T = X 1 into both sides.

My idea: write down the map P (S ⊕ T) -> P (Σ a, X a) -> Π a, P (X a) -> P S × P T, prove it's a bijection because it's the composite of three bijections (the first because P of an iso is an iso, the second by hypothesis, and the third because I guess you can write down an inverse map?), and now argue that it's the same bijection as the obvious map because it agrees with the obvious map on the two factors.

[Kevin Buzzard]

This feels like it's going to be very long, and we're still doing the easy part! I'm prepared to give it a go though.

[Reid Barton]

I think it would be a bit better to arrange the diagram as a commuting square, but it basically sounds good

[Reid Barton]

P (Σ a, X a) -> P (S ⊕ T)

[Kevin Buzzard]

right, I'm thinking of it as a square but writing it in lines

[Reid Barton]

i.e. never talk about the inverse of anything (sorry I forgot to reverse the map!)

[Kevin Buzzard]

I have e : S ⊕ T ≃ Σ a, X a and I'm happy to use the iso generated by e

[Kevin Buzzard]

oh it's just dawned on me what you mean

[Reid Barton]

but it will make your verification that the map is the right one harder, since you will need to use the fact that the two directions of e are equal

[Reid Barton]

it's easier to use the fact that f and fg iso => g iso or whatever

[Kevin Buzzard]

gotcha -- prove the square commutes and then deduce the iso on the bottom line from the other three. I'm still not completely on top of the idea that this buys me something.

[Kevin Buzzard]

Earlier on I was writing down bijections between pempty and Σ a : pempty, X a but here it was easy because to prove that a map between two types is a bijection it suffices to show that both types are singletons (for products) or empty (for sums)

[Kevin Buzzard]

doing this exercise really pushed home to me the fact that "the" empty type, represented in two different ways in type theory, gives me two objects in a category of types which I cannot consider as equal.

[Kevin Buzzard]

Category theory is just set theory with extensionality removed, thus making it harder to do anything.

[Reid Barton]

yeah but it's okay because everything is canonical :upside_down:

[Reid Barton]

Kevin Buzzard said:

I'm still not completely on top of the idea that this buys me something.

It doesn't buy you much. I just claim it will be easier to check that the square commutes (maybe the proof will even be refl?) than that your three-fold composite will be the right map. Consider that the square would still commute, and just as obviously, even if a : fin 3 instead

[Reid Barton]

In this case your approach will just need to simplify something like P.map e >> P.map e.symm, which is easy but in general this is work that you can avoid by drawing the right diagram

[Kevin Buzzard]

Thanks for the comments! I'll go with the square.