Theorems · Theorem · category theory

AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.counitIso.inv.app X).left.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
        | CategoryTheory.WithTerminal.of x => X.left.obj x
        | CategoryTheory.WithTerminal.star => X.right))
      (match CategoryTheory.WithTerminal.incl.obj X_1,
        match
          Opposite.unop
            (match CategoryTheory.WithTerminal.incl.obj X_1 with
            | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
            | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star) with
        | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
        | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
          | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x)
          | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv with
      | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
        X.left.map (CategoryTheory.WithTerminal.down f)
      | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x
      | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
        CategoryTheory.CategoryStruct.id X.right)

Defined in

Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic

Cited by

0 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category