@[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

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.

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 ⋯

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.

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

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

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.

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.

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.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