theorem CategoryTheory.Cat.id_eq_id (X : CategoryTheory.Cat) : CategoryTheory.CategoryStruct.id X = CategoryTheory.Functor.id ↑X

theorem CategoryTheory.Cat.comp_eq_comp {X : CategoryTheory.Cat} {Y : CategoryTheory.Cat} {Z : CategoryTheory.Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp F G = CategoryTheory.Functor.comp F G

@[simp]

theorem CategoryTheory.Cat.of_α (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : ↑(CategoryTheory.Cat.of C) = C

theorem CategoryTheory.Quiv.id_eq_id (X : CategoryTheory.Quiv) : CategoryTheory.CategoryStruct.id X = 𝟭q ↑X

theorem CategoryTheory.Quiv.comp_eq_comp {X : CategoryTheory.Quiv} {Y : CategoryTheory.Quiv} {Z : CategoryTheory.Quiv} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp F G = F ⋙q G

theorem CategoryTheory.conj_eqToHom_iff_heq' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom h')) ↔ HEq f g

theorem CategoryTheory.eqToHom_comp_heq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} (f : Y ⟶ X) (h : W = Y) : HEq (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) f

@[simp]

theorem CategoryTheory.eqToHom_comp_heq_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) : HEq (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) g ↔ HEq f g

@[simp]

theorem CategoryTheory.heq_eqToHom_comp_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) : HEq g (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) ↔ HEq g f

theorem CategoryTheory.comp_eqToHom_heq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (h : Y = Z) : HEq (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) f

@[simp]

theorem CategoryTheory.comp_eqToHom_heq_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) : HEq (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) g ↔ HEq f g

@[simp]

theorem CategoryTheory.heq_comp_eqToHom_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W : C} {X : C} {Y : C} {Z : C} {Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) : HEq g (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) ↔ HEq g f

theorem CategoryTheory.heq_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'} (eq1 : X = X') (eq2 : Y = Y') (eq3 : Z = Z') (H1 : HEq f f') (H2 : HEq g g') : HEq (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g')

theorem CategoryTheory.Quotient.CompClosure.congruence {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r : HomRel C) : CategoryTheory.Congruence fun (a b : C) => Relation.EqvGen (CategoryTheory.Quotient.CompClosure r)

class CategoryTheory.ReflQuiver (obj : Type u) extends Quiver : Type (max u v)

• Hom : obj → obj → Sort v
• id : (X : obj) → X ⟶ X

  The identity morphism on an object.

def CategoryTheory.«term𝟙rq» : Lean.ParserDescr

Notation for the identity morphism in a category.

Equations

• CategoryTheory.«term𝟙rq» = Lean.ParserDescr.node `CategoryTheory.term𝟙rq 1024 (Lean.ParserDescr.symbol "𝟙rq")

instance CategoryTheory.catToReflQuiver {C : Type u} [inst : CategoryTheory.Category.{v, u} C] : CategoryTheory.ReflQuiver.{v + 1, u} C

Equations

• CategoryTheory.catToReflQuiver = CategoryTheory.ReflQuiver.mk CategoryTheory.CategoryStruct.id

@[simp]

theorem CategoryTheory.ReflQuiver.id_eq_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : CategoryTheory.ReflQuiver.id X = CategoryTheory.CategoryStruct.id X

structure CategoryTheory.ReflPrefunctor (V : Type u₁) [CategoryTheory.ReflQuiver.{v₁, u₁} V] (W : Type u₂) [CategoryTheory.ReflQuiver.{v₂, u₂} W] extends Prefunctor : Sort (max (max (max (u₁ + 1) (u₂ + 1)) v₁) v₂)

A morphism of quivers. As we will later have categorical functors extend this structure, we call it a Prefunctor.

• obj : V → W
• map : {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id : ∀ (X : V), self.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (self.obj X)

  A functor preserves identity morphisms.

theorem CategoryTheory.ReflPrefunctor.map_id {V : Type u₁} [CategoryTheory.ReflQuiver.{v₁, u₁} V] {W : Type u₂} [CategoryTheory.ReflQuiver.{v₂, u₂} W] (self : V ⥤rq W) (X : V) : self.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (self.obj X)

A functor preserves identity morphisms.

theorem CategoryTheory.ReflPrefunctor.mk_obj {V : Type u_1} {W : Type u_2} [CategoryTheory.ReflQuiver.{u_3, u_1} V] [CategoryTheory.ReflQuiver.{u_4, u_2} W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X : V} : { obj := obj, map := map }.obj X = obj X

theorem CategoryTheory.ReflPrefunctor.mk_map {V : Type u_1} {W : Type u_2} [CategoryTheory.ReflQuiver.{u_3, u_1} V] [CategoryTheory.ReflQuiver.{u_4, u_2} W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X : V} {Y : V} {f : X ⟶ Y} : { obj := obj, map := map }.map f = map f

theorem CategoryTheory.ReflPrefunctor.ext {V : Type u} [CategoryTheory.ReflQuiver.{v₁, u} V] {W : Type u₂} [CategoryTheory.ReflQuiver.{v₂, u₂} W] {F : V ⥤rq W} {G : V ⥤rq W} (h_obj : ∀ (X : V), F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) : F = G

@[simp]

theorem CategoryTheory.ReflPrefunctor.id_obj (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2, u_1} V] (X : V) : (𝟭rq V).obj X = X

@[simp]

theorem CategoryTheory.ReflPrefunctor.id_map (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2, u_1} V] : ∀ {X Y : V} (f : X ⟶ Y), (𝟭rq V).map f = f

def CategoryTheory.ReflPrefunctor.id (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2, u_1} V] : V ⥤rq V

The identity morphism between quivers.

Equations

• 𝟭rq V = { toPrefunctor := 𝟭q V, map_id := ⋯ }

instance CategoryTheory.ReflPrefunctor.instInhabited (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2, u_1} V] : Inhabited (V ⥤rq V)

Equations

• CategoryTheory.ReflPrefunctor.instInhabited V = { default := 𝟭rq V }

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_map {U : Type u_1} [CategoryTheory.ReflQuiver.{u_4, u_1} U] {V : Type u_2} [CategoryTheory.ReflQuiver.{u_5, u_2} V] {W : Type u_3} [CategoryTheory.ReflQuiver.{u_6, u_3} W] (F : U ⥤rq V) (G : V ⥤rq W) : ∀ {X Y : U} (f : X ⟶ Y), (F ⋙rq G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_obj {U : Type u_1} [CategoryTheory.ReflQuiver.{u_4, u_1} U] {V : Type u_2} [CategoryTheory.ReflQuiver.{u_5, u_2} V] {W : Type u_3} [CategoryTheory.ReflQuiver.{u_6, u_3} W] (F : U ⥤rq V) (G : V ⥤rq W) (X : U) : (F ⋙rq G).obj X = G.obj (F.obj X)

def CategoryTheory.ReflPrefunctor.comp {U : Type u_1} [CategoryTheory.ReflQuiver.{u_4, u_1} U] {V : Type u_2} [CategoryTheory.ReflQuiver.{u_5, u_2} V] {W : Type u_3} [CategoryTheory.ReflQuiver.{u_6, u_3} W] (F : U ⥤rq V) (G : V ⥤rq W) : U ⥤rq W

Composition of morphisms between quivers.

Equations

• F ⋙rq G = { toPrefunctor := F.toPrefunctor ⋙q G.toPrefunctor, map_id := ⋯ }

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_id {U : Type u_1} {V : Type u_2} [CategoryTheory.ReflQuiver.{u_3, u_1} U] [CategoryTheory.ReflQuiver.{u_4, u_2} V] (F : U ⥤rq V) : F ⋙rq 𝟭rq V = F

@[simp]

theorem CategoryTheory.ReflPrefunctor.id_comp {U : Type u_1} {V : Type u_2} [CategoryTheory.ReflQuiver.{u_3, u_1} U] [CategoryTheory.ReflQuiver.{u_4, u_2} V] (F : U ⥤rq V) : 𝟭rq U ⋙rq F = F

@[simp]

theorem CategoryTheory.ReflPrefunctor.comp_assoc {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [CategoryTheory.ReflQuiver.{u_5, u_1} U] [CategoryTheory.ReflQuiver.{u_6, u_2} V] [CategoryTheory.ReflQuiver.{u_7, u_3} W] [CategoryTheory.ReflQuiver.{u_8, u_4} Z] (F : U ⥤rq V) (G : V ⥤rq W) (H : W ⥤rq Z) : F ⋙rq G ⋙rq H = F ⋙rq (G ⋙rq H)

def CategoryTheory.ReflPrefunctor.«term_⥤rq_» : Lean.TrailingParserDescr

Notation for a prefunctor between quivers.

Equations

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

def CategoryTheory.ReflPrefunctor.«term_⋙rq_» : Lean.TrailingParserDescr

Notation for composition of prefunctors.

Equations

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

def CategoryTheory.ReflPrefunctor.«term𝟭rq» : Lean.ParserDescr

Notation for the identity prefunctor on a quiver.

Equations

• CategoryTheory.ReflPrefunctor.«term𝟭rq» = Lean.ParserDescr.node `CategoryTheory.ReflPrefunctor.term𝟭rq 1024 (Lean.ParserDescr.symbol "𝟭rq")

theorem CategoryTheory.ReflPrefunctor.congr_map {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X : U} {Y : U} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) : F.map f = F.map g

