theorem CategoryTheory.Quotient.CompClosure.congruence {C : Type u_1} [Category.{u_2, u_1} C] (r : HomRel C) : Congruence fun (a b : C) => Relation.EqvGen (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 : ℕ) : Category.{0, 0} (Δ 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 b : Δ k} (f g : a ⟶ b) : SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g

def CategoryTheory.SimplexCategory.mkOfLe {n : ℕ} (i 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 j 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 : ℕ) : Functor (Δ k) SimplexCategory

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

Equations

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

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

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

theorem CategoryTheory.SimplexCategory.const_fac_thru_zero (n m : SimplexCategory) (i : Fin (m.len + 1)) : n.const m i = 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 = 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 : ℕ) : 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 : ℕ) : 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 : ℕ) : (SimplexCategory.Δ.ι k).op.lan ⊣ truncation k

Equations

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

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

Equations

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

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

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

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

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

instance CategoryTheory.SSet.coskAdj.reflective (k : ℕ) : Reflective (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 : ℕ) : (SimplexCategory.Δ.ι k).op.lan.Full

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

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

Equations

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

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

Equations

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

def CategoryTheory.nerve₂ (C : Type u_1) [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) [Category.{u_2, u_1} C] : (SimplexCategory.Δ.ι 2).op.comp (nerve C) = nerve₂ C

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

Equations

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

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

def CategoryTheory.Nerve.isPointwiseRightKanExtensionAt (C : Cat) (n : ℕ) : (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 : Cat) : (nerveRightExtension C).IsPointwiseRightKanExtension

Equations

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

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

Equations

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

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

def CategoryTheory.Nerve.cosk2NatTrans : nerveFunctor ⟶ nerveFunctor₂.comp (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 : Cat) : nerveRightExtension C ⟶ Functor.RightExtension.mk ((SimplexCategory.Δ.ι 2).op.ran.obj ((SimplexCategory.Δ.ι 2).op.comp (nerveFunctor.obj C))) ((SimplexCategory.Δ.ι 2).op.ranCounit.app ((SimplexCategory.Δ.ι 2).op.comp (nerveFunctor.obj C)))

Equations

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

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

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

Equations

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

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

Equations

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

def CategoryTheory.Nerve.cosk2Iso : nerveFunctor ≅ nerveFunctor₂.comp (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))) : 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))) : OneTruncation S

Equations

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

def CategoryTheory.SSet.OneTruncation.Hom {S : SSet} (X Y : 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) : ReflQuiver (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 : Functor SSet ReflQuiv

Equations

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

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

def CategoryTheory.SSet.OneTruncation.ofNerve.map {C : Type u} [Category.{v, u} C] {X Y : OneTruncation (nerve C)} (f : X ⟶ Y) : ComposableArrows.left X ⟶ 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} [Category.{v, u} C] : OneTruncation (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} [Category.{v, u} C] : C ⥤rq OneTruncation (nerve C)

Equations

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

def CategoryTheory.SSet.OneTruncation.ofNerve (C : Type u) [Category.{u, u} C] : ReflQuiv.of (OneTruncation (nerve C)) ≅ 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 : nerveFunctor.comp oneTruncation ≅ 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 : Cat) {X✝ Y✝ : OneTruncation (nerve ↑X)} (f : X✝ ⟶ Y✝) : (natIso.hom.app X).map f = map f

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.SSet.HoRel.ext_triangle {V : SSet} (X X' Y Y' Z Z' : 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') : HoRel ((Quotient.functor Cat.FreeReflRel).obj X) ((Quotient.functor Cat.FreeReflRel).obj Z) ((Quotient.functor Cat.FreeReflRel).map (Quiver.Path.nil.cons f)) ((Quotient.functor Cat.FreeReflRel).map ((Quiver.Path.nil.cons g).cons h)) ↔ HoRel ((Quotient.functor Cat.FreeReflRel).obj X') ((Quotient.functor Cat.FreeReflRel).obj Z') ((Quotient.functor Cat.FreeReflRel).map (Quiver.Path.nil.cons f')) ((Quotient.functor 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) : Category.{u, u} (SSet.hoCat V)

Equations

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

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

Equations

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

def CategoryTheory.SSet.hoFunctor' : Functor SSet 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 : (SimplexCategory.mk n).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) : { 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 : (SimplexCategory.mk (n + 1)).len ≤ 2 := by decide) (hn' : (SimplexCategory.mk n).len ≤ 2 := by decide) : { 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 := ⋯ })) : 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 := ⋯ })) : 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 Y : 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) : ReflQuiver (SSet.OneTruncation₂ S)

