n composable morphisms

Stream: mathlib4

[Herman Rohrbach]

How do I recurse over Fin (n + 1)? I'm trying to define the composition of m morphisms in the simplex category.

def multi_comp {n : ℕ} (f : Fin (n + 1) → Arrow SimplexCategory) (hf : ∀ i : Fin n, (f n).right = (f (n + 1)).left) :=
  comp n
where
  comp : Fin (n + 1) → Arrow SimplexCategory
    | 0 => f 0
    | i + 1 => f succ ≫ comp i

This gives me an error

invalid patterns, `i` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  {
    val :=
      .(match ↑i + 1 % (n + 1), n + 1 with
        | 0, x => 0
        | x@h:(Nat.succ n), y => Nat.modCore x y),
    isLt := (_ : (↑i + 1 % (n + 1)) % (n + 1) < n + 1) }

[Johan Commelin]

Welcome @Herman Rohrbach!

This definition is a bit tricky to write down, because you need to convince the kernel of the equality of source/domain of some objects at the right moment. You have the assumption hf, but you'll have to inject it into the actual term at some point.

[Johan Commelin]

Using a Fin (n + 1)-indexed collection of arrows might not be the optimal way of formalizing this concept.

[Johan Commelin]

Mathlib has a bunch of stuff on paths and walks in graph theory. You might be able to use some of those techniques here as well.

[Herman Rohrbach]

Thank you for the welcome @Johan Commelin !

I'm glad to know I'm not the only one who thinks this is a little tricky. I'll take a look at some of the graph theory in mathlib to see if I can find a better way of doing this.

[Joël Riou]

I would see two ways to do this (in any category C):

import Mathlib.AlgebraicTopology.SimplexCategory

universe v u

namespace CategoryTheory

variable (C : Type u) [Category.{v} C]

-- this is a little bit cheating, assuming the `n` composable arrows already
-- form a functor `Fin (n + 1) ⥤ C`, see also `AlgebraicTopology.Nerve`
abbrev ComposableArrows (n : ℕ) := Fin (n + 1) ⥤ C

variable {C n}

def composableArrows.composition (F : ComposableArrows C n) : F.obj 0 ⟶ F.obj (Fin.last _) :=
  F.map (homOfLE (Fin.zero_le _))

-- alternative approach using inductive types (similar to `Combinatorics.Quiver.Path`)

/-- `ComposableArrowsFromTo n X Y` is the type of `n` composable arrows from `X` to `Y`. -/
inductive ComposableArrowsFromTo : ℕ → C → C → Type (max u v)
  | id (X : C) : ComposableArrowsFromTo 0 X X
  | comp {X Y Z : C} {n : ℕ} (α : ComposableArrowsFromTo n X Y) (f : Y ⟶ Z) :
      ComposableArrowsFromTo (n + 1) X Z

def ComposableArrowsFromTo.composition {X Y : C} {n : ℕ} : ComposableArrowsFromTo n X Y → (X ⟶ Y)
  | id _ => 𝟙 _
  | comp α f => α.composition ≫ f

variable (C)

structure ComposableArrows' (n : ℕ) where
  source : C
  target : C
  arrows : ComposableArrowsFromTo n source target

variable {C}

def ComposableArrows'.composition {n : ℕ} (α : ComposableArrows' C n) : α.source ⟶ α.target :=
  α.arrows.composition

end CategoryTheory

I think it would be interesting to define equivalences between these two types ComposableArrows C n and ComposableArrows' C n, the more interesting part being promoting n composable arrows into a functor from Fin (n+1).

When I implemented Verdier's construction of spectral sequences, I had to consider categories of n composable arrows for n = 1, 2, 3, 4, 5, 6, 7. It would be great if I had a nice constructor for this rather than my very crude current definition:

structure Arrow₇ :=
  {X₀ X₁ X₂ X₃ X₄ X₅ X₆ X₇ : C}
  f : X₀ ⟶ X₁
  g : X₁ ⟶ X₂
  h : X₂ ⟶ X₃
  i : X₃ ⟶ X₄
  j : X₄ ⟶ X₅
  k : X₅ ⟶ X₆
  l : X₆ ⟶ X₇

[Herman Rohrbach]