def CategoryTheory.Functor.toReflPrefunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) : C ⥤rq D

Equations

• F.toReflPrefunctor = { toPrefunctor := F.toPrefunctor, map_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.toReflPrefunctor_toPrefunctor {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑C ↑D) : F.toReflPrefunctor.toPrefunctor = F.toPrefunctor

instance CategoryTheory.ReflQuiver.opposite {V : Type u_1} [CategoryTheory.ReflQuiver.{u_2, u_1} V] : CategoryTheory.ReflQuiver.{max 1 u_2, u_1} Vᵒᵖ

Vᵒᵖ reverses the direction of all arrows of V.

Equations

• CategoryTheory.ReflQuiver.opposite = CategoryTheory.ReflQuiver.mk fun (X : Vᵒᵖ) => Opposite.op (CategoryTheory.ReflQuiver.id (Opposite.unop X))

instance CategoryTheory.ReflQuiver.discreteQuiver (V : Type u) : CategoryTheory.ReflQuiver.{u + 1, u} (CategoryTheory.Discrete V)

Equations

• CategoryTheory.ReflQuiver.discreteQuiver V = CategoryTheory.ReflQuiver.mk CategoryTheory.CategoryStruct.id

def CategoryTheory.ReflQuiv : Type (max (u + 1) u (v + 1))

Equations

• CategoryTheory.ReflQuiv = CategoryTheory.Bundled CategoryTheory.ReflQuiver.{?u.4 + 1, ?u.3}

instance CategoryTheory.ReflQuiv.instCoeSortType : CoeSort CategoryTheory.ReflQuiv (Type u)

Equations

• CategoryTheory.ReflQuiv.instCoeSortType = { coe := CategoryTheory.Bundled.α }

instance CategoryTheory.ReflQuiv.str' (C : CategoryTheory.ReflQuiv) : CategoryTheory.ReflQuiver.{v + 1, u} ↑C

Equations

• C.str' = C.str

def CategoryTheory.ReflQuiv.toQuiv (C : CategoryTheory.ReflQuiv) : CategoryTheory.Quiv

Equations

• C.toQuiv = CategoryTheory.Quiv.of ↑C

def CategoryTheory.ReflQuiv.of (C : Type u) [CategoryTheory.ReflQuiver.{v + 1, u} C] : CategoryTheory.ReflQuiv

Construct a bundled ReflQuiv from the underlying type and the typeclass.

Equations

• CategoryTheory.ReflQuiv.of C = CategoryTheory.Bundled.of C

instance CategoryTheory.ReflQuiv.instInhabited : Inhabited CategoryTheory.ReflQuiv

Equations

• CategoryTheory.ReflQuiv.instInhabited = { default := CategoryTheory.ReflQuiv.of (CategoryTheory.Discrete default) }

@[simp]

theorem CategoryTheory.ReflQuiv.of_val (C : Type u) [CategoryTheory.ReflQuiver.{u_1 + 1, u} C] : ↑(CategoryTheory.ReflQuiv.of C) = C

instance CategoryTheory.ReflQuiv.category : CategoryTheory.LargeCategory CategoryTheory.ReflQuiv

Category structure on ReflQuiv

Equations

• CategoryTheory.ReflQuiv.category = CategoryTheory.Category.mk @CategoryTheory.ReflQuiv.category.proof_1 @CategoryTheory.ReflQuiv.category.proof_1 @CategoryTheory.ReflQuiv.category.proof_2

theorem CategoryTheory.ReflQuiv.id_eq_id (X : CategoryTheory.ReflQuiv) : CategoryTheory.CategoryStruct.id X = 𝟭rq ↑X

theorem CategoryTheory.ReflQuiv.comp_eq_comp {X : CategoryTheory.ReflQuiv} {Y : CategoryTheory.ReflQuiv} {Z : CategoryTheory.ReflQuiv} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp F G = F ⋙rq G

@[simp]

theorem CategoryTheory.ReflQuiv.forget_obj (C : CategoryTheory.Cat) : CategoryTheory.ReflQuiv.forget.obj C = CategoryTheory.ReflQuiv.of ↑C

@[simp]

theorem CategoryTheory.ReflQuiv.forget_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.ReflQuiv.forget.map F = CategoryTheory.Functor.toReflPrefunctor F

def CategoryTheory.ReflQuiv.forget : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.ReflQuiv

The forgetful functor from categories to quivers.

Equations

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

theorem CategoryTheory.ReflQuiv.forget_faithful {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑C ↑D) (G : CategoryTheory.Functor ↑C ↑D) (hyp : CategoryTheory.ReflQuiv.forget.map F = CategoryTheory.ReflQuiv.forget.map G) : F = G

theorem CategoryTheory.ReflQuiv.forget.Faithful : CategoryTheory.ReflQuiv.forget.Faithful

@[simp]

theorem CategoryTheory.ReflQuiv.forgetToQuiv_obj (V : CategoryTheory.ReflQuiv) : CategoryTheory.ReflQuiv.forgetToQuiv.obj V = CategoryTheory.Quiv.of ↑V

@[simp]

theorem CategoryTheory.ReflQuiv.forgetToQuiv_map : ∀ {X Y : CategoryTheory.ReflQuiv} (F : X ⟶ Y), CategoryTheory.ReflQuiv.forgetToQuiv.map F = F.toPrefunctor

def CategoryTheory.ReflQuiv.forgetToQuiv : CategoryTheory.Functor CategoryTheory.ReflQuiv CategoryTheory.Quiv

The forgetful functor from categories to quivers.

Equations

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

theorem CategoryTheory.ReflQuiv.forgetToQuiv_faithful {V : CategoryTheory.ReflQuiv} {W : CategoryTheory.ReflQuiv} (F : ↑V ⥤rq ↑W) (G : ↑V ⥤rq ↑W) (hyp : CategoryTheory.ReflQuiv.forgetToQuiv.map F = CategoryTheory.ReflQuiv.forgetToQuiv.map G) : F = G

theorem CategoryTheory.ReflQuiv.forgetToQuiv.Faithful : CategoryTheory.ReflQuiv.forgetToQuiv.Faithful

theorem CategoryTheory.ReflQuiv.forget_forgetToQuiv : CategoryTheory.ReflQuiv.forget.comp CategoryTheory.ReflQuiv.forgetToQuiv = CategoryTheory.Quiv.forget

def CategoryTheory.ReflPrefunctor.toFunctor {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : CategoryTheory.ReflQuiv.of ↑C ⟶ CategoryTheory.ReflQuiv.of ↑D) (hyp : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z), F.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) : CategoryTheory.Functor ↑C ↑D

Equations

• CategoryTheory.ReflPrefunctor.toFunctor F hyp = { obj := F.obj, map := fun {X Y : ↑C} => F.map, map_id := ⋯, map_comp := ⋯ }

inductive CategoryTheory.Cat.FreeReflRel {V : Type u_1} [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} V] (X : CategoryTheory.Paths V) (Y : CategoryTheory.Paths V) (f : X ⟶ Y) (g : X ⟶ Y) : Prop

• mk: ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver.{u_2 + 1, u_1} V] {X : V}, CategoryTheory.Cat.FreeReflRel X X (CategoryTheory.ReflQuiver.id X).toPath Quiver.Path.nil

def CategoryTheory.Cat.FreeRefl (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} V] : Type u_1

Equations

• CategoryTheory.Cat.FreeRefl V = CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel

instance CategoryTheory.Cat.instCategoryFreeRefl (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} V] : CategoryTheory.Category.{max u_1 u_2, u_1} (CategoryTheory.Cat.FreeRefl V)

Equations

• CategoryTheory.Cat.instCategoryFreeRefl V = inferInstanceAs (CategoryTheory.Category.{max ?u.18 ?u.17, ?u.18} (CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel))

def CategoryTheory.Cat.FreeRefl.quotientFunctor (V : Type u_1) [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} V] : CategoryTheory.Functor (↑(CategoryTheory.Cat.free.obj (CategoryTheory.Quiv.of V))) (CategoryTheory.Cat.FreeRefl V)

Equations

• CategoryTheory.Cat.FreeRefl.quotientFunctor V = CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel

theorem CategoryTheory.Cat.FreeRefl.lift_unique' {V : Type u_1} [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} V] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (F₁ : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D) (F₂ : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D) (h : (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp F₁ = (CategoryTheory.Cat.FreeRefl.quotientFunctor V).comp F₂) : F₁ = F₂

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_str_comp (V : CategoryTheory.ReflQuiv) ⦃a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel⦄ ⦃b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel⦄ ⦃c : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel⦄ : ∀ (a_1 : CategoryTheory.Quotient.Hom CategoryTheory.Cat.FreeReflRel a b) (a_2 : CategoryTheory.Quotient.Hom CategoryTheory.Cat.FreeReflRel b c), CategoryTheory.CategoryStruct.comp a_1 a_2 = CategoryTheory.Quotient.comp CategoryTheory.Cat.FreeReflRel a_1 a_2

