Refactoring AttachCells

Stream: maths

[Robert Maxton]

So, I am finally mostly done with my project to provide converters in both directions between docs#Topology.RelCWComplex and docs#TopCat.RelativeCWComplex. However, I am finding that the current design of docs#HomotopicalAlgebra.AttachCells makes it very difficult to make subcomplexes.

The issue is primarily one of internal dependencies: there are three types/objects (ι and the points of the two cofans) internal to AttachCells that are then used in the types of other components of the structure (π, g₁, g₂), which are then heavily used in the external API to RelativeCellComplex. Thus, a naive implementation of, say, a truncation of a CW complex to a finite subcomplex has to engage heavily with conditionals on the entire AttachCells structure; the internal dependencies then make it difficult to 'transpose' these statements into individual conditionals about each projection without heavy use of casts; and the direct coupling with external API expose the resulting tangled casts to the rest of the library.

This certainly can be worked around -- I'm currently in the process of refactoring my subcomplex to use more computable conditionals that can be matched on -- but I still think this is a pretty big footgun that I'd prefer to fix. As such, I propose that we replace both cofans and isColimits with HasCoproduct typeclass parameters, and move ι out of the AttachCells substructure into the main RelativeCellComplex structure. The remaining data π, g₁, g₂ is now non-dependent, in that no projection appears in the type of another projection.

Is this a reasonable change? @Joël Riou , you're probably the one who would be most affected by this; what are your thoughts?

[Joël Riou]

Replacing general cofans by the chosen coproduct does not seem reasonable to me. The field ι may be made a parameter, but I am not sure I undertstand how this would help the study of subcomplexes.

[Robert Maxton]

Whyever not? It's mathematically equivalent and cuts the necessary data required to make the structure in half, so it's quite appealing even aside from the issue of dependencies. And without that, you end up with a fundamentally internally dependent structure that cannot be easily transported across RelativeCellComplexes, especially ones where the relavent type parameters don't line up 'on the nose'.

[Robert Maxton]

ι needs to be a parameter because otherwise, π is of type (𝓙.attachCells ...).ι → .... Suppose that we wish to study a finite truncation of a complex; we may naively attempt to do so by reusing the existing AttachCells, but replacing all structures above a certain n by a trivial structure with ι empty.

[Robert Maxton]

Having done so, we run into a problem: π k is now of type, say, (if k < j then (𝓙.attachCells ...) else trivialCell).ι → .... "Transposing" this definition, writing a simp lemma that says if k < j then π k = ... else π k = ..., now requires embedding multiple casts into the lemmas.

[Robert Maxton]

Certainly, we can just not do that; as noted, I'm currently rewriting this structure to split the linear order into a sum of an Iio and an Ici, so that I can computably match on the structure and write defeq simp lemmas. But that requires a nontrivial amount of extra infrastructure, some of which would have to be repeated every time I wanted to make a subcomplex of this type. I'd prefer to simply make the original structure non-dependent, with as much as possible referencing static externally-defined types like the HasCoproduct API and any remaining dependencies handled at the level of the full RelativeCellComplex structure.

[Joël Riou]

I understand that there are dependent theory issues. Similar issues may appear if for example one wants to extend a functor from Fin (n + 1) to a functor from Fin (n + 2) by "adding one more arrow". In that case, one may relate both chunks of the glued functor by providing isomorphisms.
An approach in order to relate different AttachCells would be, maybe not to define a category, but to express that if f : X ⟶ Y and g : X' ⟶ Y' are both equiped with two AttachCells structure, we may have morphisms X ⟶ X' and Y ⟶ Y' which makes the square commute, as well as an (injective?) map between the indices ι which makes a certain cube commute. Developing an API around this may be useful to solve some of your issues.

[Robert Maxton]

I mean, for now, that is in fact the approach I've taken; I have a bunch of API around equivalent AttachCells on the same morphism, plus a custom recursor that allows me to work with the AttachCells structure with the HasCoproduct API + an equivalence between motives given an equivalence between AttachCells, and now I'm adding yet more API to build AttachCells on prop-eq morphisms

