The structure of an iso

Stream: Infinity-Cosmos

[Arnoud van der Leer]

Hi, I have been trying to work with isomorphisms. On paper, a 1-simplex f is an iso if there is an "inverse" 1-simplex f^-1 and two 2-simplices that fill the two inner horns given by f and f^-1 its inverse.
As far as I can see, formalizing the statement "that fill the inner horns" boils down to about 3 equalities per 2-simplex. Now, what data do we make part of the definition, and what data will we derive? For example, I can think of 3 structures, shown below.
One of the considerations for which data will be part of the structure is (I believe) whether (f^-1)^-1 will be definitionally equal to f (this only holds for isIso''). Are there other considerations?

-- Naively, an iso structure consists of an inverse, two 2-simplices, and equalities relating the 2-simplices to the 1-simplices
structure isIso {X : SSet} (hom : X _⦋1⦌) where
  inv            : X _⦋1⦌
  hom_inv_id     : X _⦋2⦌
  inv_hom_id     : X _⦋2⦌
  hom_inv_id_hom : X.δ (2 : Fin 3) hom_inv_id = hom
  hom_inv_id_inv : X.δ (0 : Fin 3) hom_inv_id = inv
  hom_inv_id_id  : X.δ (1 : Fin 3) hom_inv_id = X.σ (0 : Fin 1) (X.δ (1 : Fin 2) hom)
  inv_hom_id_inv : X.δ (2 : Fin 3) inv_hom_id = inv
  inv_hom_id_hom : X.δ (0 : Fin 3) inv_hom_id = hom
  inv_hom_id_id  : X.δ (1 : Fin 3) inv_hom_id = X.σ (0 : Fin 1) (X.δ (0 : Fin 2) hom)

-- Since the identities have been defined in terms of hom, we need to do some work for the relation between the 2-simplices and the identities on the endpoints
def isIso_inv {X : SSet} (hom : X _⦋1⦌) (I : isIso hom)
  : isIso I.inv where
    inv := hom
    [... Some fields of I, in a different order ...]
    hom_inv_id_id := by
      apply I.inv_hom_id_id.trans
      apply congr_arg
      nth_rw 1 [← I.hom_inv_id_hom]
      nth_rw 1 [← I.hom_inv_id_inv]
      unfold SimplicialObject.δ
      show ((X.map _ ≫ X.map _) _ = (X.map _ ≫ X.map _) _)
      rw [← X.map_comp]
      rw [← X.map_comp]
      apply congr_arg (fun f ↦ X.map f _)
      decide
    inv_hom_id_id := by
      apply I.hom_inv_id_id.trans
      apply congr_arg
      nth_rw 1 [← I.inv_hom_id_hom]
      nth_rw 1 [← I.inv_hom_id_inv]
      unfold SimplicialObject.δ
      show ((X.map _ ≫ X.map _) _ = (X.map _ ≫ X.map _) _)
      rw [← X.map_comp]
      rw [← X.map_comp]
      apply congr_arg (fun f ↦ X.map f _)
      decide

-- We can also leave out the inverse
structure isIso' {X : SSet} (hom : X _⦋1⦌) where
  hom_inv_id     : X _⦋2⦌
  inv_hom_id     : X _⦋2⦌
  hom_inv_id_hom : X.δ (2 : Fin 3) hom_inv_id = hom
  hom_inv_id_id  : X.δ (1 : Fin 3) hom_inv_id = X.σ (0 : Fin 1) (X.δ (1 : Fin 2) hom)
  inv_hom_id_inv : X.δ (2 : Fin 3) inv_hom_id = X.δ (0 : Fin 3) hom_inv_id
  inv_hom_id_hom : X.δ (0 : Fin 3) inv_hom_id = hom
  inv_hom_id_id  : X.δ (1 : Fin 3) inv_hom_id = X.σ (0 : Fin 1) (X.δ (0 : Fin 2) hom)

