Commit 2024-12-20 00:42 0065e8d9

View on Github →

feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor (#16783) This defines SSet.hoFunctor, which constructs a category from a simplicial set. Co-Authored-By: Emily Riehl eriehl@jhu.edu, Pietro Monticone 38562595+pitmonticone@users.noreply.github.com, and Joël Riou https://github.com/joelriou

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

added theorem SSet.δ_naturality_apply

added theorem SSet.σ_naturality_apply

Created Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

added structure SSet.OneTruncation₂.Hom

added theorem SSet.OneTruncation₂.hom_ext

added theorem SSet.OneTruncation₂.id_edge

added def SSet.OneTruncation₂.nerveEquiv

added def SSet.OneTruncation₂.nerveHomEquiv

added def SSet.OneTruncation₂.ofNerve₂.natIso

added def SSet.OneTruncation₂.ofNerve₂

added def SSet.OneTruncation₂

added theorem SSet.Truncated.HoRel₂.mk'

added inductive SSet.Truncated.HoRel₂

added theorem SSet.Truncated.HomotopyCategory.lift_unique'

added def SSet.Truncated.HomotopyCategory.quotientFunctor

added def SSet.Truncated.HomotopyCategory

added def SSet.Truncated.ev01₂

added def SSet.Truncated.ev02₂

added def SSet.Truncated.ev0₂

added def SSet.Truncated.ev12₂

added def SSet.Truncated.ev1₂

added def SSet.Truncated.ev2₂

added def SSet.Truncated.hoFunctor₂

added theorem SSet.Truncated.hoFunctor₂_naturality

added def SSet.Truncated.mapHomotopyCategory

added def SSet.Truncated.δ0₂

added def SSet.Truncated.δ1₂

added def SSet.Truncated.δ2₂

added def SSet.Truncated.ι0₂

added def SSet.Truncated.ι1₂

added def SSet.Truncated.ι2₂

added def SSet.hoFunctor

added def SSet.oneTruncation₂

added theorem SSet.δ₂_one_comp_σ₂_zero

added theorem SSet.δ₂_zero_comp_σ₂_zero

Modified Mathlib/CategoryTheory/Category/Quiv.lean

added def CategoryTheory.Quiv.equivOfIso

added def CategoryTheory.Quiv.homEquivOfIso

added theorem CategoryTheory.Quiv.homOfEq_map_homOfEq

added theorem CategoryTheory.Quiv.hom_map_inv_map_of_iso

added theorem CategoryTheory.Quiv.hom_obj_inv_obj_of_iso

added theorem CategoryTheory.Quiv.inv_map_hom_map_of_iso

added theorem CategoryTheory.Quiv.inv_obj_hom_obj_of_iso

added def CategoryTheory.Quiv.isoOfEquiv

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

deleted theorem CategoryTheory.ReflQuiv.forgetToQuiv.Faithful

added def CategoryTheory.ReflQuiv.isoOfEquiv

added def CategoryTheory.ReflQuiv.isoOfQuivIso

Modified Mathlib/CategoryTheory/Quotient.lean

added def CategoryTheory.Functor.homRel

added theorem CategoryTheory.Functor.homRel_iff

added theorem CategoryTheory.Quotient.compClosure.congruence

added theorem CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen

Modified Mathlib/Combinatorics/Quiver/Basic.lean

added def Quiver.homOfEq

added theorem Quiver.homOfEq_injective

added theorem Quiver.homOfEq_rfl

added theorem Quiver.homOfEq_trans

Modified Mathlib/Combinatorics/Quiver/Prefunctor.lean

added theorem Prefunctor.congr_hom

added theorem Prefunctor.congr_obj

added theorem Prefunctor.ext'

added theorem Prefunctor.homOfEq_map

Modified Mathlib/Combinatorics/Quiver/ReflQuiver.lean

added theorem CategoryTheory.ReflPrefunctor.ext'

added theorem CategoryTheory.ReflQuiver.homOfEq_id