The category of elements #
This file defines the category of elements, also known as (a special case of) the Grothendieck construction.
Given a functor F : C ⥤ Type, an object of F.Elements is a pair (X : C, x : F.obj X).
A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.
Implementation notes #
This construction is equivalent to a special case of a comma construction, so this is mostly just a
more convenient API. We prove the equivalence in
CategoryTheory.CategoryOfElements.structuredArrowEquivalence.
References #
- [Emily Riehl, Category Theory in Context, Section 2.4][riehl2017]
- https://en.wikipedia.org/wiki/Category_of_elements
- https://ncatlab.org/nlab/show/category+of+elements
Tags #
category of elements, Grothendieck construction, comma category
def
CategoryTheory.Functor.Elements
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
Type (max u w)
The type of objects for the category of elements of a functor F : C ⥤ Type
is a pair (X : C, x : F.obj X).
Equations
- F.Elements = ((c : C) × F.obj c)
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Functor.elementsMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
(X : C)
(x : F.obj X)
:
F.Elements
Constructor for the type F.Elements when F is a functor to types.
Equations
- F.elementsMk X x = ⟨X, x⟩
Instances For
theorem
CategoryTheory.Functor.Elements.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
(x : F.Elements)
(y : F.Elements)
(h₁ : x.fst = y.fst)
(h₂ : F.map (CategoryTheory.eqToHom h₁) x.snd = y.snd)
:
x = y
instance
CategoryTheory.categoryOfElements
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
CategoryTheory.Category.{v, max u w} F.Elements
The category structure on F.Elements, for F : C ⥤ Type.
A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.
Equations
@[simp]
theorem
CategoryTheory.NatTrans.mapElements_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{G : CategoryTheory.Functor C (Type w)}
(φ : F ⟶ G)
:
∀ (x : F.Elements),
(CategoryTheory.NatTrans.mapElements φ).obj x = match x with
| ⟨X, x⟩ => ⟨X, φ.app X x⟩
@[simp]
theorem
CategoryTheory.NatTrans.mapElements_map_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{G : CategoryTheory.Functor C (Type w)}
(φ : F ⟶ G)
{p : F.Elements}
{q : F.Elements}
:
∀ (x : p ⟶ q), ↑((CategoryTheory.NatTrans.mapElements φ).map x) = ↑x
def
CategoryTheory.NatTrans.mapElements
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{G : CategoryTheory.Functor C (Type w)}
(φ : F ⟶ G)
:
CategoryTheory.Functor F.Elements G.Elements
Natural transformations are mapped to functors between category of elements
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.elementsFunctor_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
:
∀ {X Y : CategoryTheory.Functor C (Type w)} (n : X ⟶ Y),
CategoryTheory.Functor.elementsFunctor.map n = CategoryTheory.NatTrans.mapElements n
@[simp]
theorem
CategoryTheory.Functor.elementsFunctor_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
CategoryTheory.Functor.elementsFunctor.obj F = CategoryTheory.Cat.of F.Elements
The functor mapping functors C ⥤ Type w to their category of elements
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.homMk_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
(x : F.Elements)
(y : F.Elements)
(f : x.fst ⟶ y.fst)
(hf : F.map f x.snd = y.snd)
:
↑(CategoryTheory.CategoryOfElements.homMk x y f hf) = f
def
CategoryTheory.CategoryOfElements.homMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
(x : F.Elements)
(y : F.Elements)
(f : x.fst ⟶ y.fst)
(hf : F.map f x.snd = y.snd)
:
x ⟶ y
Constructor for morphisms in the category of elements of a functor to types.
Equations
- CategoryTheory.CategoryOfElements.homMk x y f hf = ⟨f, hf⟩
Instances For
theorem
CategoryTheory.CategoryOfElements.ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{x : F.Elements}
{y : F.Elements}
{f : x ⟶ y}
{g : x ⟶ y}
:
theorem
CategoryTheory.CategoryOfElements.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
{x : F.Elements}
{y : F.Elements}
(f : x ⟶ y)
(g : x ⟶ y)
(w : ↑f = ↑g)
:
f = g
@[simp]
theorem
CategoryTheory.CategoryOfElements.comp_val
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{p : F.Elements}
{q : F.Elements}
{r : F.Elements}
{f : p ⟶ q}
{g : q ⟶ r}
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.id_val
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{p : F.Elements}
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.map_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
{p : F.Elements}
{q : F.Elements}
(f : p ⟶ q)
:
F.map (↑f) p.snd = q.snd
@[simp]
theorem
CategoryTheory.CategoryOfElements.isoMk_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
(x : F.Elements)
(y : F.Elements)
(e : x.fst ≅ y.fst)
(he : F.map e.hom x.snd = y.snd)
:
(CategoryTheory.CategoryOfElements.isoMk x y e he).inv = CategoryTheory.CategoryOfElements.homMk y x e.inv ⋯
@[simp]
theorem
CategoryTheory.CategoryOfElements.isoMk_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
(x : F.Elements)
(y : F.Elements)
(e : x.fst ≅ y.fst)
(he : F.map e.hom x.snd = y.snd)
:
(CategoryTheory.CategoryOfElements.isoMk x y e he).hom = CategoryTheory.CategoryOfElements.homMk x y e.hom he
def
CategoryTheory.CategoryOfElements.isoMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C (Type w)}
(x : F.Elements)
(y : F.Elements)
(e : x.fst ≅ y.fst)
(he : F.map e.hom x.snd = y.snd)
:
x ≅ y
Constructor for isomorphisms in the category of elements of a functor to types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.groupoidOfElements
{G : Type u}
[CategoryTheory.Groupoid G]
(F : CategoryTheory.Functor G (Type w))
:
CategoryTheory.Groupoid F.Elements
Equations
- CategoryTheory.groupoidOfElements F = CategoryTheory.Groupoid.mk (fun {p q : F.Elements} (f : p ⟶ q) => ⟨CategoryTheory.Groupoid.inv ↑f, ⋯⟩) ⋯ ⋯
@[simp]
theorem
CategoryTheory.CategoryOfElements.π_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
(X : F.Elements)
:
(CategoryTheory.CategoryOfElements.π F).obj X = X.fst
@[simp]
theorem
CategoryTheory.CategoryOfElements.π_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
∀ {X Y : F.Elements} (f : X ⟶ Y), (CategoryTheory.CategoryOfElements.π F).map f = ↑f
def
CategoryTheory.CategoryOfElements.π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
CategoryTheory.Functor F.Elements C
The functor out of the category of elements which forgets the element.
Equations
- CategoryTheory.CategoryOfElements.π F = { obj := fun (X : F.Elements) => X.fst, map := fun {X Y : F.Elements} (f : X ⟶ Y) => ↑f, map_id := ⋯, map_comp := ⋯ }
Instances For
instance
CategoryTheory.CategoryOfElements.instFaithfulElementsπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
(CategoryTheory.CategoryOfElements.π F).Faithful
Equations
- ⋯ = ⋯
instance
CategoryTheory.CategoryOfElements.instReflectsIsomorphismsElementsπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
(CategoryTheory.CategoryOfElements.π F).ReflectsIsomorphisms
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.CategoryOfElements.map_obj_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₁ : CategoryTheory.Functor C (Type w)}
{F₂ : CategoryTheory.Functor C (Type w)}
(α : F₁ ⟶ F₂)
(t : F₁.Elements)
:
((CategoryTheory.CategoryOfElements.map α).obj t).fst = t.fst
@[simp]
theorem
CategoryTheory.CategoryOfElements.map_obj_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₁ : CategoryTheory.Functor C (Type w)}
{F₂ : CategoryTheory.Functor C (Type w)}
(α : F₁ ⟶ F₂)
(t : F₁.Elements)
:
((CategoryTheory.CategoryOfElements.map α).obj t).snd = α.app t.fst t.snd
@[simp]
theorem
CategoryTheory.CategoryOfElements.map_map_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₁ : CategoryTheory.Functor C (Type w)}
{F₂ : CategoryTheory.Functor C (Type w)}
(α : F₁ ⟶ F₂)
{t₁ : F₁.Elements}
{t₂ : F₁.Elements}
(k : t₁ ⟶ t₂)
:
↑((CategoryTheory.CategoryOfElements.map α).map k) = ↑k
def
CategoryTheory.CategoryOfElements.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₁ : CategoryTheory.Functor C (Type w)}
{F₂ : CategoryTheory.Functor C (Type w)}
(α : F₁ ⟶ F₂)
:
CategoryTheory.Functor F₁.Elements F₂.Elements
A natural transformation between functors induces a functor between the categories of elements.
Equations
- CategoryTheory.CategoryOfElements.map α = { obj := fun (t : F₁.Elements) => ⟨t.fst, α.app t.fst t.snd⟩, map := fun {t₁ t₂ : F₁.Elements} (k : t₁ ⟶ t₂) => ⟨↑k, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.map_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₁ : CategoryTheory.Functor C (Type w)}
{F₂ : CategoryTheory.Functor C (Type w)}
(α : F₁ ⟶ F₂)
:
def
CategoryTheory.CategoryOfElements.toStructuredArrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
CategoryTheory.Functor F.Elements (CategoryTheory.StructuredArrow PUnit.{w + 1} F)
The forward direction of the equivalence F.Elements ≅ (*, F).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.toStructuredArrow_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
(X : F.Elements)
:
(CategoryTheory.CategoryOfElements.toStructuredArrow F).obj X = { left := { as := PUnit.unit }, right := X.fst,
hom := fun (x : (CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj { as := PUnit.unit }) => X.snd }
@[simp]
theorem
CategoryTheory.CategoryOfElements.to_comma_map_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
{X : F.Elements}
{Y : F.Elements}
(f : X ⟶ Y)
:
((CategoryTheory.CategoryOfElements.toStructuredArrow F).map f).right = ↑f
def
CategoryTheory.CategoryOfElements.fromStructuredArrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
CategoryTheory.Functor (CategoryTheory.StructuredArrow PUnit.{w + 1} F) F.Elements
The reverse direction of the equivalence F.Elements ≅ (*, F).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.fromStructuredArrow_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
(X : CategoryTheory.StructuredArrow PUnit.{w + 1} F)
:
(CategoryTheory.CategoryOfElements.fromStructuredArrow F).obj X = ⟨X.right, X.hom PUnit.unit⟩
@[simp]
theorem
CategoryTheory.CategoryOfElements.fromStructuredArrow_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
{X : CategoryTheory.StructuredArrow PUnit.{w + 1} F}
{Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F}
(f : X ⟶ Y)
:
(CategoryTheory.CategoryOfElements.fromStructuredArrow F).map f = ⟨f.right, ⋯⟩
@[simp]
@[simp]
theorem
CategoryTheory.CategoryOfElements.structuredArrowEquivalence_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
(CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id F.Elements)
@[simp]
def
CategoryTheory.CategoryOfElements.structuredArrowEquivalence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C (Type w))
:
F.Elements ≌ CategoryTheory.StructuredArrow PUnit.{w + 1} F
The equivalence between the category of elements F.Elements
and the comma category (*, F).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.toCostructuredArrow_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
∀ {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y),
(CategoryTheory.CategoryOfElements.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk (↑f.unop).unop ⋯
@[simp]
theorem
CategoryTheory.CategoryOfElements.toCostructuredArrow_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : F.Elementsᵒᵖ)
:
(CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm (Opposite.unop X).snd)
def
CategoryTheory.CategoryOfElements.toCostructuredArrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
CategoryTheory.Functor F.Elementsᵒᵖ (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
The forward direction of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F),
given by CategoryTheory.yonedaEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ)
:
((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj X).snd = CategoryTheory.yonedaEquiv.toFun (Opposite.unop X).hom
@[simp]
theorem
CategoryTheory.CategoryOfElements.fromCostructuredArrow_map_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
{X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ}
{Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ}
(f : X ⟶ Y)
:
↑((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).map f) = f.unop.left.op
@[simp]
theorem
CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ)
:
((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj X).fst = Opposite.op (Opposite.unop X).left
def
CategoryTheory.CategoryOfElements.fromCostructuredArrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ F.Elements
The reverse direction of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F),
given by CategoryTheory.yonedaEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
{X : C}
(f : CategoryTheory.yoneda.obj X ⟶ F)
:
(CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj (Opposite.op (CategoryTheory.CostructuredArrow.mk f)) = ⟨Opposite.op X, CategoryTheory.yonedaEquiv.toFun f⟩
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso = CategoryTheory.NatIso.ofComponents
(fun (X : F.Elementsᵒᵖ) =>
(CategoryTheory.CategoryOfElements.isoMk
((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
(Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X)))
(Opposite.unop X)
(CategoryTheory.Iso.refl
((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
(Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X))).fst)
⋯).op)
⋯
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_inverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso = CategoryTheory.NatIso.ofComponents
(fun (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F) =>
CategoryTheory.CostructuredArrow.isoMk
(CategoryTheory.Iso.refl
(((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.comp
(CategoryTheory.CategoryOfElements.toCostructuredArrow F)).obj
X).left)
⋯)
⋯
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_functor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
def
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
F.Elementsᵒᵖ ≌ CategoryTheory.CostructuredArrow CategoryTheory.yoneda F
The equivalence F.Elementsᵒᵖ ≅ (yoneda, F) given by yoneda lemma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₁ : CategoryTheory.Functor Cᵒᵖ (Type v)}
{F₂ : CategoryTheory.Functor Cᵒᵖ (Type v)}
(α : F₁ ⟶ F₂)
:
The equivalence (-.Elements)ᵒᵖ ≅ (yoneda, -) of is actually a natural isomorphism of functors.
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : F.Elementsᵒᵖ)
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : F.Elementsᵒᵖ)
:
def
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).functor.comp
(CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda F) ≅ (CategoryTheory.CategoryOfElements.π F).leftOp
The equivalence F.elementsᵒᵖ ≌ (yoneda, F) is compatible with the forgetful functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_hom_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ_inv_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
(X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)
:
def
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor Cᵒᵖ (Type v))
:
(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse.comp
(CategoryTheory.CategoryOfElements.π F).leftOp ≅ CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda F
The equivalence F.elementsᵒᵖ ≌ (yoneda, F) is compatible with the forgetful functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Functor.Elements.initial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
:
(CategoryTheory.yoneda.obj A).Elements
The initial object in the category of elements for a representable functor. In isInitial it is
shown that this is initial.
Equations
Instances For
def
CategoryTheory.Functor.Elements.isInitial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
:
Show that Elements.initial A is initial in the category of elements for the yoneda functor.
Equations
- One or more equations did not get rendered due to their size.