@[simp]

theorem CategoryTheory.Cat.freeRefl_map_obj_as : ∀ {X Y : CategoryTheory.ReflQuiv} (f : X ⟶ Y) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel), ((CategoryTheory.Cat.freeRefl.map f).obj a).as = f.obj a.as

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_α (V : CategoryTheory.ReflQuiv) : ↑(CategoryTheory.Cat.freeRefl.obj V) = CategoryTheory.Cat.FreeRefl ↑V

@[simp]

theorem CategoryTheory.Cat.freeRefl_map_map : ∀ {X Y : CategoryTheory.ReflQuiv} (f : X ⟶ Y) (a b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (hf : a ⟶ b), (CategoryTheory.Cat.freeRefl.map f).map hf = Quot.liftOn hf (fun (f_1 : a.as ⟶ b.as) => (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑Y).map (f.mapPath f_1)) ⋯

@[simp]

theorem CategoryTheory.Cat.freeRefl_obj_str_id (V : CategoryTheory.ReflQuiv) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) : CategoryTheory.CategoryStruct.id a = Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (CategoryTheory.CategoryStruct.id a.as)

def CategoryTheory.Cat.freeRefl : CategoryTheory.Functor CategoryTheory.ReflQuiv CategoryTheory.Cat

Equations

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

theorem CategoryTheory.Cat.freeRefl_naturality {X : Type u_1} {Y : Type u_1} [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} X] [CategoryTheory.ReflQuiver.{u_2 + 1, u_1} Y] (f : X ⥤rq Y) : CategoryTheory.Functor.comp (CategoryTheory.Cat.free.map f.toPrefunctor) (CategoryTheory.Cat.FreeRefl.quotientFunctor Y) = (CategoryTheory.Cat.FreeRefl.quotientFunctor X).comp (CategoryTheory.Cat.freeRefl.map f)

def CategoryTheory.Cat.freeReflNatTrans : CategoryTheory.ReflQuiv.forgetToQuiv.comp CategoryTheory.Cat.free ⟶ CategoryTheory.Cat.freeRefl

Equations

• CategoryTheory.Cat.freeReflNatTrans = { app := fun (V : CategoryTheory.ReflQuiv) => CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V, naturality := CategoryTheory.Cat.freeReflNatTrans.proof_1 }

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_map (V : CategoryTheory.ReflQuiv) : ∀ {X Y : ↑V} (f : X ⟶ Y), (CategoryTheory.ReflQuiv.adj.unit.app V).map f = (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V).map ((CategoryTheory.Quiv.adj.unit.app V.toQuiv).map f)

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_toPrefunctor (V : CategoryTheory.ReflQuiv) : (CategoryTheory.ReflQuiv.adj.unit.app V).toPrefunctor = CategoryTheory.Quiv.adj.unit.app V.toQuiv ⋙q (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V).toPrefunctor

@[simp]

theorem CategoryTheory.ReflQuiv.adj.unit.app_obj (V : CategoryTheory.ReflQuiv) (X : ↑V) : (CategoryTheory.ReflQuiv.adj.unit.app V).obj X = (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V).obj ((CategoryTheory.Quiv.adj.unit.app V.toQuiv).obj X)

def CategoryTheory.ReflQuiv.adj.unit.app (V : CategoryTheory.ReflQuiv) : ↑V ⥤rq ↑(CategoryTheory.ReflQuiv.forget.obj (CategoryTheory.Cat.freeRefl.obj V))

Equations

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

theorem CategoryTheory.ReflQuiv.adj.unit.component_eq (V : CategoryTheory.ReflQuiv) : CategoryTheory.ReflQuiv.forgetToQuiv.map (CategoryTheory.ReflQuiv.adj.unit.app V) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Quiv.adj.unit.app V.toQuiv) (CategoryTheory.Quiv.forget.map (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑V))

This is used in the proof of both triangle equalities. Should we simp?

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.app_map (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (hf : a ⟶ b) : (CategoryTheory.ReflQuiv.adj.counit.app C).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => (CategoryTheory.Quiv.adj.counit.app C).map f) ⋯

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.app_obj (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) : (CategoryTheory.ReflQuiv.adj.counit.app C).obj a = (CategoryTheory.Quiv.adj.counit.app C).obj a.as

def CategoryTheory.ReflQuiv.adj.counit.app (C : CategoryTheory.Cat) : CategoryTheory.Functor ↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.forget.obj C)) ↑C

Equations

• CategoryTheory.ReflQuiv.adj.counit.app C = CategoryTheory.Quotient.lift CategoryTheory.Cat.FreeReflRel (CategoryTheory.Quiv.adj.counit.app C) ⋯

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.component_eq (C : CategoryTheory.Cat) : (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑C).comp (CategoryTheory.ReflQuiv.adj.counit.app C) = CategoryTheory.Quiv.adj.counit.app C

This is used in the proof of both triangle equalities.

@[simp]

theorem CategoryTheory.ReflQuiv.adj.counit.component_eq' (C : Type u_1) [CategoryTheory.Category.{max u_1 u_2, u_1} C] : (CategoryTheory.Cat.FreeRefl.quotientFunctor C).comp (CategoryTheory.ReflQuiv.adj.counit.app (CategoryTheory.Cat.of C)) = CategoryTheory.Quiv.adj.counit.app (CategoryTheory.Cat.of C)

def CategoryTheory.ReflQuiv.adj : CategoryTheory.Cat.freeRefl ⊣ CategoryTheory.ReflQuiv.forget

The adjunction between forming the free category on a quiver, and forgetting a category to a quiver.

Equations

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

theorem CategoryTheory.Fin.le_succ {n : ℕ} (i : Fin n) : i.castSucc ≤ i.succ

def CategoryTheory.Fin.hom_succ {n : ℕ} (i : Fin n) : i.castSucc ⟶ i.succ

Equations

• CategoryTheory.Fin.hom_succ i = CategoryTheory.homOfLE ⋯

@[reducible, inline]

abbrev CategoryTheory.SimplexCategory.Δ (k : ℕ) : Type

Equations

• CategoryTheory.SimplexCategory.Δ k = SimplexCategory.Truncated k

instance CategoryTheory.SimplexCategory.instCategoryΔ (k : ℕ) : CategoryTheory.Category.{0, 0} (CategoryTheory.SimplexCategory.Δ k)

Equations

• CategoryTheory.SimplexCategory.instCategoryΔ k = inferInstanceAs (CategoryTheory.Category.{0, 0} (CategoryTheory.FullSubcategory fun (a : SimplexCategory) => a.len ≤ k))

theorem CategoryTheory.SimplexCategory.Δ.Hom.ext_iff {k : ℕ} {a : CategoryTheory.SimplexCategory.Δ k} {b : CategoryTheory.SimplexCategory.Δ k} {f : a ⟶ b} {g : a ⟶ b} : f = g ↔ SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g

theorem CategoryTheory.SimplexCategory.Δ.Hom.ext {k : ℕ} {a : CategoryTheory.SimplexCategory.Δ k} {b : CategoryTheory.SimplexCategory.Δ k} (f : a ⟶ b) (g : a ⟶ b) : SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g

def CategoryTheory.SimplexCategory.mkOfLe {n : ℕ} (i : Fin (n + 1)) (j : Fin (n + 1)) (h : i ≤ j) : SimplexCategory.mk 1 ⟶ SimplexCategory.mk n

Equations

