@[reducible, inline]

abbrev CategoryTheory.SimplicialCategory.Cotensor {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) : Type (max v u)

A specialization of the enriched category cotensor.

Equations

• CategoryTheory.SimplicialCategory.Cotensor U A = CategoryTheory.Enriched.Cotensor U A

noncomputable def CategoryTheory.SimplicialCategory.cotensorPostcompose {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} {A B : K} (ua : Cotensor U A) (ub : Cotensor U B) (f : A ⟶ B) : ua.obj ⟶ ub.obj

Equations

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

noncomputable def CategoryTheory.SimplicialCategory.cotensorPrecompose {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U V : SSet} {A : K} (ua : Cotensor U A) (va : Cotensor V A) (i : U ⟶ V) : va.obj ⟶ ua.obj

Equations

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

theorem CategoryTheory.SimplicialCategory.cotensorPostcompose_homEquiv {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} {A B : K} (ua : Cotensor U A) (ub : Cotensor U B) (f : A ⟶ B) : (eHomEquiv SSet) (cotensorPostcompose ua ub f) = CategoryStruct.comp ((eHomEquiv SSet) f) (Enriched.Cotensor.postcompose SSet ua ub)

theorem CategoryTheory.SimplicialCategory.cotensorPrecompose_homEquiv {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U V : SSet} {A : K} (ua : Cotensor U A) (va : Cotensor V A) (i : U ⟶ V) : (eHomEquiv SSet) (cotensorPrecompose ua va i) = CategoryStruct.comp ((eHomEquiv SSet) i) (Enriched.Cotensor.EhomPrecompose SSet ua va)

theorem CategoryTheory.SimplicialCategory.cotensor_local_bifunctoriality {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U V : SSet} {A B : K} (ua : Cotensor U A) (ub : Cotensor U B) (va : Cotensor V A) (vb : Cotensor V B) (i : U ⟶ V) (f : A ⟶ B) : CategoryStruct.comp (cotensorPrecompose ua va i) (cotensorPostcompose ua ub f) = CategoryStruct.comp (cotensorPostcompose va vb f) (cotensorPrecompose ub vb i)

class CategoryTheory.SimplicialCategory.HasCotensor {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) : Prop

HasCotensor U A represents the mere existence of a simplicial cotensor.

• mk' :: (
• exists_cotensor : Nonempty (Cotensor U A)

  There is some cotensor.

• )

theorem CategoryTheory.SimplicialCategory.HasCotensor.mk {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} {A : K} (c : Cotensor U A) : HasCotensor U A

noncomputable def CategoryTheory.SimplicialCategory.getCotensor {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) [HasCotensor U A] : Cotensor U A

Use the axiom of choice to extract explicit CotensorCone A X from HasCotensor A X.

Equations

• CategoryTheory.SimplicialCategory.getCotensor U A = Classical.choice ⋯

noncomputable def CategoryTheory.SimplicialCategory.cotensor.obj {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) [HasCotensor U A] : K

An arbitrary choice of cotensor obj.

Equations

• U ⋔ A = (CategoryTheory.SimplicialCategory.getCotensor U A).obj

def CategoryTheory.SimplicialCategory.«term_⋔_» : Lean.TrailingParserDescr

Equations

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

noncomputable def CategoryTheory.SimplicialCategory.cotensor.cone {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) [HasCotensor U A] : U ⟶ sHom (U ⋔ A) A

The associated cotensor cone.

Equations

• CategoryTheory.SimplicialCategory.cotensor.cone U A = (CategoryTheory.SimplicialCategory.getCotensor U A).cone

noncomputable def CategoryTheory.SimplicialCategory.cotensor.is_cotensor {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) [HasCotensor U A] : Cotensor U A

The universal property of this cone.

Equations

• CategoryTheory.SimplicialCategory.cotensor.is_cotensor U A = CategoryTheory.SimplicialCategory.getCotensor U A

noncomputable def CategoryTheory.SimplicialCategory.cotensor.iso {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) [HasCotensor U A] (X : K) : sHom X (U ⋔ A) ≅ (ihom U).obj (sHom X A)