[Robert Maxton]

But that makes a few extra thousand lines of code, and while some of that scales quite a lot of it doesn't; every time we want to build such a derived structure we're going to end up writing yet more API around the cast.

[Robert Maxton]

Why do you say it's unreasonable to replace general cofans with an abstractly defined coproduct?

[Joël Riou]

Part of the problem is that the HasCoproduct would also be a dependent one.

[Robert Maxton]

HasCoproduct is a Prop, so having it be dependent is a much lesser burden than having dependent data in Type.

Assuming you want to preserve maximal generality (i.e. not just using HasColimitsOfShape (Discrete ι) C), we can write something like...

import Mathlib.CategoryTheory.MorphismProperty.Limits

universe w' w t t' v u

open CategoryTheory Limits

namespace HomotopicalAlgebra

variable {C : Type u} [Category.{v} C]
  {α : Type t} {A B : α → C} (g : ∀ a, A a ⟶ B a)
  {X₁ X₂ : C} (f : X₁ ⟶ X₂) (ι : Type w)

structure AttachCells where
  π : ι → α
  hasCoproduct₁ : HasCoproduct (fun i ↦ A (π i)) := by infer_instance
  hasCoproduct₂ : HasCoproduct (fun i ↦ B (π i)) := by infer_instance
  g₁ : ∐ (A <| π ·) ⟶ X₁
  g₂ : ∐ (B <| π ·) ⟶ X₂
  isPushout : IsPushout g₁ (Limits.Sigma.map (g <| π ·)) f g₂

attribute [instance] AttachCells.hasCoproduct₁ AttachCells.hasCoproduct₂

Now, while there are still internal dependencies, they're much less visible from outside the structure; the HasCoproduct instances are technically dependent, but as Prop-valued typeclasses they don't complicate further usage of the structure; invoking, say, g₂ just references the statically-defined sigmaObj type and it doesn't really matter that the instance proving that that usage is valid happens to be dependent.

[Robert Maxton]

We still have the π in ∐ (A <| π ·), which I missed when I was sketching this out in my head earlier, but I think the existing eqToHom machinery can mostly handle cases like that when they appear as morphisms in a category.

[Joël Riou]

In any case, the cleaner approach is what I have suggested above.

[Robert Maxton]

That is absolutely not the cleaner approach, though? As noted, that's a thousand additional lines of code.

[Robert Maxton]

I would be curious to know where you think using the HasCoproduct API will meaningfully complicate your use of this structure?

[Joël Riou]

Using eqToHom would only solve one type of issue. What I suggested would also allow to study CW-complexes whose cells are "subsets" of cells of a large CW-complex, etc.
It would be possible to use HasCoproduct instead, but I am not at all convinced that it would solve any dependent type issue. Doing this and putting ι outside would allow to give a reasonable mathematical meaning to the notion of equality between two AttachCells structures, but I do not think it is a good idea to follow this way, as it seems much more interesting to relate AttachCells structures for two different maps through commutative squares as I have suggested above.

[Robert Maxton]

Mm. I suppose my response then, is: why should we be attempting to relate AttachCells structures at all? As far as I can tell, they're just convenient packaging that have turned out to be less than convenient; I have much less issue with writing useful API for RelativeCellComplex itself, which is the level I expect to be actually working with these structures.

In fact, my issues precisely derive from the fact that I can relatively easily come up with categorical representations of all the other data of a sub-RelativeCellComplex, before being bogged down in DTT hell when engaging with AttachCells; or, equivalently, that there is quite a lot of existing API with which to work with TransfiniteCompositionOfShape (which, ultimately, is just a bundled functor + isomorphism + some instances), but everything for AttachCells would have to be bespoke. The suggestion I outlined above makes it much easier to, say, turn a natural isomorphism between TransfiniteCompositionOfShapes into one between RelativeCellComplexes; it would also make it easier to make precisely that sort of subtyped-subcomplex you're describing, as with ι outside I can directly put constraints on a natural transformation between the underlying functors that require the cell attachment index types to be subtypes, rather than having to subtype the entire AttachCell structure or add an equivalent interface layer.