• CategoryTheory.SimplexCategory.mkOfLe i j h = SimplexCategory.mkHom { toFun := fun (x : Fin (1 + 1)) => match x with | 0 => i | 1 => j, monotone' := ⋯ }

def CategoryTheory.SimplexCategory.mkOfSucc {n : ℕ} (i : Fin n) : SimplexCategory.mk 1 ⟶ SimplexCategory.mk n

Equations

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

def CategoryTheory.SimplexCategory.mkOfLeComp {n : ℕ} (i : Fin (n + 1)) (j : Fin (n + 1)) (k : Fin (n + 1)) (h₁ : i ≤ j) (h₂ : j ≤ k) : SimplexCategory.mk 2 ⟶ SimplexCategory.mk n

Equations

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

@[reducible, inline]

abbrev CategoryTheory.SimplexCategory.Δ.ι (k : ℕ) : CategoryTheory.Functor (CategoryTheory.SimplexCategory.Δ k) SimplexCategory

The fully faithful inclusion of the truncated simplex category into the usual simplex category.

Equations

• CategoryTheory.SimplexCategory.Δ.ι k = SimplexCategory.Truncated.inclusion

instance CategoryTheory.SimplexCategory.Δ.ι.op_full (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.Full

Equations

• ⋯ = ⋯

instance CategoryTheory.SimplexCategory.Δ.ι.op_faithful (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.Faithful

Equations

• ⋯ = ⋯

theorem CategoryTheory.SimplexCategory.const_fac_thru_zero (n : SimplexCategory) (m : SimplexCategory) (i : Fin (m.len + 1)) : n.const m i = CategoryTheory.CategoryStruct.comp (n.const (SimplexCategory.mk 0) 0) ((SimplexCategory.mk 0).const m i)

theorem CategoryTheory.SimplexCategory.eq_const_of_zero {n : SimplexCategory} (f : SimplexCategory.mk 0 ⟶ n) : f = (SimplexCategory.mk 0).const n ((SimplexCategory.Hom.toOrderHom f) 0)

theorem CategoryTheory.SimplexCategory.eq_const_of_zero' {n : SimplexCategory} (f : SimplexCategory.mk 0 ⟶ n) : ∃ (a : Fin (n.len + 1)), f = (SimplexCategory.mk 0).const n a

theorem CategoryTheory.SimplexCategory.eq_const_to_zero {n : SimplexCategory} (f : n ⟶ SimplexCategory.mk 0) : f = n.const (SimplexCategory.mk 0) 0

theorem CategoryTheory.SimplexCategory.eq_of_one_to_one (f : SimplexCategory.mk 1 ⟶ SimplexCategory.mk 1) : (∃ (a : Fin ((SimplexCategory.mk 1).len + 1)), f = (SimplexCategory.mk 1).const (SimplexCategory.mk 1) a) ∨ f = CategoryTheory.CategoryStruct.id (SimplexCategory.mk 1)

theorem CategoryTheory.SimplexCategory.eq_of_one_to_two (f : SimplexCategory.mk 1 ⟶ SimplexCategory.mk 2) : f = SimplexCategory.δ 0 ∨ f = SimplexCategory.δ 1 ∨ f = SimplexCategory.δ 2 ∨ ∃ (a : Fin ((SimplexCategory.mk 2).len + 1)), f = (SimplexCategory.mk 1).const (SimplexCategory.mk 2) a

def CategoryTheory.SSet.Truncated.uliftFunctor (k : ℕ) : CategoryTheory.Functor (SSet.Truncated k) (SSet.Truncated k)

The ulift functor SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v} on truncated simplicial sets.

Equations

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

def CategoryTheory.SSet.truncation (k : ℕ) : CategoryTheory.Functor SSet (SSet.Truncated k)

This is called "sk" in SimplicialSet and SimplicialObject, but this is a better name.

Equations

• CategoryTheory.SSet.truncation k = (CategoryTheory.whiskeringLeft (SimplexCategory.Truncated k)ᵒᵖ SimplexCategoryᵒᵖ (Type ?u.7)).obj (CategoryTheory.SimplexCategory.Δ.ι k).op

def CategoryTheory.SSet.skAdj (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.lan ⊣ CategoryTheory.SSet.truncation k

Equations

• CategoryTheory.SSet.skAdj k = (CategoryTheory.SimplexCategory.Δ.ι k).op.lanAdjunction (Type ?u.34)

def CategoryTheory.SSet.coskAdj (k : ℕ) : CategoryTheory.SSet.truncation k ⊣ (CategoryTheory.SimplexCategory.Δ.ι k).op.ran

Equations

• CategoryTheory.SSet.coskAdj k = (CategoryTheory.SimplexCategory.Δ.ι k).op.ranAdjunction (Type ?u.34)

instance CategoryTheory.SSet.coskeleton_reflective (k : ℕ) : CategoryTheory.IsIso (CategoryTheory.SSet.coskAdj k).counit

Equations

• ⋯ = ⋯

instance CategoryTheory.SSet.skeleton_reflective (k : ℕ) : CategoryTheory.IsIso (CategoryTheory.SSet.skAdj k).unit

Equations

• ⋯ = ⋯

instance CategoryTheory.SSet.coskeleton.full (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.ran.Full

Equations

• ⋯ = ⋯

instance CategoryTheory.SSet.coskeleton.faithful (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.ran.Faithful

Equations

• ⋯ = ⋯

instance CategoryTheory.SSet.coskAdj.reflective (k : ℕ) : CategoryTheory.Reflective (CategoryTheory.SimplexCategory.Δ.ι k).op.ran

Equations

• CategoryTheory.SSet.coskAdj.reflective k = CategoryTheory.Reflective.mk (CategoryTheory.SSet.truncation k) (CategoryTheory.SSet.coskAdj k)

instance CategoryTheory.SSet.skeleton.full (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.lan.Full

Equations

• ⋯ = ⋯

instance CategoryTheory.SSet.skeleton.faithful (k : ℕ) : (CategoryTheory.SimplexCategory.Δ.ι k).op.lan.Faithful

Equations

• ⋯ = ⋯

instance CategoryTheory.SSet.skAdj.coreflective (k : ℕ) : CategoryTheory.Coreflective (CategoryTheory.SimplexCategory.Δ.ι k).op.lan

Equations

• CategoryTheory.SSet.skAdj.coreflective k = CategoryTheory.Coreflective.mk (CategoryTheory.SSet.truncation k) (CategoryTheory.SSet.skAdj k)

def CategoryTheory.nerveFunctor₂ : CategoryTheory.Functor CategoryTheory.Cat (SSet.Truncated 2)

Equations

• CategoryTheory.nerveFunctor₂ = CategoryTheory.nerveFunctor.comp (CategoryTheory.SSet.truncation 2)

def CategoryTheory.nerve₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : SSet.Truncated 2

Equations

• CategoryTheory.nerve₂ C = CategoryTheory.nerveFunctor₂.obj (CategoryTheory.Cat.of C)

theorem CategoryTheory.nerve₂_restrictedNerve (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : (CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerve C) = CategoryTheory.nerve₂ C

def CategoryTheory.nerve₂RestrictedIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : (CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerve C) ≅ CategoryTheory.nerve₂ C

Equations

• CategoryTheory.nerve₂RestrictedIso C = CategoryTheory.Iso.refl ((CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerve C))

def CategoryTheory.Nerve.nerveRightExtension (C : CategoryTheory.Cat) : (CategoryTheory.SimplexCategory.Δ.ι 2).op.RightExtension (CategoryTheory.nerveFunctor₂.obj C)

The identity natural transformation exhibits nerve C as a right extension of its restriction to (Δ 2).op along (Δ.ι 2).op.

Equations

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

def CategoryTheory.Nerve.nerveRightExtension.coneAt (C : CategoryTheory.Cat) (n : ℕ) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (CategoryTheory.SimplexCategory.Δ.ι 2).op).comp (CategoryTheory.nerveFunctor₂.obj C))

The natural transformation in nerveRightExtension C defines a cone with summit nerve C _[n] over the diagram (StructuredArrow.proj (op ([n] : SimplexCategory)) (Δ.ι 2).op ⋙ nerveFunctor₂.obj C) indexed by the category StructuredArrow (op [n]) (Δ.ι 2).op.

Equations

• CategoryTheory.Nerve.nerveRightExtension.coneAt C n = (CategoryTheory.Nerve.nerveRightExtension C).coneAt (Opposite.op (SimplexCategory.mk n))

theorem CategoryTheory.Nerve.ran.lift.eq {C : CategoryTheory.Cat} {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (CategoryTheory.SimplexCategory.Δ.ι 2).op).comp (CategoryTheory.nerveFunctor₂.obj C))) (x : s.pt) {i : Fin (n + 1)} {j : Fin (n + 1)} (k : i ⟶ j) : (s.π.app (CategoryTheory.Nerve.pt' i) x).obj 0 = (s.π.app (CategoryTheory.Nerve.ar' k) x).obj 0

theorem CategoryTheory.Nerve.ran.lift.eq₂ {C : CategoryTheory.Cat} {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (CategoryTheory.SimplexCategory.Δ.ι 2).op).comp (CategoryTheory.nerveFunctor₂.obj C))) (x : s.pt) {i : Fin (n + 1)} {j : Fin (n + 1)} (k : i ⟶ j) : (s.π.app (CategoryTheory.Nerve.pt' j) x).obj 0 = (s.π.app (CategoryTheory.Nerve.ar' k) x).obj 1

theorem CategoryTheory.Nerve.ran.lift.map {C : CategoryTheory.Cat} {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (CategoryTheory.SimplexCategory.Δ.ι 2).op).comp (CategoryTheory.nerveFunctor₂.obj C))) (x : s.pt) {i : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk n))).len + 1)} {j : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk n))).len + 1)} (k : i ⟶ j) : (CategoryTheory.Nerve.ran.lift s x).map k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' (s.π.app (CategoryTheory.Nerve.ar' k) x) 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))

def CategoryTheory.Nerve.isPointwiseRightKanExtensionAt (C : CategoryTheory.Cat) (n : ℕ) : (CategoryTheory.Nerve.nerveRightExtension C).IsPointwiseRightKanExtensionAt (Opposite.op (SimplexCategory.mk n))