Equations

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

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

Equations

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

def CategoryTheory.SSet.OneTruncation₂.ofTwoTruncationIso (V : SSet) : ReflQuiv.of (OneTruncation₂ ((truncation 2).obj V)) ≅ ReflQuiv.of (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 : Cat) : ReflQuiv.of (OneTruncation₂ (nerve₂ ↑C)) ≅ ReflQuiv.of (OneTruncation (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 : nerveFunctor₂.comp oneTruncation₂ ≅ nerveFunctor.comp 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 : Cat) (X✝ : ↑((nerveFunctor₂.comp oneTruncation₂).obj X)) : (natIso.hom.app X).obj X✝ = X✝

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.SSet.HoRel₂.ext_triangle {V : SSet.Truncated 2} (X X' Y Y' Z Z' : 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') : HoRel₂ ((Quotient.functor Cat.FreeReflRel).obj X) ((Quotient.functor Cat.FreeReflRel).obj Z) ((Quotient.functor Cat.FreeReflRel).map (Quiver.Path.nil.cons f)) ((Quotient.functor Cat.FreeReflRel).map ((Quiver.Path.nil.cons g).cons h)) ↔ HoRel₂ ((Quotient.functor Cat.FreeReflRel).obj X') ((Quotient.functor Cat.FreeReflRel).obj Z') ((Quotient.functor Cat.FreeReflRel).map (Quiver.Path.nil.cons f')) ((Quotient.functor 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) : Category.{u, u} (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) : Functor (↑(Cat.freeRefl.obj (ReflQuiv.of (OneTruncation₂ V)))) (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} [Category.{u_2, u_1} D] (F₁ F₂ : Functor (hoFunctor₂Obj V) D) (h : (quotientFunctor V).comp F₁ = (quotientFunctor V).comp F₂) : F₁ = F₂

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

Equations

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

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

Equations

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

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

def CategoryTheory.SSet.hoFunctor : Functor SSet Cat

Equations

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

def CategoryTheory.forgetToReflQuiv.natIso : nerveFunctor₂.comp SSet.oneTruncation₂ ≅ 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 : Cat) (X✝ : ↑(ReflQuiv.forget.obj X)) {X✝¹ Y✝ : Fin 1} (x✝ : X✝¹ ⟶ Y✝) : ((natIso.inv.app X).obj X✝).map x✝ = CategoryStruct.id X✝

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.nerve₂Adj.counit.component (C : Cat) : Functor ↑(SSet.hoFunctor₂.obj (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 : Cat) (a : Quotient SSet.HoRel₂) : (component C).obj a = (ReflQuiv.adj.counit.app C).obj ((Cat.freeRefl.map (forgetToReflQuiv.natIso.hom.app C)).obj a.as)

@[simp]

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

@[simp]

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

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

def CategoryTheory.nerve₂Adj.counit : nerveFunctor₂.comp SSet.hoFunctor₂ ⟶ Functor.id 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 : Cat} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of ↑C) (n : SimplexCategory.Δ 2) : X.obj (Opposite.op n) ⟶ (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 : Cat} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of ↑C) (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) : app F { obj := SimplexCategory.mk 0, property := ⋯ } x = ComposableArrows.mk₀ (F.obj x)

@[simp]

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

@[simp]

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

def CategoryTheory.nerve₂.seagull (C : Cat) : (nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ }) ⟶ (nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ }) ⨯ (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 : Cat) : Mono (nerve₂.seagull C)

