Simplicial objects in a category. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A simplicial object in a category C is a C-valued presheaf on simplex_category.
(Similarly a cosimplicial object is functor simplex_category ⥤ C.)
Use the notation X _[n] in the simplicial locale to obtain the n-th term of a
(co)simplicial object X, where n is a natural number.
@[nolint]
The category of simplicial objects valued in a category C.
This is the category of contravariant functors from simplex_category to C.
Equations
Instances for category_theory.simplicial_object
- category_theory.simplicial_object.category
- category_theory.simplicial_object.category_theory.limits.has_limits_of_shape
- category_theory.simplicial_object.category_theory.limits.has_limits
- category_theory.simplicial_object.category_theory.limits.has_colimits_of_shape
- category_theory.simplicial_object.category_theory.limits.has_colimits
- category_theory.idempotents.category_theory.simplicial_object.category_theory.is_idempotent_complete
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.simplicial_object.δ
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
(i : fin (n + 2)) :
X.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X.obj (opposite.op (simplex_category.mk n))
Face maps for a simplicial object.
Equations
- X.δ i = X.map (simplex_category.δ i).op
def
category_theory.simplicial_object.σ
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
(i : fin (n + 1)) :
X.obj (opposite.op (simplex_category.mk n)) ⟶ X.obj (opposite.op (simplex_category.mk (n + 1)))
Degeneracy maps for a simplicial object.
Equations
- X.σ i = X.map (simplex_category.σ i).op
def
category_theory.simplicial_object.eq_to_iso
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n m : ℕ}
(h : n = m) :
X.obj (opposite.op (simplex_category.mk n)) ≅ X.obj (opposite.op (simplex_category.mk m))
Isomorphisms from identities in ℕ.
Equations
@[simp]
theorem
category_theory.simplicial_object.eq_to_iso_refl
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
(h : n = n) :
X.eq_to_iso h = category_theory.iso.refl (X.obj (opposite.op (simplex_category.mk n)))
theorem
category_theory.simplicial_object.δ_comp_δ
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i j : fin (n + 2)}
(H : i ≤ j) :
The generic case of the first simplicial identity
theorem
category_theory.simplicial_object.δ_comp_δ_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i j : fin (n + 2)}
(H : i ≤ j)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_δ'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : ⇑fin.cast_succ i < j)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_δ'
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : ⇑fin.cast_succ i < j) :
theorem
category_theory.simplicial_object.δ_comp_δ''_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : i ≤ ⇑fin.cast_succ j)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_δ_self
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)} :
The special case of the first simplicial identity
theorem
category_theory.simplicial_object.δ_comp_δ_self_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_δ_self'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{j : fin (n + 3)}
{i : fin (n + 2)}
(H : j = ⇑fin.cast_succ i)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_of_le
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : i ≤ ⇑fin.cast_succ j) :
The second simplicial identity
theorem
category_theory.simplicial_object.δ_comp_σ_of_le_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : i ≤ ⇑fin.cast_succ j)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_self_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 1)}
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_self
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 1)} :
X.σ i ≫ X.δ (⇑fin.cast_succ i) = 𝟙 (X.obj (opposite.op (simplex_category.mk n)))
The first part of the third simplicial identity
theorem
category_theory.simplicial_object.δ_comp_σ_self'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = ⇑fin.cast_succ i)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_self'
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = ⇑fin.cast_succ i) :
X.σ i ≫ X.δ j = 𝟙 (X.obj (opposite.op (simplex_category.mk n)))
theorem
category_theory.simplicial_object.δ_comp_σ_succ_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 1)}
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_succ
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 1)} :
X.σ i ≫ X.δ i.succ = 𝟙 (X.obj (opposite.op (simplex_category.mk n)))
The second part of the third simplicial identity
theorem
category_theory.simplicial_object.δ_comp_σ_succ'
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = i.succ) :
X.σ i ≫ X.δ j = 𝟙 (X.obj (opposite.op (simplex_category.mk n)))
theorem
category_theory.simplicial_object.δ_comp_σ_succ'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = i.succ)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk n)) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_of_gt_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : ⇑fin.cast_succ j < i)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X') :
theorem
category_theory.simplicial_object.δ_comp_σ_of_gt
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : ⇑fin.cast_succ j < i) :
The fourth simplicial identity
theorem
category_theory.simplicial_object.δ_comp_σ_of_gt'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : j.succ < i)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X') :
theorem
category_theory.simplicial_object.σ_comp_σ_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i j : fin (n + 1)}
(H : i ≤ j)
{X' : C}
(f' : X.obj (opposite.op (simplex_category.mk (n + 1 + 1))) ⟶ X') :
theorem
category_theory.simplicial_object.σ_comp_σ
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
{n : ℕ}
{i j : fin (n + 1)}
(H : i ≤ j) :
The fifth simplicial identity
@[simp]
theorem
category_theory.simplicial_object.δ_naturality_assoc
{C : Type u}
[category_theory.category C]
{X' X : category_theory.simplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 2))
{X'_1 : C}
(f' : X'.obj (opposite.op (simplex_category.mk n)) ⟶ X'_1) :
X.δ i ≫ f.app (opposite.op (simplex_category.mk n)) ≫ f' = f.app (opposite.op (simplex_category.mk (n + 1))) ≫ X'.δ i ≫ f'
@[simp]
theorem
category_theory.simplicial_object.δ_naturality
{C : Type u}
[category_theory.category C]
{X' X : category_theory.simplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 2)) :
X.δ i ≫ f.app (opposite.op (simplex_category.mk n)) = f.app (opposite.op (simplex_category.mk (n + 1))) ≫ X'.δ i
@[simp]
theorem
category_theory.simplicial_object.σ_naturality
{C : Type u}
[category_theory.category C]
{X' X : category_theory.simplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 1)) :
X.σ i ≫ f.app (opposite.op (simplex_category.mk (n + 1))) = f.app (opposite.op (simplex_category.mk n)) ≫ X'.σ i
@[simp]
theorem
category_theory.simplicial_object.σ_naturality_assoc
{C : Type u}
[category_theory.category C]
{X' X : category_theory.simplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 1))
{X'_1 : C}
(f' : X'.obj (opposite.op (simplex_category.mk (n + 1))) ⟶ X'_1) :
X.σ i ≫ f.app (opposite.op (simplex_category.mk (n + 1))) ≫ f' = f.app (opposite.op (simplex_category.mk n)) ≫ X'.σ i ≫ f'
@[simp]
theorem
category_theory.simplicial_object.whiskering_obj_obj_map
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : simplex_categoryᵒᵖ ⥤ C)
(_x _x_1 : simplex_categoryᵒᵖ)
(f : _x ⟶ _x_1) :
@[simp]
theorem
category_theory.simplicial_object.whiskering_map_app_app
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(G H : C ⥤ D)
(τ : G ⟶ H)
(F : simplex_categoryᵒᵖ ⥤ C)
(c : simplex_categoryᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_object.whiskering_obj_obj_obj
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : simplex_categoryᵒᵖ ⥤ C)
(X : simplex_categoryᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_object.whiskering_obj_map_app
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(_x _x_1 : simplex_categoryᵒᵖ ⥤ C)
(α : _x ⟶ _x_1)
(X : simplex_categoryᵒᵖ) :
def
category_theory.simplicial_object.whiskering
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D] :
Functor composition induces a functor on simplicial objects.
@[protected, instance]
@[nolint]
def
category_theory.simplicial_object.truncated
(C : Type u)
[category_theory.category C]
(n : ℕ) :
Type (max v u)
Truncated simplicial objects.
Equations
Instances for category_theory.simplicial_object.truncated
- category_theory.simplicial_object.truncated.category
- category_theory.simplicial_object.truncated.category_theory.limits.has_limits_of_shape
- category_theory.simplicial_object.truncated.category_theory.limits.has_limits
- category_theory.simplicial_object.truncated.category_theory.limits.has_colimits_of_shape
- category_theory.simplicial_object.truncated.category_theory.limits.has_colimits
@[protected, instance]
def
category_theory.simplicial_object.truncated.category_theory.limits.has_limits_of_shape
{C : Type u}
[category_theory.category C]
{n : ℕ}
{J : Type v}
[category_theory.small_category J]
[category_theory.limits.has_limits_of_shape J C] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem
category_theory.simplicial_object.truncated.whiskering_obj_obj_obj
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : (simplex_category.truncated n)ᵒᵖ ⥤ C)
(X : (simplex_category.truncated n)ᵒᵖ) :
def
category_theory.simplicial_object.truncated.whiskering
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D] :
Functor composition induces a functor on truncated simplicial objects.
@[simp]
theorem
category_theory.simplicial_object.truncated.whiskering_obj_map_app
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(_x _x_1 : (simplex_category.truncated n)ᵒᵖ ⥤ C)
(α : _x ⟶ _x_1)
(X : (simplex_category.truncated n)ᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_object.truncated.whiskering_map_app_app
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(G H : C ⥤ D)
(τ : G ⟶ H)
(F : (simplex_category.truncated n)ᵒᵖ ⥤ C)
(c : (simplex_category.truncated n)ᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_object.truncated.whiskering_obj_obj_map
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : (simplex_category.truncated n)ᵒᵖ ⥤ C)
(_x _x_1 : (simplex_category.truncated n)ᵒᵖ)
(f : _x ⟶ _x_1) :
The skeleton functor from simplicial objects to truncated simplicial objects.
@[reducible]
The constant simplicial object is the constant functor.
@[protected, instance]
@[nolint]
def
category_theory.simplicial_object.augmented
(C : Type u)
[category_theory.category C] :
Type (max (max v u) u v)
The category of augmented simplicial objects, defined as a comma category.
Equations
Instances for category_theory.simplicial_object.augmented
@[simp]
theorem
category_theory.simplicial_object.augmented.drop_map
{C : Type u}
[category_theory.category C]
(_x _x_1 : category_theory.comma (𝟭 (category_theory.simplicial_object C)) (category_theory.simplicial_object.const C))
(f : _x ⟶ _x_1) :
Drop the augmentation.
@[simp]
@[simp]
theorem
category_theory.simplicial_object.augmented.point_map
{C : Type u}
[category_theory.category C]
(_x _x_1 : category_theory.comma (𝟭 (category_theory.simplicial_object C)) (category_theory.simplicial_object.const C))
(f : _x ⟶ _x_1) :
The point of the augmentation.
@[simp]
def
category_theory.simplicial_object.augmented.to_arrow
{C : Type u}
[category_theory.category C] :
The functor from augmented objects to arrows.
Equations
- category_theory.simplicial_object.augmented.to_arrow = {obj := λ (X : category_theory.simplicial_object.augmented C), {left := (category_theory.simplicial_object.augmented.drop.obj X).obj (opposite.op (simplex_category.mk 0)), right := category_theory.simplicial_object.augmented.point.obj X, hom := X.hom.app (opposite.op (simplex_category.mk 0))}, map := λ (X Y : category_theory.simplicial_object.augmented C) (η : X ⟶ Y), {left := (category_theory.simplicial_object.augmented.drop.map η).app (opposite.op (simplex_category.mk 0)), right := category_theory.simplicial_object.augmented.point.map η, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.simplicial_object.augmented.to_arrow_map_left
{C : Type u}
[category_theory.category C]
(X Y : category_theory.simplicial_object.augmented C)
(η : X ⟶ Y) :
@[simp]
theorem
category_theory.simplicial_object.augmented.to_arrow_map_right
{C : Type u}
[category_theory.category C]
(X Y : category_theory.simplicial_object.augmented C)
(η : X ⟶ Y) :
@[simp]
@[simp]
@[simp]
theorem
category_theory.simplicial_object.augmented.to_arrow_obj_left
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C) :
theorem
category_theory.simplicial_object.augmented.w₀
{C : Type u}
[category_theory.category C]
{X Y : category_theory.simplicial_object.augmented C}
(f : X ⟶ Y) :
The compatibility of a morphism with the augmentation, on 0-simplices
theorem
category_theory.simplicial_object.augmented.w₀_assoc
{C : Type u}
[category_theory.category C]
{X Y : category_theory.simplicial_object.augmented C}
(f : X ⟶ Y)
{X' : C}
(f' : ((category_theory.simplicial_object.const C).obj Y.right).obj (opposite.op (simplex_category.mk 0)) ⟶ X') :
@[simp]
def
category_theory.simplicial_object.augmented.whiskering_obj
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(F : C ⥤ D) :
Functor composition induces a functor on augmented simplicial objects.
Equations
- category_theory.simplicial_object.augmented.whiskering_obj C D F = {obj := λ (X : category_theory.simplicial_object.augmented C), {left := ((category_theory.simplicial_object.whiskering C D).obj F).obj (category_theory.simplicial_object.augmented.drop.obj X), right := F.obj (category_theory.simplicial_object.augmented.point.obj X), hom := category_theory.whisker_right X.hom F ≫ (category_theory.functor.const_comp simplex_categoryᵒᵖ X.right F).hom}, map := λ (X Y : category_theory.simplicial_object.augmented C) (η : X ⟶ Y), {left := category_theory.whisker_right η.left F, right := F.map η.right, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.simplicial_object.augmented.whiskering_map_app_right
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
(X Y : C ⥤ D)
(η : X ⟶ Y)
(A : category_theory.simplicial_object.augmented C) :
@[simp]
theorem
category_theory.simplicial_object.augmented.whiskering_obj_2
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
(F : C ⥤ D) :
@[simp]
theorem
category_theory.simplicial_object.augmented.whiskering_map_app_left
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
(X Y : C ⥤ D)
(η : X ⟶ Y)
(A : category_theory.simplicial_object.augmented C) :
def
category_theory.simplicial_object.augmented.whiskering
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D] :
Functor composition induces a functor on augmented simplicial objects.
Equations
- category_theory.simplicial_object.augmented.whiskering C D = {obj := category_theory.simplicial_object.augmented.whiskering_obj C D _inst_2, map := λ (X Y : C ⥤ D) (η : X ⟶ Y), {app := λ (A : category_theory.simplicial_object.augmented C), {left := category_theory.whisker_left (category_theory.simplicial_object.augmented.drop.obj A) η, right := η.app (category_theory.simplicial_object.augmented.point.obj A), w' := _}, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.simplicial_object.augment_left
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
(X₀ : C)
(f : X.obj (opposite.op (simplex_category.mk 0)) ⟶ X₀)
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f) :
def
category_theory.simplicial_object.augment
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
(X₀ : C)
(f : X.obj (opposite.op (simplex_category.mk 0)) ⟶ X₀)
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f) :
Augment a simplicial object with an object.
@[simp]
theorem
category_theory.simplicial_object.augment_right
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
(X₀ : C)
(f : X.obj (opposite.op (simplex_category.mk 0)) ⟶ X₀)
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f) :
@[simp]
theorem
category_theory.simplicial_object.augment_hom_app
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
(X₀ : C)
(f : X.obj (opposite.op (simplex_category.mk 0)) ⟶ X₀)
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f)
(i : simplex_categoryᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_object.augment_hom_zero
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object C)
(X₀ : C)
(f : X.obj (opposite.op (simplex_category.mk 0)) ⟶ X₀)
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f) :
(X.augment X₀ f w).hom.app (opposite.op (simplex_category.mk 0)) = f
@[protected, instance]
@[nolint]
Cosimplicial objects.
Equations
Instances for category_theory.cosimplicial_object
- category_theory.cosimplicial_object.category
- category_theory.cosimplicial_object.category_theory.limits.has_limits_of_shape
- category_theory.cosimplicial_object.category_theory.limits.has_limits
- category_theory.cosimplicial_object.category_theory.limits.has_colimits_of_shape
- category_theory.cosimplicial_object.category_theory.limits.has_colimits
- category_theory.idempotents.category_theory.cosimplicial_object.category_theory.is_idempotent_complete
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.cosimplicial_object.δ
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
(i : fin (n + 2)) :
X.obj (simplex_category.mk n) ⟶ X.obj (simplex_category.mk (n + 1))
Coface maps for a cosimplicial object.
Equations
- X.δ i = X.map (simplex_category.δ i)
def
category_theory.cosimplicial_object.σ
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
(i : fin (n + 1)) :
X.obj (simplex_category.mk (n + 1)) ⟶ X.obj (simplex_category.mk n)
Codegeneracy maps for a cosimplicial object.
Equations
- X.σ i = X.map (simplex_category.σ i)
def
category_theory.cosimplicial_object.eq_to_iso
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n m : ℕ}
(h : n = m) :
X.obj (simplex_category.mk n) ≅ X.obj (simplex_category.mk m)
Isomorphisms from identities in ℕ.
Equations
@[simp]
theorem
category_theory.cosimplicial_object.eq_to_iso_refl
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
(h : n = n) :
X.eq_to_iso h = category_theory.iso.refl (X.obj (simplex_category.mk n))
theorem
category_theory.cosimplicial_object.δ_comp_δ
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i j : fin (n + 2)}
(H : i ≤ j) :
The generic case of the first cosimplicial identity
theorem
category_theory.cosimplicial_object.δ_comp_δ_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i j : fin (n + 2)}
(H : i ≤ j)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1 + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_δ'
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : ⇑fin.cast_succ i < j) :
theorem
category_theory.cosimplicial_object.δ_comp_δ'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : ⇑fin.cast_succ i < j)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1 + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_δ''_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : i ≤ ⇑fin.cast_succ j)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1 + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_δ_self_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1 + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_δ_self
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)} :
The special case of the first cosimplicial identity
theorem
category_theory.cosimplicial_object.δ_comp_δ_self'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : j = ⇑fin.cast_succ i)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1 + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_of_le_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : i ≤ ⇑fin.cast_succ j)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_of_le
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : i ≤ ⇑fin.cast_succ j) :
The second cosimplicial identity
theorem
category_theory.cosimplicial_object.δ_comp_σ_self_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 1)}
{X' : C}
(f' : X.obj (simplex_category.mk n) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_self
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 1)} :
X.δ (⇑fin.cast_succ i) ≫ X.σ i = 𝟙 (X.obj (simplex_category.mk n))
The first part of the third cosimplicial identity
theorem
category_theory.cosimplicial_object.δ_comp_σ_self'
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = ⇑fin.cast_succ i) :
theorem
category_theory.cosimplicial_object.δ_comp_σ_self'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = ⇑fin.cast_succ i)
{X' : C}
(f' : X.obj (simplex_category.mk n) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_succ_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 1)}
{X' : C}
(f' : X.obj (simplex_category.mk n) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_succ
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 1)} :
The second part of the third cosimplicial identity
theorem
category_theory.cosimplicial_object.δ_comp_σ_succ'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = i.succ)
{X' : C}
(f' : X.obj (simplex_category.mk n) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_succ'
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = i.succ) :
theorem
category_theory.cosimplicial_object.δ_comp_σ_of_gt
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : ⇑fin.cast_succ j < i) :
The fourth cosimplicial identity
theorem
category_theory.cosimplicial_object.δ_comp_σ_of_gt_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : ⇑fin.cast_succ j < i)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.δ_comp_σ_of_gt'_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : j.succ < i)
{X' : C}
(f' : X.obj (simplex_category.mk (n + 1)) ⟶ X') :
theorem
category_theory.cosimplicial_object.σ_comp_σ_assoc
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i j : fin (n + 1)}
(H : i ≤ j)
{X' : C}
(f' : X.obj (simplex_category.mk n) ⟶ X') :
theorem
category_theory.cosimplicial_object.σ_comp_σ
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
{n : ℕ}
{i j : fin (n + 1)}
(H : i ≤ j) :
The fifth cosimplicial identity
@[simp]
theorem
category_theory.cosimplicial_object.δ_naturality_assoc
{C : Type u}
[category_theory.category C]
{X' X : category_theory.cosimplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 2))
{X'_1 : C}
(f' : X'.obj (simplex_category.mk (n + 1)) ⟶ X'_1) :
@[simp]
theorem
category_theory.cosimplicial_object.δ_naturality
{C : Type u}
[category_theory.category C]
{X' X : category_theory.cosimplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 2)) :
X.δ i ≫ f.app (simplex_category.mk (n + 1)) = f.app (simplex_category.mk n) ≫ X'.δ i
@[simp]
theorem
category_theory.cosimplicial_object.σ_naturality_assoc
{C : Type u}
[category_theory.category C]
{X' X : category_theory.cosimplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 1))
{X'_1 : C}
(f' : X'.obj (simplex_category.mk n) ⟶ X'_1) :
@[simp]
theorem
category_theory.cosimplicial_object.σ_naturality
{C : Type u}
[category_theory.category C]
{X' X : category_theory.cosimplicial_object C}
(f : X ⟶ X')
{n : ℕ}
(i : fin (n + 1)) :
X.σ i ≫ f.app (simplex_category.mk n) = f.app (simplex_category.mk (n + 1)) ≫ X'.σ i
@[simp]
theorem
category_theory.cosimplicial_object.whiskering_obj_obj_obj
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : simplex_category ⥤ C)
(X : simplex_category) :
@[simp]
theorem
category_theory.cosimplicial_object.whiskering_obj_map_app
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(_x _x_1 : simplex_category ⥤ C)
(α : _x ⟶ _x_1)
(X : simplex_category) :
@[simp]
theorem
category_theory.cosimplicial_object.whiskering_map_app_app
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(G H : C ⥤ D)
(τ : G ⟶ H)
(F : simplex_category ⥤ C)
(c : simplex_category) :
def
category_theory.cosimplicial_object.whiskering
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D] :
Functor composition induces a functor on cosimplicial objects.
@[simp]
theorem
category_theory.cosimplicial_object.whiskering_obj_obj_map
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : simplex_category ⥤ C)
(_x _x_1 : simplex_category)
(f : _x ⟶ _x_1) :
@[protected, instance]
@[nolint]
def
category_theory.cosimplicial_object.truncated
(C : Type u)
[category_theory.category C]
(n : ℕ) :
Type (max v u)
Truncated cosimplicial objects.
Equations
Instances for category_theory.cosimplicial_object.truncated
- category_theory.cosimplicial_object.truncated.category
- category_theory.cosimplicial_object.truncated.category_theory.limits.has_limits_of_shape
- category_theory.cosimplicial_object.truncated.category_theory.limits.has_limits
- category_theory.cosimplicial_object.truncated.category_theory.limits.has_colimits_of_shape
- category_theory.cosimplicial_object.truncated.category_theory.limits.has_colimits
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.cosimplicial_object.truncated.whiskering
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D] :
Functor composition induces a functor on truncated cosimplicial objects.
@[simp]
theorem
category_theory.cosimplicial_object.truncated.whiskering_obj_map_app
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(_x _x_1 : simplex_category.truncated n ⥤ C)
(α : _x ⟶ _x_1)
(X : simplex_category.truncated n) :
@[simp]
theorem
category_theory.cosimplicial_object.truncated.whiskering_map_app_app
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(G H : C ⥤ D)
(τ : G ⟶ H)
(F : simplex_category.truncated n ⥤ C)
(c : simplex_category.truncated n) :
@[simp]
theorem
category_theory.cosimplicial_object.truncated.whiskering_obj_obj_map
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : simplex_category.truncated n ⥤ C)
(_x _x_1 : simplex_category.truncated n)
(f : _x ⟶ _x_1) :
@[simp]
theorem
category_theory.cosimplicial_object.truncated.whiskering_obj_obj_obj
(C : Type u)
[category_theory.category C]
{n : ℕ}
(D : Type u_1)
[category_theory.category D]
(H : C ⥤ D)
(F : simplex_category.truncated n ⥤ C)
(X : simplex_category.truncated n) :
The skeleton functor from cosimplicial objects to truncated cosimplicial objects.
@[reducible]
The constant cosimplicial object.
@[protected, instance]
@[nolint]
def
category_theory.cosimplicial_object.augmented
(C : Type u)
[category_theory.category C] :
Type (max v u)
Augmented cosimplicial objects.
Equations
Instances for category_theory.cosimplicial_object.augmented
Drop the augmentation.
@[simp]
theorem
category_theory.cosimplicial_object.augmented.drop_map
{C : Type u}
[category_theory.category C]
(_x _x_1 : category_theory.comma (category_theory.cosimplicial_object.const C) (𝟭 (category_theory.cosimplicial_object C)))
(f : _x ⟶ _x_1) :
@[simp]
@[simp]
The point of the augmentation.
@[simp]
theorem
category_theory.cosimplicial_object.augmented.point_map
{C : Type u}
[category_theory.category C]
(_x _x_1 : category_theory.comma (category_theory.cosimplicial_object.const C) (𝟭 (category_theory.cosimplicial_object C)))
(f : _x ⟶ _x_1) :
@[simp]
@[simp]
theorem
category_theory.cosimplicial_object.augmented.to_arrow_map_left
{C : Type u}
[category_theory.category C]
(X Y : category_theory.cosimplicial_object.augmented C)
(η : X ⟶ Y) :
@[simp]
theorem
category_theory.cosimplicial_object.augmented.to_arrow_map_right
{C : Type u}
[category_theory.category C]
(X Y : category_theory.cosimplicial_object.augmented C)
(η : X ⟶ Y) :
def
category_theory.cosimplicial_object.augmented.to_arrow
{C : Type u}
[category_theory.category C] :
The functor from augmented objects to arrows.
Equations
- category_theory.cosimplicial_object.augmented.to_arrow = {obj := λ (X : category_theory.cosimplicial_object.augmented C), {left := category_theory.cosimplicial_object.augmented.point.obj X, right := (category_theory.cosimplicial_object.augmented.drop.obj X).obj (simplex_category.mk 0), hom := X.hom.app (simplex_category.mk 0)}, map := λ (X Y : category_theory.cosimplicial_object.augmented C) (η : X ⟶ Y), {left := category_theory.cosimplicial_object.augmented.point.map η, right := (category_theory.cosimplicial_object.augmented.drop.map η).app (simplex_category.mk 0), w' := _}, map_id' := _, map_comp' := _}
@[simp]
@[simp]
@[simp]
def
category_theory.cosimplicial_object.augmented.whiskering_obj
(C : Type u)
[category_theory.category C]
(D : Type u_1)
[category_theory.category D]
(F : C ⥤ D) :
Functor composition induces a functor on augmented cosimplicial objects.
Equations
- category_theory.cosimplicial_object.augmented.whiskering_obj C D F = {obj := λ (X : category_theory.cosimplicial_object.augmented C), {left := F.obj (category_theory.cosimplicial_object.augmented.point.obj X), right := ((category_theory.cosimplicial_object.whiskering C D).obj F).obj (category_theory.cosimplicial_object.augmented.drop.obj X), hom := (category_theory.functor.const_comp simplex_category (category_theory.cosimplicial_object.augmented.point.obj X) F).inv ≫ category_theory.whisker_right X.hom F}, map := λ (X Y : category_theory.cosimplicial_object.augmented C) (η : X ⟶ Y), {left := F.map η.left, right := category_theory.whisker_right η.right F, w' := _}, map_id' := _, map_comp' := _}
def
category_theory.cosimplicial_object.augmented.whiskering
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D] :
Functor composition induces a functor on augmented cosimplicial objects.
Equations
- category_theory.cosimplicial_object.augmented.whiskering C D = {obj := category_theory.cosimplicial_object.augmented.whiskering_obj C D _inst_2, map := λ (X Y : C ⥤ D) (η : X ⟶ Y), {app := λ (A : category_theory.cosimplicial_object.augmented C), {left := η.app (category_theory.cosimplicial_object.augmented.point.obj A), right := category_theory.whisker_left (category_theory.cosimplicial_object.augmented.drop.obj A) η, w' := _}, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.cosimplicial_object.augmented.whiskering_map_app_left
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
(X Y : C ⥤ D)
(η : X ⟶ Y)
(A : category_theory.cosimplicial_object.augmented C) :
@[simp]
theorem
category_theory.cosimplicial_object.augmented.whiskering_obj_2
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
(F : C ⥤ D) :
@[simp]
theorem
category_theory.cosimplicial_object.augmented.whiskering_map_app_right
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
(X Y : C ⥤ D)
(η : X ⟶ Y)
(A : category_theory.cosimplicial_object.augmented C) :
def
category_theory.cosimplicial_object.augment
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
(X₀ : C)
(f : X₀ ⟶ X.obj (simplex_category.mk 0))
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂) :
Augment a cosimplicial object with an object.
@[simp]
theorem
category_theory.cosimplicial_object.augment_hom_app
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
(X₀ : C)
(f : X₀ ⟶ X.obj (simplex_category.mk 0))
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂)
(i : simplex_category) :
@[simp]
theorem
category_theory.cosimplicial_object.augment_right
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
(X₀ : C)
(f : X₀ ⟶ X.obj (simplex_category.mk 0))
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂) :
@[simp]
theorem
category_theory.cosimplicial_object.augment_left
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
(X₀ : C)
(f : X₀ ⟶ X.obj (simplex_category.mk 0))
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂) :
@[simp]
theorem
category_theory.cosimplicial_object.augment_hom_zero
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object C)
(X₀ : C)
(f : X₀ ⟶ X.obj (simplex_category.mk 0))
(w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂) :
(X.augment X₀ f w).hom.app (simplex_category.mk 0) = f
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_functor_obj_map
(C : Type u)
[category_theory.category C]
(F : (simplex_categoryᵒᵖ ⥤ C)ᵒᵖ)
(X Y : simplex_category)
(f : X ⟶ Y) :
((category_theory.simplicial_cosimplicial_equiv C).functor.obj F).map f = ((opposite.unop F).map f.op).op
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_unit_iso_hom_app
(C : Type u)
[category_theory.category C]
(X : (simplex_categoryᵒᵖ ⥤ C)ᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_inverse_map
(C : Type u)
[category_theory.category C]
(F G : simplex_category ⥤ Cᵒᵖ)
(η : F ⟶ G) :
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_unit_iso_inv_app
(C : Type u)
[category_theory.category C]
(X : (simplex_categoryᵒᵖ ⥤ C)ᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_functor_obj_obj
(C : Type u)
[category_theory.category C]
(F : (simplex_categoryᵒᵖ ⥤ C)ᵒᵖ)
(X : simplex_category) :
((category_theory.simplicial_cosimplicial_equiv C).functor.obj F).obj X = opposite.op ((opposite.unop F).obj (opposite.op X))
The anti-equivalence between simplicial objects and cosimplicial objects.
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_counit_iso_inv_app_app
(C : Type u)
[category_theory.category C]
(X : simplex_category ⥤ Cᵒᵖ)
(X_1 : simplex_category) :
((category_theory.simplicial_cosimplicial_equiv C).counit_iso.inv.app X).app X_1 = 𝟙 (X.obj X_1)
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_functor_map_app
(C : Type u)
[category_theory.category C]
(F G : (simplex_categoryᵒᵖ ⥤ C)ᵒᵖ)
(η : F ⟶ G)
(X : simplex_category) :
((category_theory.simplicial_cosimplicial_equiv C).functor.map η).app X = (η.unop.app (opposite.op X)).op
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_inverse_obj
(C : Type u)
[category_theory.category C]
(F : simplex_category ⥤ Cᵒᵖ) :
@[simp]
theorem
category_theory.simplicial_cosimplicial_equiv_counit_iso_hom_app_app
(C : Type u)
[category_theory.category C]
(X : simplex_category ⥤ Cᵒᵖ)
(X_1 : simplex_category) :
((category_theory.simplicial_cosimplicial_equiv C).counit_iso.hom.app X).app X_1 = 𝟙 (X.obj X_1)
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_inverse_map
(C : Type u)
[category_theory.category C]
(F G : simplex_categoryᵒᵖ ⥤ Cᵒᵖ)
(α : F ⟶ G) :
(category_theory.cosimplicial_simplicial_equiv C).inverse.map α = quiver.hom.op {app := λ (X : simplex_category), (α.app (opposite.op X)).unop, naturality' := _}
The anti-equivalence between cosimplicial objects and simplicial objects.
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_unit_iso_hom_app
(C : Type u)
[category_theory.category C]
(X : (simplex_category ⥤ C)ᵒᵖ) :
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_functor_obj_map
(C : Type u)
[category_theory.category C]
(F : (simplex_category ⥤ C)ᵒᵖ)
(X Y : simplex_categoryᵒᵖ)
(f : X ⟶ Y) :
((category_theory.cosimplicial_simplicial_equiv C).functor.obj F).map f = ((opposite.unop F).map f.unop).op
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_unit_iso_inv_app
(C : Type u)
[category_theory.category C]
(X : (simplex_category ⥤ C)ᵒᵖ) :
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_inverse_obj
(C : Type u)
[category_theory.category C]
(F : simplex_categoryᵒᵖ ⥤ Cᵒᵖ) :
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_counit_iso_hom_app_app
(C : Type u)
[category_theory.category C]
(X : simplex_categoryᵒᵖ ⥤ Cᵒᵖ)
(X_1 : simplex_categoryᵒᵖ) :
((category_theory.cosimplicial_simplicial_equiv C).counit_iso.hom.app X).app X_1 = 𝟙 (X.obj X_1)
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_counit_iso_inv_app_app
(C : Type u)
[category_theory.category C]
(X : simplex_categoryᵒᵖ ⥤ Cᵒᵖ)
(X_1 : simplex_categoryᵒᵖ) :
((category_theory.cosimplicial_simplicial_equiv C).counit_iso.inv.app X).app X_1 = 𝟙 (X.obj X_1)
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_functor_map_app
(C : Type u)
[category_theory.category C]
(F G : (simplex_category ⥤ C)ᵒᵖ)
(α : F ⟶ G)
(X : simplex_categoryᵒᵖ) :
((category_theory.cosimplicial_simplicial_equiv C).functor.map α).app X = (α.unop.app (opposite.unop X)).op
@[simp]
theorem
category_theory.cosimplicial_simplicial_equiv_functor_obj_obj
(C : Type u)
[category_theory.category C]
(F : (simplex_category ⥤ C)ᵒᵖ)
(X : simplex_categoryᵒᵖ) :
((category_theory.cosimplicial_simplicial_equiv C).functor.obj F).obj X = opposite.op ((opposite.unop F).obj (opposite.unop X))
@[simp]
theorem
category_theory.simplicial_object.augmented.right_op_left
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C) :
X.right_op.left = opposite.op X.right
@[simp]
def
category_theory.simplicial_object.augmented.right_op
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C) :
Construct an augmented cosimplicial object in the opposite category from an augmented simplicial object.
Equations
- X.right_op = {left := opposite.op X.right, right := category_theory.functor.right_op X.left, hom := category_theory.nat_trans.right_op X.hom}
@[simp]
def
category_theory.cosimplicial_object.augmented.left_op
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object.augmented Cᵒᵖ) :
Construct an augmented simplicial object from an augmented cosimplicial object in the opposite category.
Equations
- X.left_op = {left := category_theory.functor.left_op X.right, right := opposite.unop X.left, hom := category_theory.nat_trans.left_op X.hom}
@[simp]
theorem
category_theory.cosimplicial_object.augmented.left_op_right
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object.augmented Cᵒᵖ) :
X.left_op.right = opposite.unop X.left
@[simp]
@[simp]
@[simp]
@[simp]
theorem
category_theory.simplicial_object.augmented.right_op_left_op_iso_inv_left_app
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C)
(X_1 : simplex_categoryᵒᵖ) :
@[simp]
def
category_theory.simplicial_object.augmented.right_op_left_op_iso
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C) :
Converting an augmented simplicial object to an augmented cosimplicial object and back is isomorphic to the given object.
@[simp]
theorem
category_theory.simplicial_object.augmented.right_op_left_op_iso_hom_left_app
{C : Type u}
[category_theory.category C]
(X : category_theory.simplicial_object.augmented C)
(X_1 : simplex_categoryᵒᵖ) :
@[simp]
@[simp]
def
category_theory.cosimplicial_object.augmented.left_op_right_op_iso
{C : Type u}
[category_theory.category C]
(X : category_theory.cosimplicial_object.augmented Cᵒᵖ) :
Converting an augmented cosimplicial object to an augmented simplicial object and back is isomorphic to the given object.
@[simp]
@[simp]
def
category_theory.simplicial_to_cosimplicial_augmented
(C : Type u)
[category_theory.category C] :
A functorial version of simplicial_object.augmented.right_op.
Equations
- category_theory.simplicial_to_cosimplicial_augmented C = {obj := λ (X : (category_theory.simplicial_object.augmented C)ᵒᵖ), (opposite.unop X).right_op, map := λ (X Y : (category_theory.simplicial_object.augmented C)ᵒᵖ) (f : X ⟶ Y), {left := f.unop.right.op, right := category_theory.nat_trans.right_op f.unop.left, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.simplicial_to_cosimplicial_augmented_map_left
(C : Type u)
[category_theory.category C]
(X Y : (category_theory.simplicial_object.augmented C)ᵒᵖ)
(f : X ⟶ Y) :
@[simp]
@[simp]
theorem
category_theory.simplicial_to_cosimplicial_augmented_map_right
(C : Type u)
[category_theory.category C]
(X Y : (category_theory.simplicial_object.augmented C)ᵒᵖ)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.cosimplicial_to_simplicial_augmented_map
(C : Type u)
[category_theory.category C]
(X Y : category_theory.cosimplicial_object.augmented Cᵒᵖ)
(f : X ⟶ Y) :
(category_theory.cosimplicial_to_simplicial_augmented C).map f = quiver.hom.op {left := category_theory.nat_trans.left_op f.right, right := f.left.unop, w' := _}
@[simp]
def
category_theory.cosimplicial_to_simplicial_augmented
(C : Type u)
[category_theory.category C] :
A functorial version of cosimplicial_object.augmented.left_op.
Equations
- category_theory.cosimplicial_to_simplicial_augmented C = {obj := λ (X : category_theory.cosimplicial_object.augmented Cᵒᵖ), opposite.op X.left_op, map := λ (X Y : category_theory.cosimplicial_object.augmented Cᵒᵖ) (f : X ⟶ Y), quiver.hom.op {left := category_theory.nat_trans.left_op f.right, right := f.left.unop, w' := _}, map_id' := _, map_comp' := _}
def
category_theory.simplicial_cosimplicial_augmented_equiv
(C : Type u)
[category_theory.category C] :
The contravariant categorical equivalence between augmented simplicial objects and augmented cosimplicial objects in the opposite category.
Equations
- category_theory.simplicial_cosimplicial_augmented_equiv C = category_theory.equivalence.mk (category_theory.simplicial_to_cosimplicial_augmented C) (category_theory.cosimplicial_to_simplicial_augmented C) (category_theory.nat_iso.of_components (λ (X : (category_theory.simplicial_object.augmented C)ᵒᵖ), (opposite.unop X).right_op_left_op_iso.op) _) (category_theory.nat_iso.of_components (λ (X : category_theory.cosimplicial_object.augmented Cᵒᵖ), X.left_op_right_op_iso) _)