InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Cotensors

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

source

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.

source

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.

source

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)

source

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)

source

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)

source

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.

)

Instances

CategoryTheory.SimplicialCategory.hasCotensorsOfHasCotensors

source

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

source

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 ⋯

source

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

An arbitrary choice of cotensor obj.

Equations

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

source

def CategoryTheory.SimplicialCategory.«term_⋔_» :

Lean.TrailingParserDescr

Equations

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

source

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

source

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

source

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.

source

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.

source

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.

Instances

source

@[instance 100]

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

HasCotensor U A

source

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.

source

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.

source

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)

source

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.

source

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)

source

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