-- Because we have more asymmetric data, we need to do more work here
def isIso'_inv {X : SSet} (hom : X _⦋1⦌) (I : isIso' hom)
  : isIso' (X.δ (0 : Fin 3) I.hom_inv_id) where
    [... Some fields of I, in a different order ...]
    hom_inv_id_id := by
      apply I.inv_hom_id_id.trans
      apply congr_arg
      nth_rw 1 [← I.hom_inv_id_hom]
      unfold SimplicialObject.δ
      show ((X.map _ ≫ X.map _) _ = (X.map _ ≫ X.map _) _)
      rw [← X.map_comp]
      rw [← X.map_comp]
      apply congr_arg (fun f ↦ X.map f _)
      decide
    inv_hom_id_inv := by
      apply I.hom_inv_id_hom.trans
      apply I.inv_hom_id_hom.symm
    inv_hom_id_hom := rfl
    inv_hom_id_id := by
      apply I.hom_inv_id_id.trans
      apply congr_arg
      nth_rw 1 [← I.inv_hom_id_hom]
      nth_rw 1 [← I.inv_hom_id_inv]
      unfold SimplicialObject.δ
      show ((X.map _ ≫ X.map _) _ = (X.map _ ≫ X.map _) _)
      rw [← X.map_comp]
      rw [← X.map_comp]
      apply congr_arg (fun f ↦ X.map f _)
      decide

-- In the other direction, we can include the endpoints in the data
structure isIso'' {X : SSet} (hom : X _⦋1⦌) where
  pt₀            : X _⦋0⦌ := X.δ (1 : Fin 2) hom
  pt₁            : X _⦋0⦌ := X.δ (0 : Fin 2) hom
  inv            : X _⦋1⦌
  hom_inv_id     : X _⦋2⦌
  inv_hom_id     : X _⦋2⦌
  hom_inv_id_hom : X.δ (2 : Fin 3) hom_inv_id = hom
  hom_inv_id_inv : X.δ (0 : Fin 3) hom_inv_id = inv
  hom_inv_id_id  : X.δ (1 : Fin 3) hom_inv_id = X.σ (0 : Fin 1) pt₀
  inv_hom_id_inv : X.δ (2 : Fin 3) inv_hom_id = inv
  inv_hom_id_hom : X.δ (0 : Fin 3) inv_hom_id = hom
  inv_hom_id_id  : X.δ (1 : Fin 3) inv_hom_id = X.σ (0 : Fin 1) pt₁

-- Now, we can make the inverse of the inverse definitionally equal to hom
def isIso''_inv {X : SSet} (hom : X _⦋1⦌) (I : isIso'' hom)
  : isIso'' I.inv where
    pt₀ := I.pt₁
    pt₁ := I.pt₀
    inv := hom
    [and then the other fields of I, in a different order]

-- We can show that the endpoints have to be the endpoints of hom and I.inv:
lemma isIso''_hom_pt₀ {X : SSet} (hom : X _⦋1⦌) (I : isIso'' hom)
  : I.pt₀ = X.δ (1 : Fin 2) hom
  := ...
lemma isIso''_inv_pt₀ {X : SSet} (hom : X _⦋1⦌) (I : isIso'' hom)
  : I.pt₀ = X.δ (0 : Fin 2) I.inv
  := ...

Ps. Also, I'm new here, and do not know what lemmas have already been formalized, and how, so there is probably a lot to improve in my code. Feel free to comment on that here, or to wait until I file a PR (one or the other might be better, depending on the nature of the comments :-) )

[Joël Riou]

Please look at docs#SSet.Edge.CompStruct

[Arnoud van der Leer]

How do we define the start and end points of hom? We need that to define inv as an Edge from end to start.

[Arnoud van der Leer]

So do we take the isIso'' route, defining these end points as the first pieces of data, and going from there?

[Arnoud van der Leer]

With
x0 x1 : X_[0]
inv : Edge x1 x2
hom_inv_id : CompStruct hom inv (id x0)
inv_hom_id : CompStruct inv hom (id x1)

[Joël Riou]

The "hom" should also be an Edge.

[Arnoud van der Leer]

Ah, of course

[Arnoud van der Leer]

The definition becomes a bit cleaner. However, when using this, a lot of the goals start mentioning truncation:

((truncation 2).obj X).map (SimplexCategory.Truncated.δ₂ 2 ⋯ ⋯).op (yonedaEquiv (hom_inv_id ≫ g)) = f.toTruncated.edge

What is the right way to deal with this? Currently, it takes a couple of steps (in each proof) to simplify away enough of the truncation terms. Is there a nice lemma that I could use instead, that states for example that if these edges are equal, then their images after truncation are also equal, or something?

[Arnoud van der Leer]

Also, I am considering adding a constructor for isos.
In my original proposal, the fact that hom and inv are equal to faces of a 2-simplex ensures that the start (resp end) point of hom is the end (resp start) point of inv.
However, in this new structure, since hom and inv are edges, we need to show this explicitly.
Is such a constructor a good idea? Something along the lines of this?

def isIso.mk' {X : SSet} (hom : X _⦋1⦌)
  (inv            : X _⦋1⦌)
  (hom_inv_id     : X _⦋2⦌)
  (inv_hom_id     : X _⦋2⦌)
  (hom_inv_id_hom : X.δ (2 : Fin 3) hom_inv_id = hom)
  (hom_inv_id_inv : X.δ (0 : Fin 3) hom_inv_id = inv)
  (hom_inv_id_id  : X.δ (1 : Fin 3) hom_inv_id = X.σ (0 : Fin 1) (X.δ (1 : Fin 2) hom))
  (inv_hom_id_inv : X.δ (2 : Fin 3) inv_hom_id = inv)
  (inv_hom_id_hom : X.δ (0 : Fin 3) inv_hom_id = hom)
  (inv_hom_id_id  : X.δ (1 : Fin 3) inv_hom_id = X.σ (0 : Fin 1) (X.δ (0 : Fin 2) hom))
  : isIso {
    edge := hom
    src_eq := rfl
    tgt_eq := rfl
  }

[Joël Riou]

Using docs#SSet.Edge.CompStruct.mk should avoid the appearance of truncations. I am not convinced there is a need for another constructor for isos because in many cases the src_eq/tgt_eq are obtained by rfl anyway.
In terms of design, it seems more appropriate to me to define first anIso structure (with hom and inv fields) rather than IsIso.

[Arnoud van der Leer]

Ah, thanks.
Then how would you state https://emilyriehl.github.io/infinity-cosmos/blueprint/sec-homotopy-category.html#prop:coherent-iso?

[Arnoud van der Leer]

Joël Riou said:

...in many cases the src_eq/tgt_eq are obtained by rfl anyway.

And are you sure that in many cases, we have

X.δ (0 : Fin 2) hom = X.δ (1 : Fin 2) inv

definitionally? Because in the first nontrivial case that I worked on, inv := {edge := yonedaEquiv (coherentIso.inv ≫ g), ...}, which means we do not have this definitional equality.

[Joël Riou]

For rfl, I was thinking of explicit examples in nerves of "decidable" categories.
I do not think it would be a problem phrasing the relation with cohrentIso using Iso rather than IsIso (the name is a little bit problematic as Is... is expected to be a Prop). The real difficulties would appear for the proof!

[Arnoud van der Leer]

How would you phrase it?
Because "There is an equivalence between iso structures on f iff its Yoneda lift Δ⦋1⦌ ⟶ X factors through the embedding into coherentIso" is a stronger statement than "The isos in X are equivalent to the maps coherentIso ⟶ X".

[Joël Riou]

I did not suggest changing the statement.

[Emily Riehl]

I would state that result as a logical equivalence between propositions. There's a way to understand this result as a weak equivalence of types but here weak equivalence means in the sense of the Joyal model structure and not in the sense of mathlibs equivalence of types (which is an isomorphism) in the category of types.

So the statement is that a given 1-simplex f in X admits the IsIso structure you define if and only if there is a map from coherentIso to X that restricts to f on one of the edges.

[Arnoud van der Leer]

Emily Riehl said:

I would state that result as a logical equivalence between propositions.
...
So the statement is that a given 1-simplex f in X admits the IsIso structure you define if and only if there is a map from coherentIso to X that restricts to f on one of the edges.

I agree. Although these are not propositions (hProp), since IsIso can have multiple nonequivalent members, right?

[Joël Riou]

The LHS could be something like ∃ (e : Edge.Iso x₀ x₁), e.hom = f where Edge.Iso is the structure considered above. Equivalently, the morphism induced by f in the homotopy category is an isomorphism (in the sense of CategoryTheory.IsIso).
I do not know the proof (the hard part must be to construct a morphism from coherentIso from an isomorphism), but I would assume that from e : Edge.Iso x₀ x₁ as above, it should be possible to ensure that two obvious 1-simplices of coherentIso are mapped to e.hom and e.inv respectively (and hopefully, there are 2-simplices that are mapped to the given homInvId and invHomId).

[Arnoud van der Leer]

So I'm trying to understand

def F {I : isIso f} : coherentIso ⟶ X

by constructing it explicitly. Everything up and including the 2-simplices is fairly trivial: Given

  hom            : Edge x₀ x₁
  inv            : Edge x₁ x₀
  hom_inv_id     : Edge.CompStruct hom inv (Edge.id x₀)
  inv_hom_id     : Edge.CompStruct inv hom (Edge.id x₁)

First of all, F must send coherentIso.σ i x to X.σ i (F x).
Also, it sends i : coherentIso _⦋0⦌ to xᵢ : X _⦋0⦌, 0 -[f]-> 1 : coherentIso _⦋1⦌ to hom : X _⦋1⦌ and 0 -[f]-> 1 -[f⁻¹]-> 0 : coherentIso _⦋2⦌ to hom_inv_id : X _⦋2⦌ (and similarly for 1 -[f⁻¹]-> 0 and 1 -[f⁻¹]-> 0 -[f]-> 1)

However, that is where the troubles begin. Where do we send the two nondegenerate elements of coherentIso _⦋3⦌? The only tool that we have, is inner horn filling. As far I understand, this goes as follows:
For g = 0 -> 1 -> 0 -> 1 : coherentIso _⦋3⦌, we have an inner horn Λ¹(3) ⟶ X given by δ 3: hom_inv_id, δ 2: X.σ 1 f and δ 0: inv_hom_id. This horn has a filling H. We could try to set F g to be H. Now, this satisfies most of the requirements:

• X.δ 0 (F g) = X.δ 0 H = inv_hom_id = F(coherentIso.δ 0 g)
• X.δ 2 (F g) = X.δ 2 H = X.σ 1 f = F(coherentIso.δ 2 g)
• X.δ 3 (F g) = X.δ 3 H = hom_inv_id = F(coherentIso.δ 3 g)

However, how do we know that X.δ 1 H = F(coherentIso.δ 1 g)? There is probably some higher homotopy between them, but since a quasicategory does not have unique horn fillings, this brings us nothing. Am I missing something?

[Joël Riou]