Equations

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

def CategoryTheory.Nerve.isPointwiseRightKanExtension (C : CategoryTheory.Cat) : (CategoryTheory.Nerve.nerveRightExtension C).IsPointwiseRightKanExtension

Equations

• CategoryTheory.Nerve.isPointwiseRightKanExtension C Δ = CategoryTheory.Nerve.isPointwiseRightKanExtensionAt C (Opposite.unop Δ).len

def CategoryTheory.Nerve.isPointwiseRightKanExtension.isUniversal (C : CategoryTheory.Cat) : CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Nerve.nerveRightExtension C)

Equations

• CategoryTheory.Nerve.isPointwiseRightKanExtension.isUniversal C = (CategoryTheory.Nerve.isPointwiseRightKanExtension C).isUniversal

theorem CategoryTheory.Nerve.isRightKanExtension (C : CategoryTheory.Cat) : (CategoryTheory.Nerve.nerveRightExtension C).left.IsRightKanExtension (CategoryTheory.Nerve.nerveRightExtension C).hom

def CategoryTheory.Nerve.cosk2NatTrans : CategoryTheory.nerveFunctor ⟶ CategoryTheory.nerveFunctor₂.comp (CategoryTheory.SimplexCategory.Δ.ι 2).op.ran

The natural map from a nerve.

Equations

• CategoryTheory.Nerve.cosk2NatTrans = CategoryTheory.whiskerLeft CategoryTheory.nerveFunctor (CategoryTheory.SSet.coskAdj 2).unit

def CategoryTheory.Nerve.cosk2RightExtension.hom (C : CategoryTheory.Cat) : CategoryTheory.Nerve.nerveRightExtension C ⟶ CategoryTheory.Functor.RightExtension.mk ((CategoryTheory.SimplexCategory.Δ.ι 2).op.ran.obj ((CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerveFunctor.obj C))) ((CategoryTheory.SimplexCategory.Δ.ι 2).op.ranCounit.app ((CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerveFunctor.obj C)))

Equations

• CategoryTheory.Nerve.cosk2RightExtension.hom C = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.Nerve.cosk2NatTrans.app C) ⋯

instance CategoryTheory.Nerve.cosk2RightExtension.hom_isIso (C : CategoryTheory.Cat) : CategoryTheory.IsIso (CategoryTheory.Nerve.cosk2RightExtension.hom C)

Equations

• ⋯ = ⋯

def CategoryTheory.Nerve.cosk2RightExtension.component.hom.iso (C : CategoryTheory.Cat) : CategoryTheory.Nerve.nerveRightExtension C ≅ CategoryTheory.Functor.RightExtension.mk ((CategoryTheory.SimplexCategory.Δ.ι 2).op.ran.obj ((CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerveFunctor.obj C))) ((CategoryTheory.SimplexCategory.Δ.ι 2).op.ranCounit.app ((CategoryTheory.SimplexCategory.Δ.ι 2).op.comp (CategoryTheory.nerveFunctor.obj C)))

Equations

• CategoryTheory.Nerve.cosk2RightExtension.component.hom.iso C = CategoryTheory.asIso (CategoryTheory.Nerve.cosk2RightExtension.hom C)

def CategoryTheory.Nerve.cosk2NatIso.component (C : CategoryTheory.Cat) : CategoryTheory.nerveFunctor.obj C ≅ (CategoryTheory.SimplexCategory.Δ.ι 2).op.ran.obj (CategoryTheory.nerveFunctor₂.obj C)

Equations

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

def CategoryTheory.Nerve.cosk2Iso : CategoryTheory.nerveFunctor ≅ CategoryTheory.nerveFunctor₂.comp (CategoryTheory.SimplexCategory.Δ.ι 2).op.ran

It follows that we have a natural isomorphism between nerveFunctor and nerveFunctor ⋙ cosk₂ whose components are the isomorphisms just established.

Equations

• CategoryTheory.Nerve.cosk2Iso = CategoryTheory.NatIso.ofComponents CategoryTheory.Nerve.cosk2NatIso.component @CategoryTheory.Nerve.cosk2Iso.proof_2

def CategoryTheory.SSet.OneTruncation (S : SSet) : Type u_1

Equations

• CategoryTheory.SSet.OneTruncation S = S.obj (Opposite.op (SimplexCategory.mk 0))

def CategoryTheory.SSet.OneTruncation.src {S : SSet} (f : S.obj (Opposite.op (SimplexCategory.mk 1))) : CategoryTheory.SSet.OneTruncation S

Equations

• CategoryTheory.SSet.OneTruncation.src f = S.map (SimplexCategory.δ 1).op f

def CategoryTheory.SSet.OneTruncation.tgt {S : SSet} (f : S.obj (Opposite.op (SimplexCategory.mk 1))) : CategoryTheory.SSet.OneTruncation S

Equations

• CategoryTheory.SSet.OneTruncation.tgt f = S.map (SimplexCategory.δ 0).op f

def CategoryTheory.SSet.OneTruncation.Hom {S : SSet} (X : CategoryTheory.SSet.OneTruncation S) (Y : CategoryTheory.SSet.OneTruncation S) : Type u_1

Equations

• X.Hom Y = { p : S.obj (Opposite.op (SimplexCategory.mk 1)) // CategoryTheory.SSet.OneTruncation.src p = X ∧ CategoryTheory.SSet.OneTruncation.tgt p = Y }

instance CategoryTheory.instReflQuiverOneTruncation (S : SSet) : CategoryTheory.ReflQuiver.{u_1 + 1, u_1} (CategoryTheory.SSet.OneTruncation S)

Equations

• CategoryTheory.instReflQuiverOneTruncation S = CategoryTheory.ReflQuiver.mk fun (X : CategoryTheory.SSet.OneTruncation S) => ⟨S.map (SimplexCategory.σ 0).op X, ⋯⟩

def CategoryTheory.SSet.oneTruncation : CategoryTheory.Functor SSet CategoryTheory.ReflQuiv

Equations

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

theorem CategoryTheory.opstuff {C : Type u} [CategoryTheory.Category.{v, u} C] (V : CategoryTheory.Functor Cᵒᵖ (Type w)) {X : C} {Y : C} {Z : C} {α : X ⟶ Y} {β : Y ⟶ Z} {γ : X ⟶ Z} {φ : V.obj (Opposite.op Z)} : CategoryTheory.CategoryStruct.comp α β = γ → V.map α.op (V.map β.op φ) = V.map γ.op φ

def CategoryTheory.SSet.OneTruncation.ofNerve.map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve C)} {Y : CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve C)} (f : X ⟶ Y) : CategoryTheory.ComposableArrows.left X ⟶ CategoryTheory.ComposableArrows.left Y

Equations

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

def CategoryTheory.SSet.OneTruncation.ofNerve.hom {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve C) ⥤rq C

Equations

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

def CategoryTheory.SSet.OneTruncation.ofNerve.inv {C : Type u} [CategoryTheory.Category.{v, u} C] : C ⥤rq CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve C)

Equations

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

def CategoryTheory.SSet.OneTruncation.ofNerve (C : Type u) [CategoryTheory.Category.{u, u} C] : CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve C)) ≅ CategoryTheory.ReflQuiv.of C

Equations

• CategoryTheory.SSet.OneTruncation.ofNerve C = { hom := CategoryTheory.SSet.OneTruncation.ofNerve.hom, inv := CategoryTheory.SSet.OneTruncation.ofNerve.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.SSet.OneTruncation.ofNerve.natIso_inv_app_map (X : CategoryTheory.Cat) : ∀ {X_1 Y : ↑X} (f : X_1 ⟶ Y), (CategoryTheory.SSet.OneTruncation.ofNerve.natIso.inv.app X).map f = ⟨CategoryTheory.ComposableArrows.mk₁ f, ⋯⟩

@[simp]

theorem CategoryTheory.SSet.OneTruncation.ofNerve.natIso_inv_app_obj_map (X : CategoryTheory.Cat) : ∀ (x : ↑X) {X_1 Y : Fin 1} (x_1 : X_1 ⟶ Y), ((CategoryTheory.SSet.OneTruncation.ofNerve.natIso.inv.app X).obj x).map x_1 = CategoryTheory.CategoryStruct.id x

@[simp]

theorem CategoryTheory.SSet.OneTruncation.ofNerve.natIso_hom_app_map (X : CategoryTheory.Cat) : ∀ {X_1 Y : CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve ↑X)} (f : X_1 ⟶ Y), (CategoryTheory.SSet.OneTruncation.ofNerve.natIso.hom.app X).map f = CategoryTheory.SSet.OneTruncation.ofNerve.map f

@[simp]

theorem CategoryTheory.SSet.OneTruncation.ofNerve.natIso_hom_app_obj (X : CategoryTheory.Cat) : ∀ (x : CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve ↑X)), (CategoryTheory.SSet.OneTruncation.ofNerve.natIso.hom.app X).obj x = CategoryTheory.ComposableArrows.left x

@[simp]

