def CategoryTheory.SimplicialCategory.coneNatTrans {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] {A : SSet} {AX : K} {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) : Type

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

theorem CategoryTheory.SimplicialCategory.IsCotensor.uniq {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] {A : SSet} {X : K} {AX : K} {cone : A ⟶ CategoryTheory.SimplicialCategory.sHom AX X} (self : CategoryTheory.SimplicialCategory.IsCotensor AX cone) (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

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

HasCotensor F represents the mere existence of a simplicial cotensor.

• mk' :: (
• exists_cotensor : Nonempty (CategoryTheory.SimplicialCategory.CotensorCone A X)

  There is some limit cone for F

• )

theorem CategoryTheory.SimplicialCategory.HasCotensor.exists_cotensor {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] {A : SSet} {X : K} [self : CategoryTheory.SimplicialCategory.HasCotensor A X] : Nonempty (CategoryTheory.SimplicialCategory.CotensorCone A X)

There is some limit cone for F

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

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

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

Equations

• CategoryTheory.SimplicialCategory.getCotensorCone A X = Classical.choice ⋯

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 : ∀ (A : SSet) (X : K), CategoryTheory.SimplicialCategory.HasCotensor A X

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

theorem CategoryTheory.SimplicialCategory.HasCotensors.has_cotensors {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] [self : CategoryTheory.SimplicialCategory.HasCotensors K] (A : SSet) (X : K) : CategoryTheory.SimplicialCategory.HasCotensor A X

All A : SSet and X : 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] (A : SSet) (X : K) : CategoryTheory.SimplicialCategory.HasCotensor A X

Equations

• ⋯ = ⋯

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

An arbitrary choice of cotensor obj.

Equations

• A ⋔ X = (CategoryTheory.SimplicialCategory.getCotensorCone A X).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] (A : SSet) (X : K) [CategoryTheory.SimplicialCategory.HasCotensor A X] : A ⟶ CategoryTheory.SimplicialCategory.sHom (A ⋔ X) X

The associated cotensor cone.

Equations

• CategoryTheory.SimplicialCategory.cotensor.cone A X = (CategoryTheory.SimplicialCategory.getCotensorCone A X).cone

def CategoryTheory.SimplicialCategory.cotensor.is_cotensor {K : Type u} [CategoryTheory.Category.{v, u} K] [CategoryTheory.SimplicialCategory K] (A : SSet) (X : K) [CategoryTheory.SimplicialCategory.HasCotensor A X] : CategoryTheory.SimplicialCategory.IsCotensor (A ⋔ X) (CategoryTheory.SimplicialCategory.cotensor.cone A X)

The universal property of this cone.

Equations

• CategoryTheory.SimplicialCategory.cotensor.is_cotensor A X = (CategoryTheory.SimplicialCategory.getCotensorCone A X).is_cotensor

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

Equations

• CategoryTheory.SimplicialCategory.cotensor.iso A X Y = CategoryTheory.asIso (CategoryTheory.SimplicialCategory.coneNatTrans Y (CategoryTheory.SimplicialCategory.cotensor.cone A X))

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

Equations

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

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

Equations

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

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

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] {A : SSet} {B : SSet} (i : A ⟶ B) {X : K} {Y : K} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialCategory.cotensorCovMap B f) (CategoryTheory.SimplicialCategory.cotensorContraMap i Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialCategory.cotensorContraMap i X) (CategoryTheory.SimplicialCategory.cotensorCovMap A f)