@[reducible, inline]

abbrev CategoryTheory.SimplicialCategory.Cotensor {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] {U : SSet} {A B : K} (ua : CategoryTheory.SimplicialCategory.Cotensor U A) (ub : CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] {U V : SSet} {A : K} (ua : CategoryTheory.SimplicialCategory.Cotensor U A) (va : CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] {U : SSet} {A B : K} (ua : CategoryTheory.SimplicialCategory.Cotensor U A) (ub : CategoryTheory.SimplicialCategory.Cotensor U B) (f : A ⟶ B) : (CategoryTheory.eHomEquiv SSet) (CategoryTheory.SimplicialCategory.cotensorPostcompose ua ub f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv SSet) f) (CategoryTheory.Enriched.Cotensor.postcompose SSet ua ub)

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

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

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

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

• mk' :: (
• exists_cotensor : Nonempty (CategoryTheory.SimplicialCategory.Cotensor U A)

  There is some cotensor.

• )

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

noncomputable def CategoryTheory.SimplicialCategory.getCotensor {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (U : SSet) (A : K) [CategoryTheory.SimplicialCategory.HasCotensor U A] : CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (U : SSet) (A : K) [CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (U : SSet) (A : K) [CategoryTheory.SimplicialCategory.HasCotensor U A] : U ⟶ CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (U : SSet) (A : K) [CategoryTheory.SimplicialCategory.HasCotensor U A] : CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (U : SSet) (A : K) [CategoryTheory.SimplicialCategory.HasCotensor U A] (X : K) : CategoryTheory.SimplicialCategory.sHom X (U ⋔ A) ≅ (CategoryTheory.ihom U).obj (CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (U : SSet) (A : K) [CategoryTheory.SimplicialCategory.HasCotensor U A] (X : K) : (X ⟶ U ⋔ A) ≃ (U ⟶ CategoryTheory.SimplicialCategory.sHom X A)

Equations

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

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

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

• has_cotensors : ∀ (U : SSet) (A : K), CategoryTheory.SimplicialCategory.HasCotensor U A

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

@[instance 100]

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.SimplicialCategory.cotensorCovMap {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] [CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] [CategoryTheory.SimplicialCategory.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} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] [CategoryTheory.SimplicialCategory.HasCotensors K] {U V : SSet} (i : U ⟶ V) {A B : K} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialCategory.cotensorCovMap V f) (CategoryTheory.SimplicialCategory.cotensorContraMap i B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialCategory.cotensorContraMap i A) (CategoryTheory.SimplicialCategory.cotensorCovMap U f)

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

Equations

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

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

• uniq : ∀ (Y : K), CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.coneNatTrans Y cone)

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

• obj : K

  The object

• cone : A ⟶ CategoryTheory.SimplicialCategory.sHom self.obj X

  The cone itself

• is_cotensor : CategoryTheory.SimplicialCategory.IsCotensor self.obj self.cone

  The universal property of the limit cone