theorem CategoryTheory.SSet.OneTruncation.ofNerve.natIso_inv_app_obj_obj (X : CategoryTheory.Cat) : ∀ (x : ↑X) (x_1 : Fin 1), ((CategoryTheory.SSet.OneTruncation.ofNerve.natIso.inv.app X).obj x).obj x_1 = x

def CategoryTheory.SSet.OneTruncation.ofNerve.natIso : CategoryTheory.nerveFunctor.comp CategoryTheory.SSet.oneTruncation ≅ CategoryTheory.ReflQuiv.forget

Equations

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

inductive CategoryTheory.SSet.HoRel {V : SSet} (X : ↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation V)))) (Y : ↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation V)))) (f : X ⟶ Y) (g : X ⟶ Y) : Prop

• mk: ∀ {V : SSet} (φ : V.obj (Opposite.op (SimplexCategory.mk 2))), CategoryTheory.SSet.HoRel { as := V.toPrefunctor.2 CategoryTheory.ι0.op φ } { as := V.toPrefunctor.2 CategoryTheory.ι2.op φ } (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (Quiver.Path.nil.cons (CategoryTheory.ev02 φ))) (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) ((Quiver.Path.nil.cons (CategoryTheory.ev01 φ)).cons (CategoryTheory.ev12 φ)))

theorem CategoryTheory.SSet.HoRel.ext_triangle {V : SSet} (X : CategoryTheory.SSet.OneTruncation V) (X' : CategoryTheory.SSet.OneTruncation V) (Y : CategoryTheory.SSet.OneTruncation V) (Y' : CategoryTheory.SSet.OneTruncation V) (Z : CategoryTheory.SSet.OneTruncation V) (Z' : CategoryTheory.SSet.OneTruncation V) (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (f : X ⟶ Z) (f' : X' ⟶ Z') (hf : ↑f = ↑f') (g : X ⟶ Y) (g' : X' ⟶ Y') (hg : ↑g = ↑g') (h : Y ⟶ Z) (h' : Y' ⟶ Z') (hh : ↑h = ↑h') : CategoryTheory.SSet.HoRel ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f)) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g).cons h)) ↔ CategoryTheory.SSet.HoRel ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f')) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g').cons h'))

def CategoryTheory.SSet.hoCat (V : SSet) : Type u

Equations

• CategoryTheory.SSet.hoCat V = CategoryTheory.Quotient CategoryTheory.SSet.HoRel

instance CategoryTheory.instCategoryHoCat (V : SSet) : CategoryTheory.Category.{u, u} (CategoryTheory.SSet.hoCat V)

Equations

• CategoryTheory.instCategoryHoCat V = inferInstanceAs (CategoryTheory.Category.{?u.11, ?u.11} (CategoryTheory.Quotient CategoryTheory.SSet.HoRel))

def CategoryTheory.SSet.hoFunctorMap {V : SSet} {W : SSet} (F : V ⟶ W) : CategoryTheory.Functor (CategoryTheory.SSet.hoCat V) (CategoryTheory.SSet.hoCat W)

Equations

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

def CategoryTheory.SSet.hoFunctor' : CategoryTheory.Functor SSet CategoryTheory.Cat

Equations

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

def CategoryTheory.SSet.OneTruncation₂ (S : SSet.Truncated 2) : Type u_1

Equations

• CategoryTheory.SSet.OneTruncation₂ S = S.obj (Opposite.op { obj := SimplexCategory.mk 0, property := CategoryTheory.SSet.OneTruncation₂.proof_1 })

@[reducible, inline]

abbrev CategoryTheory.SSet.δ₂ {n : ℕ} (i : Fin (n + 2)) (hn : autoParam ((SimplexCategory.mk n).len ≤ 2) _auto✝) (hn' : autoParam ((SimplexCategory.mk (n + 1)).len ≤ 2) _auto✝) : { obj := SimplexCategory.mk n, property := hn } ⟶ { obj := SimplexCategory.mk (n + 1), property := hn' }

Equations

• CategoryTheory.SSet.δ₂ i hn hn' = SimplexCategory.δ i

@[reducible, inline]

abbrev CategoryTheory.SSet.σ₂ {n : ℕ} (i : Fin (n + 1)) (hn : autoParam ((SimplexCategory.mk (n + 1)).len ≤ 2) _auto✝) (hn' : autoParam ((SimplexCategory.mk n).len ≤ 2) _auto✝) : { obj := SimplexCategory.mk (n + 1), property := hn } ⟶ { obj := SimplexCategory.mk n, property := hn' }

Equations

• CategoryTheory.SSet.σ₂ i hn hn' = SimplexCategory.σ i

def CategoryTheory.SSet.OneTruncation₂.src {S : SSet.Truncated 2} (f : S.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })) : CategoryTheory.SSet.OneTruncation₂ S

Equations

• CategoryTheory.SSet.OneTruncation₂.src f = S.map (CategoryTheory.SSet.δ₂ 1 CategoryTheory.SSet.OneTruncation₂.src.proof_3 CategoryTheory.SSet.OneTruncation₂.src.proof_2).op f

def CategoryTheory.SSet.OneTruncation₂.tgt {S : SSet.Truncated 2} (f : S.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })) : CategoryTheory.SSet.OneTruncation₂ S

Equations

• CategoryTheory.SSet.OneTruncation₂.tgt f = S.map (CategoryTheory.SSet.δ₂ 0 CategoryTheory.SSet.OneTruncation₂.tgt.proof_3 CategoryTheory.SSet.OneTruncation₂.tgt.proof_2).op f

def CategoryTheory.SSet.OneTruncation₂.Hom {S : SSet.Truncated 2} (X : CategoryTheory.SSet.OneTruncation₂ S) (Y : CategoryTheory.SSet.OneTruncation₂ S) : Type u_1

Equations

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

instance CategoryTheory.instReflQuiverOneTruncation₂ (S : SSet.Truncated 2) : CategoryTheory.ReflQuiver.{u_1 + 1, u_1} (CategoryTheory.SSet.OneTruncation₂ S)

Equations

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

def CategoryTheory.SSet.oneTruncation₂ : CategoryTheory.Functor (SSet.Truncated 2) CategoryTheory.ReflQuiv

Equations

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

def CategoryTheory.SSet.OneTruncation₂.ofTwoTruncationIso (V : SSet) : CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ ((CategoryTheory.SSet.truncation 2).obj V)) ≅ CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation V)

Equations

• CategoryTheory.SSet.OneTruncation₂.ofTwoTruncationIso V = CategoryTheory.Iso.refl (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ ((CategoryTheory.SSet.truncation 2).obj V)))

def CategoryTheory.SSet.OneTruncation₂.nerve₂Iso (C : CategoryTheory.Cat) : CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ (CategoryTheory.nerve₂ ↑C)) ≅ CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation (CategoryTheory.nerve ↑C))

Equations

• CategoryTheory.SSet.OneTruncation₂.nerve₂Iso C = CategoryTheory.Iso.refl (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ (CategoryTheory.nerve₂ ↑C)))

@[simp]

theorem CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso_inv_app_map (X : CategoryTheory.Cat) : ∀ {X_1 Y : ↑((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂).obj X)} (f : X_1 ⟶ Y), (CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso.inv.app X).map f = f

@[simp]

theorem CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso_hom_app_obj (X : CategoryTheory.Cat) (X : ↑((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂).obj X✝)) : (CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso.hom.app X✝).obj X = X

@[simp]

theorem CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso_inv_app_obj (X : CategoryTheory.Cat) (X : ↑((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂).obj X✝)) : (CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso.inv.app X✝).obj X = X

@[simp]

theorem CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso_hom_app_map (X : CategoryTheory.Cat) : ∀ {X_1 Y : ↑((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂).obj X)} (f : X_1 ⟶ Y), (CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso.hom.app X).map f = f

def CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso : CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂ ≅ CategoryTheory.nerveFunctor.comp CategoryTheory.SSet.oneTruncation

Equations

• CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso = CategoryTheory.Iso.refl (CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂)

inductive CategoryTheory.SSet.HoRel₂ {V : SSet.Truncated 2} (X : ↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ V)))) (Y : ↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ V)))) (f : X ⟶ Y) (g : X ⟶ Y) : Prop

• mk: ∀ {V : SSet.Truncated 2} (φ : V.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), CategoryTheory.SSet.HoRel₂ { as := V.toPrefunctor.2 CategoryTheory.ι0₂.op φ } { as := V.toPrefunctor.2 CategoryTheory.ι2₂.op φ } (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (Quiver.Path.nil.cons (CategoryTheory.ev02₂ φ))) (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) ((Quiver.Path.nil.cons (CategoryTheory.ev01₂ φ)).cons (CategoryTheory.ev12₂ φ)))

theorem CategoryTheory.SSet.HoRel₂.ext_triangle {V : SSet.Truncated 2} (X : CategoryTheory.SSet.OneTruncation₂ V) (X' : CategoryTheory.SSet.OneTruncation₂ V) (Y : CategoryTheory.SSet.OneTruncation₂ V) (Y' : CategoryTheory.SSet.OneTruncation₂ V) (Z : CategoryTheory.SSet.OneTruncation₂ V) (Z' : CategoryTheory.SSet.OneTruncation₂ V) (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (f : X ⟶ Z) (f' : X' ⟶ Z') (hf : ↑f = ↑f') (g : X ⟶ Y) (g' : X' ⟶ Y') (hg : ↑g = ↑g') (h : Y ⟶ Z) (h' : Y' ⟶ Z') (hh : ↑h = ↑h') : CategoryTheory.SSet.HoRel₂ ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f)) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g).cons h)) ↔ CategoryTheory.SSet.HoRel₂ ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f')) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g').cons h'))

def CategoryTheory.SSet.hoFunctor₂Obj (V : SSet.Truncated 2) : Type u

Equations

• CategoryTheory.SSet.hoFunctor₂Obj V = CategoryTheory.Quotient CategoryTheory.SSet.HoRel₂

instance CategoryTheory.instCategoryHoFunctor₂Obj (V : SSet.Truncated 2) : CategoryTheory.Category.{u, u} (CategoryTheory.SSet.hoFunctor₂Obj V)

Equations

• CategoryTheory.instCategoryHoFunctor₂Obj V = inferInstanceAs (CategoryTheory.Category.{?u.12, ?u.12} (CategoryTheory.Quotient CategoryTheory.SSet.HoRel₂))

def CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor (V : SSet.Truncated 2) : CategoryTheory.Functor (↑(CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of (CategoryTheory.SSet.OneTruncation₂ V)))) (CategoryTheory.SSet.hoFunctor₂Obj V)

Equations

• CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor V = CategoryTheory.Quotient.functor CategoryTheory.SSet.HoRel₂

theorem CategoryTheory.SSet.hoFunctor₂Obj.lift_unique' (V : SSet.Truncated 2) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F₁ : CategoryTheory.Functor (CategoryTheory.SSet.hoFunctor₂Obj V) D) (F₂ : CategoryTheory.Functor (CategoryTheory.SSet.hoFunctor₂Obj V) D) (h : (CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor V).comp F₁ = (CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor V).comp F₂) : F₁ = F₂

def CategoryTheory.SSet.hoFunctor₂Map {V : SSet.Truncated 2} {W : SSet.Truncated 2} (F : V ⟶ W) : CategoryTheory.Functor (CategoryTheory.SSet.hoFunctor₂Obj V) (CategoryTheory.SSet.hoFunctor₂Obj W)

Equations

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

def CategoryTheory.SSet.hoFunctor₂ : CategoryTheory.Functor (SSet.Truncated 2) CategoryTheory.Cat

Equations

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

theorem CategoryTheory.SSet.hoFunctor₂_naturality {X : SSet.Truncated 2} {Y : SSet.Truncated 2} (f : X ⟶ Y) : CategoryTheory.Functor.comp ((CategoryTheory.SSet.oneTruncation₂.comp CategoryTheory.Cat.freeRefl).map f) (CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor Y) = (CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor X).comp (CategoryTheory.SSet.hoFunctor₂Map f)

def CategoryTheory.SSet.hoFunctor : CategoryTheory.Functor SSet CategoryTheory.Cat

Equations

• CategoryTheory.SSet.hoFunctor = (CategoryTheory.SSet.truncation 2).comp CategoryTheory.SSet.hoFunctor₂

@[simp]

theorem CategoryTheory.forgetToReflQuiv.natIso_inv_app_obj_obj (X : CategoryTheory.Cat) (X : ↑(CategoryTheory.ReflQuiv.forget.obj X✝)) : ∀ (x : Fin 1), ((CategoryTheory.forgetToReflQuiv.natIso.inv.app X✝).obj X).obj x = X

@[simp]

theorem CategoryTheory.forgetToReflQuiv.natIso_inv_app_obj_map (X : CategoryTheory.Cat) (X : ↑(CategoryTheory.ReflQuiv.forget.obj X✝)) : ∀ {X_1 Y : Fin 1} (x : X_1 ⟶ Y), ((CategoryTheory.forgetToReflQuiv.natIso.inv.app X✝).obj X).map x = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.forgetToReflQuiv.natIso_hom_app_map (X : CategoryTheory.Cat) : ∀ {X_1 Y : ↑((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂).obj X)} (f : X_1 ⟶ Y), (CategoryTheory.forgetToReflQuiv.natIso.hom.app X).map f = CategoryTheory.SSet.OneTruncation.ofNerve.map f

@[simp]

theorem CategoryTheory.forgetToReflQuiv.natIso_hom_app_obj (X : CategoryTheory.Cat) (X : ↑((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂).obj X✝)) : (CategoryTheory.forgetToReflQuiv.natIso.hom.app X✝).obj X = CategoryTheory.ComposableArrows.left X

@[simp]

theorem CategoryTheory.forgetToReflQuiv.natIso_inv_app_map (X : CategoryTheory.Cat) : ∀ {X_1 Y : ↑(CategoryTheory.ReflQuiv.forget.obj X)} (f : X_1 ⟶ Y), (CategoryTheory.forgetToReflQuiv.natIso.inv.app X).map f = ⟨CategoryTheory.ComposableArrows.mk₁ f, ⋯⟩

def CategoryTheory.forgetToReflQuiv.natIso : CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.oneTruncation₂ ≅ CategoryTheory.ReflQuiv.forget

Equations

• CategoryTheory.forgetToReflQuiv.natIso = CategoryTheory.SSet.OneTruncation₂.nerve₂.natIso ≪≫ CategoryTheory.SSet.OneTruncation.ofNerve.natIso

@[simp]

theorem CategoryTheory.nerve₂Adj.counit.component_map (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.SSet.HoRel₂) (b : CategoryTheory.Quotient CategoryTheory.SSet.HoRel₂) (hf : a ⟶ b) : (CategoryTheory.nerve₂Adj.counit.component C).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => (CategoryTheory.ReflQuiv.adj.counit.app C).map (Quot.liftOn f (fun (f : a.as.as ⟶ b.as.as) => (CategoryTheory.Cat.FreeRefl.quotientFunctor ↑C).map ((CategoryTheory.forgetToReflQuiv.natIso.hom.app C).mapPath f)) ⋯)) ⋯

@[simp]

theorem CategoryTheory.nerve₂Adj.counit.component_obj (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.SSet.HoRel₂) : (CategoryTheory.nerve₂Adj.counit.component C).obj a = (CategoryTheory.ReflQuiv.adj.counit.app C).obj ((CategoryTheory.Cat.freeRefl.map (CategoryTheory.forgetToReflQuiv.natIso.hom.app C)).obj a.as)

def CategoryTheory.nerve₂Adj.counit.component (C : CategoryTheory.Cat) : CategoryTheory.Functor ↑(CategoryTheory.SSet.hoFunctor₂.obj (CategoryTheory.nerveFunctor₂.obj C)) ↑C

Equations

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

@[simp]

theorem CategoryTheory.nerve₂Adj.counit.component_eq (C : CategoryTheory.Cat) : (CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor (CategoryTheory.nerve₂ ↑C)).comp (CategoryTheory.nerve₂Adj.counit.component C) = (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight CategoryTheory.forgetToReflQuiv.natIso.hom CategoryTheory.Cat.freeRefl) CategoryTheory.ReflQuiv.adj.counit).app C

theorem CategoryTheory.nerve₂Adj.counit.naturality' ⦃C : CategoryTheory.Cat⦄ ⦃D : CategoryTheory.Cat⦄ (F : C ⟶ D) : CategoryTheory.Functor.comp ((CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.hoFunctor₂).map F) (CategoryTheory.nerve₂Adj.counit.component D) = (CategoryTheory.nerve₂Adj.counit.component C).comp F

def CategoryTheory.nerve₂Adj.counit : CategoryTheory.nerveFunctor₂.comp CategoryTheory.SSet.hoFunctor₂ ⟶ CategoryTheory.Functor.id CategoryTheory.Cat

Equations

• CategoryTheory.nerve₂Adj.counit = { app := CategoryTheory.nerve₂Adj.counit.component, naturality := CategoryTheory.nerve₂Adj.counit.naturality' }

def CategoryTheory.toNerve₂.mk.app {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (F : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.ReflQuiv.of ↑C) (n : CategoryTheory.SimplexCategory.Δ 2) : X.obj (Opposite.op n) ⟶ (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op n)

Equations

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

@[simp]

theorem CategoryTheory.toNerve₂.mk.app_zero {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (F : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.ReflQuiv.of ↑C) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) : CategoryTheory.toNerve₂.mk.app F { obj := SimplexCategory.mk 0, property := ⋯ } x = CategoryTheory.ComposableArrows.mk₀ (F.obj x)

@[simp]

theorem CategoryTheory.toNerve₂.mk.app_one {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (F : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.ReflQuiv.of ↑C) (f : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })) : CategoryTheory.toNerve₂.mk.app F { obj := SimplexCategory.mk 1, property := ⋯ } f = CategoryTheory.ComposableArrows.mk₁ (F.map ⟨f, ⋯⟩)

@[simp]

theorem CategoryTheory.toNerve₂.mk.app_two {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (F : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.ReflQuiv.of ↑C) (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })) : CategoryTheory.toNerve₂.mk.app F { obj := SimplexCategory.mk 2, property := ⋯ } φ = CategoryTheory.ComposableArrows.mk₂ (F.map (CategoryTheory.ev01₂ φ)) (F.map (CategoryTheory.ev12₂ φ))

