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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
- uniq : ∀ (Y : K), CategoryTheory.IsIso (CategoryTheory.SimplicialCategory.coneNatTrans Y cone)
Instances For
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)
:
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
Instances For
theorem
CategoryTheory.SimplicialCategory.CotensorCone.is_cotensor
{K : Type u}
[CategoryTheory.Category.{v, u} K]
[CategoryTheory.SimplicialCategory K]
{A : SSet}
{X : K}
(self : CategoryTheory.SimplicialCategory.CotensorCone A X)
:
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)
:
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
- )
Instances
theorem
CategoryTheory.SimplicialCategory.HasCotensor.exists_cotensor
{K : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} K} {inst_1 : 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)
:
def
CategoryTheory.SimplicialCategory.getCotensorCone
{K : Type u}
[CategoryTheory.Category.{v, u} K]
[CategoryTheory.SimplicialCategory K]
(A : SSet)
(X : K)
[CategoryTheory.SimplicialCategory.HasCotensor A X]
:
Use the axiom of choice to extract explicit CotensorCone A X
from HasCotensor A X
.
Equations
Instances For
class
CategoryTheory.SimplicialCategory.HasCotensors
(K : Type u)
[CategoryTheory.Category.{v, u} K]
[CategoryTheory.SimplicialCategory K]
:
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
andX : K
have a cotensor.
Instances
theorem
CategoryTheory.SimplicialCategory.HasCotensors.has_cotensors
{K : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} K} {inst_1 : 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)
:
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
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]
:
The universal property of this cone.
Equations
- ⋯ = ⋯
Instances For
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
Instances For
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.
Instances For
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
: