Documentation

Mathlib.AlgebraicTopology.SimplicialObject.Basic

Simplicial objects in a category. #

A simplicial object in a category C is a C-valued presheaf on SimplexCategory. (Similarly, a cosimplicial object is a functor SimplexCategory ⥤ C.)

Notation #

The following notations can be enabled via open Simplicial.

The following notations can be enabled via open CategoryTheory.SimplicialObject.Truncated.

The category of simplicial objects valued in a category C. This is the category of contravariant functors from SimplexCategory to C.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.comp_app (C : Type u) [Category.{v, u} C] {X✝ Y✝ Z✝ : Functor SimplexCategoryᵒᵖ C} (α : NatTrans X✝ Y✝) (β : NatTrans Y✝ Z✝) (X : SimplexCategoryᵒᵖ) :

    X _⦋n⦌ denotes the nth-term of the simplicial object X

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem CategoryTheory.SimplicialObject.hom_ext {C : Type u} [Category.{v, u} C] {X Y : SimplicialObject C} (f g : X Y) (h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) :
      f = g

      Face maps for a simplicial object.

      Equations
      Instances For

        Degeneracy maps for a simplicial object.

        Equations
        Instances For

          The diagonal of a simplex is the long edge of the simplex.

          Equations
          Instances For

            Isomorphisms from identities in ℕ.

            Equations
            Instances For
              theorem CategoryTheory.SimplicialObject.δ_comp_δ {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i j : Fin (n + 2)} (H : i j) :

              The generic case of the first simplicial identity

              theorem CategoryTheory.SimplicialObject.δ_comp_δ' {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
              theorem CategoryTheory.SimplicialObject.δ_comp_δ'' {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) :
              CategoryStruct.comp (X.δ j.succ) (X.δ (i.castLT )) = CategoryStruct.comp (X.δ i) (X.δ j)

              The special case of the first simplicial identity

              theorem CategoryTheory.SimplicialObject.δ_comp_δ_self' {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = i.castSucc) :
              theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) :

              The second simplicial identity

              The first part of the third simplicial identity

              theorem CategoryTheory.SimplicialObject.δ_comp_σ_self'_assoc {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) {Z : C} (h : X.obj (Opposite.op (SimplexCategory.mk n)) Z) :

              The second part of the third simplicial identity

              theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ'_assoc {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) {Z : C} (h : X.obj (Opposite.op (SimplexCategory.mk n)) Z) :
              theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :

              The fourth simplicial identity

              theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt' {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
              CategoryStruct.comp (X.σ j) (X.δ i) = CategoryStruct.comp (X.δ (i.pred )) (X.σ (j.castLT ))
              theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj (Opposite.op (SimplexCategory.mk (n + 1))) Z) :
              theorem CategoryTheory.SimplicialObject.σ_comp_σ {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n : } {i j : Fin (n + 1)} (H : i j) :

              The fifth simplicial identity

              @[simp]
              theorem CategoryTheory.SimplicialObject.whiskering_obj_map_app (C : Type u) [Category.{v, u} C] (D : Type u_1) [Category.{u_2, u_1} D] (H : Functor C D) {X✝ Y✝ : Functor SimplexCategoryᵒᵖ C} (α : X✝ Y✝) (X : SimplexCategoryᵒᵖ) :
              (((whiskering C D).obj H).map α).app X = H.map (α.app X)
              @[simp]
              theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_map (C : Type u) [Category.{v, u} C] (D : Type u_1) [Category.{u_2, u_1} D] (H : Functor C D) (F : Functor SimplexCategoryᵒᵖ C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ Y✝) :
              (((whiskering C D).obj H).obj F).map f = H.map (F.map f)
              @[simp]
              theorem CategoryTheory.SimplicialObject.whiskering_map_app_app (C : Type u) [Category.{v, u} C] (D : Type u_1) [Category.{u_2, u_1} D] {X✝ Y✝ : Functor C D} (τ : X✝ Y✝) (F : Functor SimplexCategoryᵒᵖ C) (c : SimplexCategoryᵒᵖ) :
              (((whiskering C D).map τ).app F).app c = τ.app (F.obj c)
              @[simp]
              @[simp]

              For X : Truncated C n and m ≤ n, X _⦋m⦌ₙ is the m-th term of X. The proof p : m ≤ n can also be provided using the syntax X _⦋m, p⦌ₙ.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def CategoryTheory.SimplicialObject.Truncated.trunc (C : Type u) [Category.{v, u} C] (n m : ) (h : m n := by omega) :

                Further truncation of truncated simplicial objects.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.SimplicialObject.Truncated.trunc_obj_map (C : Type u) [Category.{v, u} C] (n m : ) (h : m n := by omega) (G : Functor (SimplexCategory.Truncated n)ᵒᵖ C) {X✝ Y✝ : (SimplexCategory.Truncated m)ᵒᵖ} (f : X✝ Y✝) :
                  ((trunc C n m h).obj G).map f = G.map ((SimplexCategory.Truncated.incl m n h).map f.unop).op
                  @[simp]
                  theorem CategoryTheory.SimplicialObject.Truncated.trunc_map_app (C : Type u) [Category.{v, u} C] (n m : ) (h : m n := by omega) {X✝ Y✝ : Functor (SimplexCategory.Truncated n)ᵒᵖ C} (α : X✝ Y✝) (X : (SimplexCategory.Truncated m)ᵒᵖ) :
                  @[reducible, inline]

                  The constant simplicial object is the constant functor.

                  Equations
                  Instances For
                    theorem CategoryTheory.SimplicialObject.Augmented.hom_ext {C : Type u} [Category.{v, u} C] {X Y : Augmented C} (f g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
                    f = g

                    The functor from augmented objects to arrows.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]

                      The compatibility of a morphism with the augmentation, on 0-simplices

                      Functor composition induces a functor on augmented simplicial objects.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Functor composition induces a functor on augmented simplicial objects.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] {X✝ Y✝ : Functor C D} (η : X✝ Y✝) (A : Augmented C) :
                          @[simp]
                          theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_right (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] {X✝ Y✝ : Functor C D} (η : X✝ Y✝) (A : Augmented C) :
                          (((whiskering C D).map η).app A).right = η.app (point.obj A)

                          The constant augmented simplicial object functor.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.SimplicialObject.Augmented.const_map_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ Y✝) :

                            Augment a simplicial object with an object.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.SimplicialObject.augment_left {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (X₀ : C) (f : X.obj (Opposite.op (SimplexCategory.mk 0)) X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 i), CategoryStruct.comp (X.map g₁.op) f = CategoryStruct.comp (X.map g₂.op) f) :
                              (X.augment X₀ f w).left = X
                              @[simp]
                              theorem CategoryTheory.SimplicialObject.augment_right {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (X₀ : C) (f : X.obj (Opposite.op (SimplexCategory.mk 0)) X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 i), CategoryStruct.comp (X.map g₁.op) f = CategoryStruct.comp (X.map g₂.op) f) :
                              (X.augment X₀ f w).right = X₀
                              @[simp]
                              theorem CategoryTheory.CosimplicialObject.comp_app (C : Type u) [Category.{v, u} C] {X✝ Y✝ Z✝ : Functor SimplexCategory C} (α : NatTrans X✝ Y✝) (β : NatTrans Y✝ Z✝) (X : SimplexCategory) :

                              X ^⦋n⦌ denotes the nth-term of the cosimplicial object X

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem CategoryTheory.CosimplicialObject.hom_ext {C : Type u} [Category.{v, u} C] {X Y : CosimplicialObject C} (f g : X Y) (h : ∀ (n : SimplexCategory), f.app n = g.app n) :
                                f = g

                                Coface maps for a cosimplicial object.

                                Equations
                                Instances For

                                  Codegeneracy maps for a cosimplicial object.

                                  Equations
                                  Instances For

                                    Isomorphisms from identities in ℕ.

                                    Equations
                                    Instances For

                                      The generic case of the first cosimplicial identity

                                      theorem CategoryTheory.CosimplicialObject.δ_comp_δ' {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
                                      theorem CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) Z) :
                                      theorem CategoryTheory.CosimplicialObject.δ_comp_δ'' {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) :
                                      CategoryStruct.comp (X.δ (i.castLT )) (X.δ j.succ) = CategoryStruct.comp (X.δ j) (X.δ i)
                                      theorem CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) Z) :

                                      The special case of the first cosimplicial identity

                                      theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self' {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) :
                                      theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) :

                                      The second cosimplicial identity

                                      The first part of the third cosimplicial identity

                                      theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk n) Z) :

                                      The second part of the third cosimplicial identity

                                      theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ'_assoc {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) {Z : C} (h : X.obj (SimplexCategory.mk n) Z) :
                                      theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :

                                      The fourth cosimplicial identity

                                      theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt' {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
                                      CategoryStruct.comp (X.δ i) (X.σ j) = CategoryStruct.comp (X.σ (j.castLT )) (X.δ (i.pred ))
                                      theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) Z) :

                                      The fifth cosimplicial identity

                                      @[simp]
                                      theorem CategoryTheory.CosimplicialObject.whiskering_obj_obj_map (C : Type u) [Category.{v, u} C] (D : Type u_1) [Category.{u_2, u_1} D] (H : Functor C D) (F : Functor SimplexCategory C) {X✝ Y✝ : SimplexCategory} (f : X✝ Y✝) :
                                      (((whiskering C D).obj H).obj F).map f = H.map (F.map f)
                                      @[simp]
                                      theorem CategoryTheory.CosimplicialObject.whiskering_obj_map_app (C : Type u) [Category.{v, u} C] (D : Type u_1) [Category.{u_2, u_1} D] (H : Functor C D) {X✝ Y✝ : Functor SimplexCategory C} (α : X✝ Y✝) (X : SimplexCategory) :
                                      (((whiskering C D).obj H).map α).app X = H.map (α.app X)
                                      @[simp]
                                      theorem CategoryTheory.CosimplicialObject.whiskering_map_app_app (C : Type u) [Category.{v, u} C] (D : Type u_1) [Category.{u_2, u_1} D] {X✝ Y✝ : Functor C D} (τ : X✝ Y✝) (F : Functor SimplexCategory C) (c : SimplexCategory) :
                                      (((whiskering C D).map τ).app F).app c = τ.app (F.obj c)

                                      Functor composition induces a functor on truncated cosimplicial objects.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app (C : Type u) [Category.{v, u} C] {n : } (D : Type u_1) [Category.{u_2, u_1} D] {X✝ Y✝ : Functor C D} (τ : X✝ Y✝) (F : Functor (SimplexCategory.Truncated n) C) (c : SimplexCategory.Truncated n) :
                                        (((whiskering C D).map τ).app F).app c = τ.app (F.obj c)
                                        @[simp]
                                        theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app (C : Type u) [Category.{v, u} C] {n : } (D : Type u_1) [Category.{u_2, u_1} D] (H : Functor C D) {X✝ Y✝ : Functor (SimplexCategory.Truncated n) C} (α : X✝ Y✝) (X : SimplexCategory.Truncated n) :
                                        (((whiskering C D).obj H).map α).app X = H.map (α.app X)
                                        @[simp]
                                        theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map (C : Type u) [Category.{v, u} C] {n : } (D : Type u_1) [Category.{u_2, u_1} D] (H : Functor C D) (F : Functor (SimplexCategory.Truncated n) C) {X✝ Y✝ : SimplexCategory.Truncated n} (f : X✝ Y✝) :
                                        (((whiskering C D).obj H).obj F).map f = H.map (F.map f)

                                        For X : Truncated C n and m ≤ n, X ^⦋m⦌ₙ is the m-th term of X. The proof p : m ≤ n can also be provided using the syntax X ^⦋m, p⦌ₙ.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def CategoryTheory.CosimplicialObject.Truncated.trunc (C : Type u) [Category.{v, u} C] (n m : ) (h : m n := by omega) :

                                          Further truncation of truncated cosimplicial objects.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            For all m ≤ n, truncation m factors through Truncated n.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem CategoryTheory.CosimplicialObject.Augmented.hom_ext {C : Type u} [Category.{v, u} C] {X Y : Augmented C} (f g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
                                              f = g

                                              The functor from augmented objects to arrows.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]

                                                Functor composition induces a functor on augmented cosimplicial objects.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Functor composition induces a functor on augmented cosimplicial objects.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_left (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] {X✝ Y✝ : Functor C D} (η : X✝ Y✝) (A : Augmented C) :
                                                    (((whiskering C D).map η).app A).left = η.app (point.obj A)
                                                    @[simp]

                                                    The constant augmented cosimplicial object functor.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.CosimplicialObject.Augmented.const_map_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ Y✝) :
                                                      (const.map f).left = f

                                                      Augment a cosimplicial object with an object.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.CosimplicialObject.augment_hom_app {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) (X₀ : C) (f : X₀ X.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 i), CategoryStruct.comp f (X.map g₁) = CategoryStruct.comp f (X.map g₂)) (x✝ : SimplexCategory) :
                                                        (X.augment X₀ f w).hom.app x✝ = CategoryStruct.comp f (X.map ((SimplexCategory.mk 0).const x✝ 0))
                                                        @[simp]
                                                        theorem CategoryTheory.CosimplicialObject.augment_right {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) (X₀ : C) (f : X₀ X.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 i), CategoryStruct.comp f (X.map g₁) = CategoryStruct.comp f (X.map g₂)) :
                                                        (X.augment X₀ f w).right = X
                                                        @[simp]
                                                        theorem CategoryTheory.CosimplicialObject.augment_left {C : Type u} [Category.{v, u} C] (X : CosimplicialObject C) (X₀ : C) (f : X₀ X.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 i), CategoryStruct.comp f (X.map g₁) = CategoryStruct.comp f (X.map g₂)) :
                                                        (X.augment X₀ f w).left = X₀

                                                        Construct an augmented cosimplicial object in the opposite category from an augmented simplicial object.

                                                        Equations
                                                        Instances For

                                                          Construct an augmented simplicial object from an augmented cosimplicial object in the opposite category.

                                                          Equations
                                                          Instances For

                                                            Converting an augmented simplicial object to an augmented cosimplicial object and back is isomorphic to the given object.

                                                            Equations
                                                            Instances For

                                                              Converting an augmented cosimplicial object to an augmented simplicial object and back is isomorphic to the given object.

                                                              Equations
                                                              Instances For

                                                                A functorial version of SimplicialObject.Augmented.rightOp.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For

                                                                  A functorial version of Cosimplicial_object.Augmented.leftOp.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For

                                                                    The contravariant categorical equivalence between augmented simplicial objects and augmented cosimplicial objects in the opposite category.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For