@Joël Riou Thank you for your extensive thoughts on the matter, I like your suggestions! The first one is nice because it makes it easy to check e.g. if every morphism has a certain MorphismProperty, but the second one might be easier to construct.

I noticed that in SimplexCategory, almost everything has been implemented except the fact that it is generated by face and degeneracy maps, so I thought I'd give that a go as a little project to get to know category theory and algebraic topology in mathlib a little bit.

[Johan Commelin]

Yeah, that project would be really good. It's been on my radar for > 4 years, but I never got around to actually doing it.

[Johan Commelin]

I think it could be phrased as some sort of induction principle.

[Kevin Buzzard]

It's not just that it's generated by these maps, we also know the precise relations, right?

[Herman Rohrbach]

@Johan Commelin That was my feeling as well. There are already lemmas telling us we can split off face and degeneracy maps as long as the input map is not injective or surjective, and we should use those until we're 'left' with a bijection which is the identity by another lemma.

@Kevin Buzzard Yes, and these have already been proved in mathlib, so it's just this final step that is missing.

[Kevin Buzzard]

Do we have the statement that the known easy relations generate all the relations in a precise sense? i.e. "there are no more relations"?

[Herman Rohrbach]

@Kevin Buzzard I think we do, in the sense that any category whose objects are the usual finite ordinals [n] and whose morphisms are generated by the face and degeneracy maps subject to the simplicial relations must be the simplex category, see e.g. MacLane's Categories for the working mathematician, Section VII.5.

[Kevin Buzzard]

Yes, sorry for the misunderstanding -- I know it's a theorem, I'm asking if we have it in mathlib!

[Joël Riou]

The theorem is not in mathlib. We have notions of path category of a quiver ("free category" generated by some arrows), and also that of quotient category by a congruence generated by some relations among morphisms, so that it is certainly possible to state the presentation theorem for SimplexCategory.

About ComposableArrows in general, I was able to get reasonably good constructors for functors Fin (n + 1) ⥤ C, see https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/ComposableArrows.lean and especially https://github.com/leanprover-community/mathlib4/blob/1d6d79c4498537deabead84846eb4eba11456ba4/Mathlib/CategoryTheory/ComposableArrows.lean#L272

[Adam Topaz]

Johan Commelin said:

I think it could be phrased as some sort of induction principle.

This sounds similar to how we handled naturality in the snake lemma in LTE.

[Herman Rohrbach]

Using @Joël Riou 's idea for an inductive type, I have now managed to show that monomorphisms in SimplexCategory admit a decomposition into face maps.

import Mathlib.AlgebraicTopology.SimplicialSet
import Mathlib.CategoryTheory.MorphismProperty
import Mathlib.CategoryTheory.CommSq
import Mathlib.Data.Set.Image

open CategoryTheory

universe v u

namespace CategoryTheory

variable (C : Type u) [Category.{v} C]

inductive ComposableWithProperty (P : MorphismProperty C) (X : C) : C → Type max u v
  | nil : ComposableWithProperty P X X
  | append {Y Z : C} (_ : ComposableWithProperty P X Y) (f : Y ⟶ Z) (_ : P f) : ComposableWithProperty P X Z

namespace ComposableWithProperty

variable {P : MorphismProperty C}

def toComposable {X Y : C} {f : X ⟶ Y} (hf : P f) : ComposableWithProperty P X Y :=
  nil.append f hf

def total_comp {X Y : C} : ComposableWithProperty P X Y → (X ⟶ Y)
  | nil => 𝟙 _
  | append α f hf => α.total_comp ≫ f

def length {X Y : C} : ComposableWithProperty P X Y → ℕ
  | nil => 0
  | append α _ _ => α.length + 1

@[simp]
lemma total_comp_append {X Y Z : C} (α : ComposableWithProperty P X Y) (f : Y ⟶ Z) (hf : P f)
    : (α.append f hf).total_comp = α.total_comp ≫ f := by
  rw [total_comp]

end ComposableWithProperty

namespace SimplexCategory

open Simplicial

lemma gt_not_inj {m n : ℕ} (f : mk m ⟶ mk n)
    : m > n → ¬Function.Injective f.toOrderHom := by
  contrapose
  simp
  intro h
  have hf : Mono f := by simpa [mono_iff_injective]
  exact len_le_of_mono hf