def CategoryTheory.nerve₂.seagull (C : CategoryTheory.Cat) : (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ }) ⟶ (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ }) ⨯ (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })

This is similiar to one of the famous Segal maps, except valued in a product rather than a pullback.

Equations

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

instance CategoryTheory.instMonoObjOppositeTruncatedOfNatNatCatTruncatedNerveFunctor₂OpMkSimplexCategoryLeLenMkProdSeagull (C : CategoryTheory.Cat) : CategoryTheory.Mono (CategoryTheory.nerve₂.seagull C)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.toNerve₂.mk_app {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (F : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.ReflQuiv.of ↑C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (CategoryTheory.ev02₂ φ) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ev01₂ φ)) (F.map (CategoryTheory.ev12₂ φ))) (n : (SimplexCategory.Truncated 2)ᵒᵖ) : ∀ (a : X.obj (Opposite.op (Opposite.unop n))), (CategoryTheory.toNerve₂.mk F hyp).app n a = CategoryTheory.toNerve₂.mk.app F (Opposite.unop n) a

def CategoryTheory.toNerve₂.mk {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (F : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.ReflQuiv.of ↑C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (CategoryTheory.ev02₂ φ) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ev01₂ φ)) (F.map (CategoryTheory.ev12₂ φ))) : X ⟶ CategoryTheory.nerveFunctor₂.obj C

Equations

• CategoryTheory.toNerve₂.mk F hyp = { app := fun (n : (SimplexCategory.Truncated 2)ᵒᵖ) => CategoryTheory.toNerve₂.mk.app F (Opposite.unop n), naturality := ⋯ }

@[simp]

theorem CategoryTheory.toNerve₂.mk'_app {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (f : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.SSet.oneTruncation₂.obj (CategoryTheory.nerveFunctor₂.obj C)) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev02₂ φ) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev01₂ φ)) ((CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev12₂ φ))) (n : (SimplexCategory.Truncated 2)ᵒᵖ) : ∀ (a : X.obj (Opposite.op (Opposite.unop n))), (CategoryTheory.toNerve₂.mk' f hyp).app n a = CategoryTheory.toNerve₂.mk.app (CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.hom.app C)) (Opposite.unop n) a

def CategoryTheory.toNerve₂.mk' {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (f : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.SSet.oneTruncation₂.obj (CategoryTheory.nerveFunctor₂.obj C)) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev02₂ φ) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev01₂ φ)) ((CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev12₂ φ))) : X ⟶ CategoryTheory.nerveFunctor₂.obj C

ER: We might prefer this version where we are missing the analogue of the hypothesis hyp conjugated by the isomorphism nerve₂Adj.NatIso.app C

Equations

• CategoryTheory.toNerve₂.mk' f hyp = CategoryTheory.toNerve₂.mk (CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom) hyp

theorem CategoryTheory.oneTruncation₂_toNerve₂Mk' {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (f : CategoryTheory.SSet.oneTruncation₂.obj X ⟶ CategoryTheory.SSet.oneTruncation₂.obj (CategoryTheory.nerveFunctor₂.obj C)) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev02₂ φ) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev01₂ φ)) ((CategoryTheory.CategoryStruct.comp f (CategoryTheory.forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev12₂ φ))) : CategoryTheory.SSet.oneTruncation₂.map (CategoryTheory.toNerve₂.mk' f hyp) = f

theorem CategoryTheory.toNerve₂.ext {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (f : X ⟶ CategoryTheory.nerve₂ ↑C) (g : X ⟶ CategoryTheory.nerve₂ ↑C) (hyp : CategoryTheory.SSet.oneTruncation₂.map f = CategoryTheory.SSet.oneTruncation₂.map g) : f = g

Now do a case split. For n = 0 and n = 1 this is covered by the hypothesis. For n = 2 this is covered by the new lemma above.

theorem CategoryTheory.toNerve₂.ext' {X : SSet.Truncated 2} {C : CategoryTheory.Cat} (f : X ⟶ CategoryTheory.nerveFunctor₂.obj C) (g : X ⟶ CategoryTheory.nerveFunctor₂.obj C) (hyp : CategoryTheory.SSet.oneTruncation₂.map f = CategoryTheory.SSet.oneTruncation₂.map g) : f = g

ER: This is dumb.

def CategoryTheory.nerve₂Adj.unit.component (X : SSet.Truncated 2) : X ⟶ CategoryTheory.nerveFunctor₂.obj (CategoryTheory.SSet.hoFunctor₂.obj X)

Equations

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

theorem CategoryTheory.nerve₂Adj.unit.component_eq (X : SSet.Truncated 2) : CategoryTheory.SSet.oneTruncation₂.map (CategoryTheory.nerve₂Adj.unit.component X) = CategoryTheory.ReflQuiv.adj.unit.app (CategoryTheory.SSet.oneTruncation₂.obj X) ⋙rq (CategoryTheory.SSet.hoFunctor₂Obj.quotientFunctor X).toReflPrefunctor ⋙rq CategoryTheory.forgetToReflQuiv.natIso.inv.app (CategoryTheory.SSet.hoFunctor₂.obj X)

def CategoryTheory.nerve₂Adj.unit : CategoryTheory.Functor.id (SSet.Truncated 2) ⟶ CategoryTheory.SSet.hoFunctor₂.comp CategoryTheory.nerveFunctor₂

Equations

• CategoryTheory.nerve₂Adj.unit = { app := CategoryTheory.nerve₂Adj.unit.component, naturality := CategoryTheory.nerve₂Adj.unit.proof_1 }

def CategoryTheory.nerve₂Adj : CategoryTheory.SSet.hoFunctor₂ ⊣ CategoryTheory.nerveFunctor₂

The adjunction between forming the free category on a quiver, and forgetting a category to a quiver.

Equations

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

instance CategoryTheory.nerveFunctor₂.faithful : CategoryTheory.nerveFunctor₂.Faithful

Equations

• CategoryTheory.nerveFunctor₂.faithful = ⋯

instance CategoryTheory.nerveFunctor₂.full : CategoryTheory.nerveFunctor₂.Full

Equations

• CategoryTheory.nerveFunctor₂.full = ⋯

instance CategoryTheory.nerve₂Adj.reflective : CategoryTheory.Reflective CategoryTheory.nerveFunctor₂

Equations

• CategoryTheory.nerve₂Adj.reflective = CategoryTheory.Reflective.mk CategoryTheory.SSet.hoFunctor₂ CategoryTheory.nerve₂Adj

def CategoryTheory.nerveAdjunction : CategoryTheory.SSet.hoFunctor ⊣ CategoryTheory.nerveFunctor

Equations

• CategoryTheory.nerveAdjunction = ((CategoryTheory.SSet.coskAdj 2).comp CategoryTheory.nerve₂Adj).ofNatIsoRight CategoryTheory.Nerve.cosk2Iso.symm

instance CategoryTheory.nerveFunctor.faithful : CategoryTheory.nerveFunctor.Faithful

Repleteness exists for full and faithful functors but not fully faithful functors, which is why we do this inefficiently.

Equations

• CategoryTheory.nerveFunctor.faithful = ⋯

instance CategoryTheory.nerveFunctor.full : CategoryTheory.nerveFunctor.Full

Equations

• CategoryTheory.nerveFunctor.full = ⋯

instance CategoryTheory.nerveCounit_isIso : CategoryTheory.IsIso CategoryTheory.nerveAdjunction.counit

Equations

• CategoryTheory.nerveCounit_isIso = ⋯

def CategoryTheory.nerveCounitNatIso : CategoryTheory.nerveFunctor.comp CategoryTheory.SSet.hoFunctor ≅ CategoryTheory.Functor.id CategoryTheory.Cat

Equations

• CategoryTheory.nerveCounitNatIso = CategoryTheory.asIso CategoryTheory.nerveAdjunction.counit

instance CategoryTheory.instReflectiveSSetCatNerveFunctor : CategoryTheory.Reflective CategoryTheory.nerveFunctor

Equations

• CategoryTheory.instReflectiveSSetCatNerveFunctor = CategoryTheory.Reflective.mk CategoryTheory.SSet.hoFunctor CategoryTheory.nerveAdjunction

instance CategoryTheory.instHasColimitsCat_infinityCosmos : CategoryTheory.Limits.HasColimits CategoryTheory.Cat

Equations

• CategoryTheory.instHasColimitsCat_infinityCosmos = ⋯