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)

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 {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 (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 := ⋯ }

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.

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

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

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 (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)))

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₂)

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

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₂

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.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_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_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.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_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)

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

• ⋯ = ⋯

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.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.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

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

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_infinityCosmos : CategoryTheory.Reflective CategoryTheory.nerveFunctor

Equations

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

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

Equations

• CategoryTheory.instHasColimitsCat_infinityCosmos = ⋯