Theorems · Theorem · category theory

AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C)
  (X_1 : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.unitIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (match
          match Opposite.unop X_1 with
          | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
          | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with
        | CategoryTheory.WithTerminal.of x =>
          (CategoryTheory.Iso.refl
                (CategoryTheory.WithTerminal.incl.comp
                  ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app
            x
        | CategoryTheory.WithTerminal.star =>
          CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).inv
      (X.map
        (match Opposite.unop X_1 with
          | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x))
          | CategoryTheory.WithInitial.star =>
            CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv)

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