The natural isomorphism induced by a cotensor.

Equations

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

noncomputable def CategoryTheory.SimplicialCategory.cotensor.iso.underlying {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A : K) [HasCotensor U A] (X : K) : (X ⟶ U ⋔ A) ≃ (U ⟶ sHom X A)

Equations

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

theorem CategoryTheory.SimplicialCategory.homEquiv'_comp {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {X Y Z : K} (f : X ⟶ Y) (g : Y ⟶ Z) : (homEquiv' X Z) (CategoryStruct.comp f g) = (ConcreteCategory.hom ((sHomWhiskerRight f Z).app (Opposite.op { len := 0 }))) ((homEquiv' Y Z) g)

Ordinary composition, transported to zero-simplices of the enriched hom.

theorem CategoryTheory.SimplicialCategory.eHomEquiv_comp_eHomWhiskerRight {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {X Y Z : K} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryStruct.comp ((eHomEquiv SSet) g) (eHomWhiskerRight SSet f Z) = (eHomEquiv SSet) (CategoryStruct.comp f g)

Ordinary composition in the right variable, transported to enriched morphisms.

theorem CategoryTheory.SimplicialCategory.homEquiv'_id {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (X : K) : (homEquiv' X X) (CategoryStruct.id X) = (ConcreteCategory.hom ((eId SSet X).app (Opposite.op { len := 0 }))) PUnit.unit

The identity morphism, transported to zero-simplices of the enriched hom.

theorem CategoryTheory.SimplicialCategory.cotensor_underlying_homEquiv {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (U : SSet) (A X : K) [HasCotensor U A] (h : X ⟶ U ⋔ A) : (homEquiv' U (sHom X A)) ((cotensor.iso.underlying U A X) h) = (ConcreteCategory.hom (((evaluation SimplexCategoryᵒᵖ (Type v)).obj (Opposite.op { len := 0 })).map (cotensor.iso U A X).hom)) ((homEquiv' X (U ⋔ A)) h)

The zero-simplex form of cotensor.iso.underlying.

theorem CategoryTheory.SimplicialCategory.homEquiv'_comp_sset_ihom {U V W : SSet} (i : U ⟶ V) (f : V ⟶ W) : (homEquiv' U W) (CategoryStruct.comp i f) = (ConcreteCategory.hom ((CategoryStruct.comp ((eHomEquiv SSet) i) ((ihom U).map f)).app (Opposite.op { len := 0 }))) PUnit.unit

Composition in SSet, expressed through the closed structure.

theorem CategoryTheory.SimplicialCategory.cotensor_coneNatTrans_naturality_left {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} {A X Y : K} (ux : Cotensor U A) (h : X ⟶ Y) : CategoryStruct.comp (eHomWhiskerRight SSet h ux.obj) (ux.coneNatTrans X) = CategoryStruct.comp (ux.coneNatTrans Y) ((ihom U).map (eHomWhiskerRight SSet h A))

Naturality of a cotensor cone in the representing object.

theorem CategoryTheory.SimplicialCategory.cotensor_coneNatTrans_eId {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} {A : K} (ux : Cotensor U A) : CategoryStruct.comp (eId SSet ux.obj) (ux.coneNatTrans ux.obj) = MonoidalClosed.curry' ux.cone

Evaluating a cotensor cone at the identity of its representing object recovers the cone.

theorem CategoryTheory.SimplicialCategory.cotensor_coneNatTrans_id {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} (A : K) [HasCotensor U A] : (ConcreteCategory.hom (((getCotensor U A).coneNatTrans (U ⋔ A)).app (Opposite.op { len := 0 }))) ((homEquiv' (U ⋔ A) (U ⋔ A)) (CategoryStruct.id (U ⋔ A))) = (homEquiv' U (sHom (U ⋔ A) A)) (getCotensor U A).cone

The zero-simplex form of cotensor_coneNatTrans_eId.

theorem CategoryTheory.SimplicialCategory.cotensor_iso_underlying_eq_cone {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {U : SSet} (A X : K) [HasCotensor U A] (h : X ⟶ U ⋔ A) : (cotensor.iso.underlying U A X) h = CategoryStruct.comp (getCotensor U A).cone (eHomWhiskerRight SSet h A)

The underlying map of a cotensor isomorphism is represented by the chosen cotensor cone.

class CategoryTheory.SimplicialCategory.HasCotensors (K : Type u) [Category.{v, u} K] [SimplicialCategory K] : Prop

K has simplicial cotensors when cotensors with any simplicial set exist.

• has_cotensors (U : SSet) (A : K) : HasCotensor U A

  All U : SSet and A : K have a cotensor.

@[instance 100]

instance CategoryTheory.SimplicialCategory.hasCotensorsOfHasCotensors {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] (U : SSet) (A : K) : HasCotensor U A

noncomputable def CategoryTheory.SimplicialCategory.cotensorCovMap {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] (U : SSet) {A B : K} (f : A ⟶ B) : U ⋔ A ⟶ U ⋔ B

Equations

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

noncomputable def CategoryTheory.SimplicialCategory.cotensorContraMap {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] {U V : SSet} (i : U ⟶ V) (A : K) : V ⋔ A ⟶ U ⋔ A

Equations

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

theorem CategoryTheory.SimplicialCategory.homEquiv'_cotensorContraMap {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] {U V : SSet} (i : U ⟶ V) (A : K) : (homEquiv' (V ⋔ A) (U ⋔ A)) (cotensorContraMap i A) = (ConcreteCategory.hom ((CategoryStruct.comp ((eHomEquiv SSet) i) (Enriched.Cotensor.EhomPrecompose SSet (getCotensor U A) (getCotensor V A))).app (Opposite.op { len := 0 }))) PUnit.unit

The zero-simplex corresponding to a contravariant cotensor map.

theorem CategoryTheory.SimplicialCategory.cotensor_contraMap_cone {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] {U V : SSet} (i : U ⟶ V) (A : K) : CategoryStruct.comp (getCotensor U A).cone (eHomWhiskerRight SSet (cotensorContraMap i A) A) = CategoryStruct.comp i (getCotensor V A).cone

The chosen cotensor cone is natural with respect to contravariant cotensor maps.

theorem CategoryTheory.SimplicialCategory.cotensor_iso_underlying_precompose {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] {U V : SSet} (i : U ⟶ V) (A X : K) (g : X ⟶ V ⋔ A) : (cotensor.iso.underlying U A X) (CategoryStruct.comp g (cotensorContraMap i A)) = CategoryStruct.comp i ((cotensor.iso.underlying V A X) g)

Naturality of cotensor.iso.underlying under precomposition in the simplicial-set variable.

theorem CategoryTheory.SimplicialCategory.cotensor_bifunctoriality {K : Type u} [Category.{v, u} K] [SimplicialCategory K] [HasCotensors K] {U V : SSet} (i : U ⟶ V) {A B : K} (f : A ⟶ B) : CategoryStruct.comp (cotensorContraMap i A) (cotensorCovMap U f) = CategoryStruct.comp (cotensorCovMap V f) (cotensorContraMap i B)

def CategoryTheory.SimplicialCategory.coneNatTrans {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {A : SSet} {AX X : K} (Y : K) (cone : A ⟶ sHom AX X) : sHom Y AX ⟶ (ihom A).obj (sHom Y X)

Equations

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

structure CategoryTheory.SimplicialCategory.IsCotensor {K : Type u} [Category.{v, u} K] [SimplicialCategory K] {A : SSet} {X : K} (AX : K) (cone : A ⟶ sHom AX X) : Prop

• uniq (Y : K) : IsIso (coneNatTrans Y cone)

structure CategoryTheory.SimplicialCategory.CotensorCone {K : Type u} [Category.{v, u} K] [SimplicialCategory K] (A : SSet) (X : K) : Type (max u v)

• obj : K

  The object

• cone : A ⟶ sHom self.obj X

  The cone itself

• is_cotensor : IsCotensor self.obj self.cone

  The universal property of the limit cone