This is a nontrivial result. I would suggest doing the other implication first. For this direction, I have had a quick look at the proof in 1.1.16 of [RV22]. @Emily Riehl may give more clarifications, but the rough idea is to reduce to the case X is a Kan complex, and then obtain the map from coherentIso by using the right lifting property with respect to the inclusion Δ[1] ⟶ coherentIso which is a trivial cofibration (for the Quillen model category structure). If we know everything about this model category structure, it follows from the fact that it is a monomorphism between two contractible simplicial sets (these are nerves of categories that are equivalent to the terminal object of Cat). With less technology, we need to show that Δ[1] ⟶ coherentIso is an anodyne extension. This is exercice 1.1.v in [RV22]. The better way to show this is probably to use the notion of pairing (introduced by Sean Moss) https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.html because #28462 will show that this is an anodyne extension.
(This exact proof does not give a control about whether suitable simplices in coherentIso are sent to inv, hom_inv_id or inv_hom_id. I feel it would be interesting to examine what exactly is possible: this may involve introducing subcomplexes of coherentIso generated by one (or maybe two) nondegenerate 2-simplices.)

[Robin Carlier]

Doesn’t the reduction to Kan complexes also require Joyal’s "special outer horn" lemma (1.1.14)?

[Arnoud van der Leer]

Ah, right, that looks very nontrivial indeed.

[Arnoud van der Leer]

I have done the other implication. I'll clean it up a bit more, and if I still find this fun to do at that point, I'll submit a PR :-)

[Arnoud van der Leer]

Ideally, this would not only be a logical equivalence, but also an equivalence of types, right?

[Joël Riou]

Arnoud van der Leer said:

Ideally, this would not only be a logical equivalence, but also an equivalence of types, right?

No, I do not think so.

[Joël Riou]

Robin Carlier said:

Doesn’t the reduction to Kan complexes also require Joyal’s "special outer horn" lemma (1.1.14)?

Yes, you are right!

[Arnoud van der Leer]

Joël Riou said:

No, I do not think so.

Why is that? The types here are not propositions, so a logical equivalence, while nice to have, would not express everything there is to say about the relation between these types. It feels like the "wrong" kind of equivalence to shoot for here.
I mean, there also is a logical equivalence between the natural numbers and the one-element set, but that does not tell us a lot.

[Arnoud van der Leer]

So do you mean

• that it is unnecessary to prove that it is an equivalence of types?
• that it would be impractical to prove?
• these types are actually not equivalent?

[Joël Riou]

I think it is two optimistic to expect these types are equivalent.

[Arnoud van der Leer]

Hm... If they are not, I'd expect that to be because coherentIso -> has more elements.
If we 2-truncate coherentIso and X, we have an equivalence, right?

[Joël Riou]

This discussion is pointless unless there is a clear answer to the last part of my message #Infinity-Cosmos > The structure of an iso @ 💬.

[Emily Riehl]

I'm late to this conversation, as usual, but let me add a few comments.

The first thing to clarify is that @Joël Riou is right that this result is not expressible as an equivalence of types. I think of the data used to define the type isIso as indexed by the 2-skeleton of the coherent isomorphism. Concretely it is given by two 0-simplices, two opposing 1-simplices, and the 2-simplices with boundary discussed above.

The problem is that sk_2 coherentIso is an incoherent model of the homotopy coherent isomorphism, in that this object is not weakly equivalent (in the Joyal model structure) to coherentIso.

[Emily Riehl]

There are various finite models of the homotopy coherent isomorphism that you can read about in any homotopy type theory book. Several of them are subcomplexes of coherentIso. Here's how you define them. Start by taking the n-skeleton for n at least 3. Then throw away one of the two top dimensional non-degenerate simplices (either one). The resulting objects are models of the homotopy coherent isomorphism. In Elements of Infinity-Category Theory we call them $E^-_n$ and $E^+_n$ where the n is the dimension and the - or + indicates the starting vertex of the simplex that is kept. In the bottom case $E^-_3$ and $E^+_3$ , which are isomorphic (though not as subcomplexes of coherentIso) define the free-living adjoint equivalence by adding a single 3-simplex expressing a coherence between the 2-cells of sk_2coherentIso.

[Emily Riehl]

Now let's turn to the issue of proving that you can extend along Δ[1] -> coherentIso assuming the 1-simplex is an isomorphism. Here's how I think about the proof.

[Emily Riehl]