def CategoryTheory.toNerve₂.mk {X : SSet.Truncated 2} {C : Cat} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of ↑C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (CategoryTheory.ev02₂✝ φ) = CategoryStruct.comp (F.map (CategoryTheory.ev01₂✝ φ)) (F.map (CategoryTheory.ev12₂✝ φ))) : X ⟶ 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 : Cat} (F : SSet.oneTruncation₂.obj X ⟶ ReflQuiv.of ↑C) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), F.map (CategoryTheory.ev02₂✝ φ) = CategoryStruct.comp (F.map (CategoryTheory.ev01₂✝ φ)) (F.map (CategoryTheory.ev12₂✝ φ))) (n : (SimplexCategory.Truncated 2)ᵒᵖ) (a✝ : X.obj (Opposite.op (Opposite.unop n))) : (mk F hyp).app n a✝ = mk.app F (Opposite.unop n) a✝

def CategoryTheory.toNerve₂.mk' {X : SSet.Truncated 2} {C : Cat} (f : SSet.oneTruncation₂.obj X ⟶ SSet.oneTruncation₂.obj (nerveFunctor₂.obj C)) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryStruct.comp f (forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev02₂✝ φ) = CategoryStruct.comp ((CategoryStruct.comp f (forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev01₂✝ φ)) ((CategoryStruct.comp f (forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev12₂✝ φ))) : X ⟶ 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 : Cat} (f : SSet.oneTruncation₂.obj X ⟶ SSet.oneTruncation₂.obj (nerveFunctor₂.obj C)) (hyp : ∀ (φ : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := ⋯ })), (CategoryStruct.comp f (forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev02₂✝ φ) = CategoryStruct.comp ((CategoryStruct.comp f (forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev01₂✝ φ)) ((CategoryStruct.comp f (forgetToReflQuiv.natIso.app C).hom).map (CategoryTheory.ev12₂✝ φ))) (n : (SimplexCategory.Truncated 2)ᵒᵖ) (a✝ : X.obj (Opposite.op (Opposite.unop n))) : (mk' f hyp).app n a✝ = mk.app (CategoryStruct.comp f (forgetToReflQuiv.natIso.hom.app C)) (Opposite.unop n) a✝

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

theorem CategoryTheory.toNerve₂.ext {X : SSet.Truncated 2} {C : Cat} (f : X ⟶ nerve₂ ↑C) (g : X ⟶ nerve₂ ↑C) (hyp : SSet.oneTruncation₂.map f = 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 : Cat} (f : X ⟶ nerveFunctor₂.obj C) (g : X ⟶ nerveFunctor₂.obj C) (hyp : SSet.oneTruncation₂.map f = SSet.oneTruncation₂.map g) : f = g

ER: This is dumb.

def CategoryTheory.nerve₂Adj.unit.component (X : SSet.Truncated 2) : X ⟶ nerveFunctor₂.obj (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) : SSet.oneTruncation₂.map (component X) = ReflQuiv.adj.unit.app (SSet.oneTruncation₂.obj X) ⋙rq (SSet.hoFunctor₂Obj.quotientFunctor X).toReflPrefunctor ⋙rq forgetToReflQuiv.natIso.inv.app (SSet.hoFunctor₂.obj X)

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

Equations

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

def CategoryTheory.nerve₂Adj : SSet.hoFunctor₂ ⊣ 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 : nerveFunctor₂.Faithful

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

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

Equations

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

def CategoryTheory.nerveAdjunction : SSet.hoFunctor ⊣ nerveFunctor

Equations

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

instance CategoryTheory.nerveFunctor.faithful : nerveFunctor.Faithful

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

instance CategoryTheory.nerveFunctor.full : nerveFunctor.Full

instance CategoryTheory.nerveCounit_isIso : IsIso nerveAdjunction.counit

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

Equations

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

instance CategoryTheory.instReflectiveSSetCatNerveFunctor_infinityCosmos : Reflective nerveFunctor

Equations

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

instance CategoryTheory.instHasColimitsCat_infinityCosmos : Limits.HasColimits Cat