lemma lt_not_surj {m n : ℕ} (f : mk m ⟶ mk n)
    : m < n → ¬Function.Surjective f.toOrderHom := by
  contrapose
  simp
  intro h
  have hf : Epi f := by simpa [epi_iff_surjective]
  exact len_le_of_epi hf

def DegeneracyMap : MorphismProperty SimplexCategory :=
  fun _ _ f => ∃ (n : ℕ) (i : Fin (n + 1)), Arrow.mk f = Arrow.mk (σ i)

def FaceMap : MorphismProperty SimplexCategory :=
  fun _ _ f => ∃ (n : ℕ) (i : Fin (n + 2)), Arrow.mk f = Arrow.mk (δ i)

theorem face_decomp {n m : ℕ} (f : mk n ⟶ mk (n + m)) (hf : Mono f)
    : ∃ (α : ComposableWithProperty FaceMap (mk n) (mk (n + m))),
    α.total_comp = f := by
  induction m with
  | zero =>
    have hid : f = 𝟙 (mk n) := by
      apply eq_id_of_mono f
    use ComposableWithProperty.nil
    simp [ComposableWithProperty.total_comp, hid]
  | succ m ih =>
    have hm : n < n + Nat.succ m := by simp
    have h := lt_not_surj f hm
    have h := eq_comp_δ_of_not_surjective f h
    choose i g hg using h
    have hg₂ : Mono g := by
      have _ : Mono (g ≫ (δ i)) := by
        rw [← hg]
        exact hf
      exact mono_of_mono g (δ i)
    specialize ih g hg₂
    choose α hα using ih
    have hδ : FaceMap (δ i) := by
      constructor
      use i
    use α.append (δ i) hδ
    rw [ComposableWithProperty.total_comp_append α (δ i) hδ, hα]
    exact hg.symm

end SimplexCategory

@Johan Commelin Is this the kind of inductive proof you had in mind? Obviously it shouldn't be too hard to prove something similar for epimorphisms and degeneracy maps, using a RevComposableWithProperty where the arrows are appended on the left instead of on the right of the diagram.

[Johan Commelin]

Nice work!

[Johan Commelin]

The induction principle that I had in mind was more of the form: If you want to construct/prove something for all maps in the simplex category, then you only need to do it for face/degeneracy maps and show that it behaves well with respect to some compositions.

[Herman Rohrbach]

That makes sense, it would be great to be able to construct simplicial objects by defining n-simplices, face and degeneracy maps and proving the simplicial identities (which I guess would be a consequence of the kind of thing you propose). I think the statement I formalized could be a step in that direction, I'll think about it some more.

[Johan Commelin]

Yes, and yes, and yes please (-;

[Adam Topaz]

I wonder whether all sufficiently concrete categories in mathlib ($\Delta^{op}$ in this case) should come equipped with an "induction principle" for constructing functors out of them? Also, what about an induction principle for constructing natural transformations (i.e. morphisms between simplicial objects in the simplicial case)?

[Junyan Xu]

abbrev ComposableArrows (n : ℕ) := Fin (n + 1) ⥤ C

This is a powerful idea. I'm working on Van Kampen and need to define a functor out of the fundamental groupoid by partitioning a path into small paths contained in some open set in an open cover, defining the functor on these small paths, and then composing the resulting morphisms, which is quite complicated if you think about it. Then I revisited this thread and immediately realized what I should really do is to show that any path on X induces a functor I ⥤ FundamentalGroupoid X, where I is the unit interval. You can extend this to two dimensions and show a homotopy induces a functor out of I × I (with the product order), and given a monotone sequence from Fin (n+1) to I you can compose with the induced functor and then use composableArrows.composition. To show the definition is independent of the partition you choose, normally you'd take a common refinement, which would be a mess to formalize; with this approach you can fix a finite partition and patch together functors defined on these subintervals to get a functor defined on all of I, and show independence inductively on larger and larger intervals, which will make the proof a lot simpler.

[Johan Commelin]

@Junyan Xu FYI #7999 is a PR by Joel that contains the defn of ComposableArrows.

[Junyan Xu]

Thanks! I'm not seeing the PR being particularly useful to me, but the inspiration is real.