Step 1. Decompose this extension as a pushout of 0-horn extensions, one in each dimension. In the terminology introduced above. You're starting with the subcomplex $E^-_1$, which contains just one of the two 1-simplices of coherent iso. The first 0-horn inclusion adds $E^-_2$ attached as the filler of the 0th horn and $E^-_2$ attached as the filler of the missing face. The next 0-horn inclusion then adds $E^-_3$ and $E^+_2$ and so on.

[Emily Riehl]

Some remarks on step 1:

• The point of this construction is that by the time you're attaching the $E^+_n$ s you already have their full boundary. So you can't attach these by filling a horn at that dimension. You have to move up a dimension.
• This sort of construction feels relatively straightforward to me on paper but I worry that it secretly uses Reedy category theory or something to argue that the final colimit is the full coherentIso. Essentially I'm building a simplicial set by attaching only the non-degenerate simplices modulo their boundary. The degenerate simplices come along for free.
• This can also be done with right horn inclusions instead of left horn inclusions.

[Arnoud van der Leer]

Indeed. I worked this out on paper recently (a nice exercise), and there it seems clear that in each dimension, this crystallizes at some moment to the right set,
But how one would even formulate all this, let alone prove it, I am not sure.

[Emily Riehl]

Step 2: as @Robin Carlier noted above is special outer horn filling. This is established via a bunch of technical lemmas in appendix D to our book (and elsewhere). Here is one way to establish it.

Proposition: If a quasi-category admits extensions along the map $E^-_1 \to E^-_3$ then it admits extensions along left (and right) horns whose initial (respectively final) edge is an isomorphism.

What this extension condition means is that if an edge in a quasi-category is an isomorphism then this can be extended to the half adjoint equivalence.

[Arnoud van der Leer]

Okay, if it is not an equivalencu of types. Would it maybe be a retraction onto isIso? (so a one-sided inverse)

[Emily Riehl]

The construction in the proof is explained in Proposition D.4.8 in a slightly more general setting (of marked simplicial sets). But to understand the geometry, you can ignore the markings. The basic idea is to take your left horn and decompose it as a pushout join of $E^-_0 \to E^-_1$ with a simplex boundary inclusion. You can then extend from the domain of this map to a more complicated simplicial set (see diagram (D.4.9)) using a sequence of inner horn extensions plus the extension along $E^-_1 \to E^-_3$. You can find the codomain of your outer horn inside here. So this extension solves the problem. If you're trying to extend along the left horn inclusion Horn n 0 -> Δ[n] you find it inside a partially degenerated n+2 simplex.

[Emily Riehl]

Step 3. The final step is to show that all quasi-categories satisfy the condition of the proposition I just mentioned. This is rather delicate: see Proposition D.5.1. It's reminiscent of an argument from bicategory theory: namely that any equivalence can be made into an adjoint equivalence at the cost of replacing one of the 2-cells by something else. Essentially this construction is just a translation of that into simplicial sets.

[Emily Riehl]

So as @Joël Riou noted this is not an easy result!

[Emily Riehl]

Perhaps there are simpler proofs but this is the one that I know (that doesn't rely on knowing about the characterization of the maximal sub Kan complex of a quasi-category).

[Emily Riehl]

Arnoud van der Leer said:

Okay, if it is not an equivalencu of types. Would it maybe be a retraction onto isIso? (so a one-sided inverse)

Unfortunately, no. You can see that there is no where for the non-degenerate 3-simplices of coherentIso to go in sk_2coherentIso. In general, a simplicial set basically never retracts onto its skeleton (unless is it n-skeletal).

[Joël Riou]

If I understand properly your remark about "replacing one of the 2-cells by something else", is it correct to say that if we have an IsIso structure (with hom, inv, and two 2-simplices hom_inv_id and inv_hom_id satisfying the expected properties), then it is possible to find a map from coherentIso which send suitable simplices to hom, inv and hom_inv_id (but maybe not inv_hom_id?).