Theorems · Definition · category theory

FreeSimplexQuiver.homRel.casesOn

∀ {motive : ⦃X Y : CategoryTheory.Paths FreeSimplexQuiver⦄ → (a a_1 : X ⟶ Y) → FreeSimplexQuiver.homRel a a_1 → Prop}
  ⦃X Y : CategoryTheory.Paths FreeSimplexQuiver⦄ {a a_1 : X ⟶ Y} (t : FreeSimplexQuiver.homRel a a_1),
  (∀ {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j),
      motive
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i))
          ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ j.succ)))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ j))
          ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc)))
        ⋯) →
    (∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc),
        motive
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc))
            ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.succ)))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j))
            ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i)))
          ⋯) →
      (∀ {n : ℕ} {i : Fin (n + 1)},
          motive
            (CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc))
              ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i)))
            (CategoryTheory.CategoryStruct.id
              ((CategoryTheory.Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk n)))
            ⋯) →
        (∀ {n : ℕ} {i : Fin (n + 1)},
            motive
              (CategoryTheory.CategoryStruct.comp
                ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.succ))
                ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i)))
              (CategoryTheory.CategoryStruct.id
                ((CategoryTheory.Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk n)))
              ⋯) →
          (∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i),
              motive
                (CategoryTheory.CategoryStruct.comp
                  ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.succ))
                  ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.castSucc)))
                (CategoryTheory.CategoryStruct.comp
                  ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j))
                  ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i)))
                ⋯) →
            (∀ {n : ℕ} {i j : Fin (n + 1)} (H : i ≤ j),
                motive
                  (CategoryTheory.CategoryStruct.comp
                    ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i.castSucc))
                    ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j)))
                  (CategoryTheory.CategoryStruct.comp
                    ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.succ))
                    ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i)))
                  ⋯) →
              motive a a_1 t

Defined in

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext