feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor

[digama0]

This defines SSet.hoFunctor, which constructs a category from a simplicial set.

Co-Authored-By: Emily Riehl [email protected] and Pietro Monticone [email protected]

---

• [x] depends on: #16779
• [x] depends on: #16780
• [x] depends on: #16781

• Prerequisite for #16784.

[github-actions[bot]]

PR summary 83b5747768

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (new file)	842

---

Declarations diff

+ Functor.congruence_homRel + Functor.homRel + Functor.homRel_iff + HoRel₂ + HoRel₂.mk' + HomotopyCategory.lift_unique' + OneTruncation₂ + OneTruncation₂.Hom + OneTruncation₂.hom_ext + OneTruncation₂.id_edge + OneTruncation₂.nerveEquiv + OneTruncation₂.nerveHomEquiv + OneTruncation₂.ofNerve₂ + OneTruncation₂.ofNerve₂.natIso + ReflQuiver.homOfEq_id + _root_.SSet.Truncated.HomotopyCategory + _root_.SSet.Truncated.HomotopyCategory.quotientFunctor + compClosure.congruence + congr_hom + congr_obj + equivOfIso + ev01₂ + ev02₂ + ev0₂ + ev12₂ + ev1₂ + ev2₂ + functor_homRel_eq_compClosure_eqvGen + hoFunctor + hoFunctor₂ + hoFunctor₂_naturality + homEquivOfIso + homOfEq + homOfEq_injective + homOfEq_map + homOfEq_map_homOfEq + homOfEq_rfl + homOfEq_trans + hom_map_inv_map_of_iso + hom_obj_inv_obj_of_iso + instance (S : SSet.Truncated 2) : ReflQuiver (OneTruncation₂ S) + instance (V : SSet.Truncated.{u} 2) : Category.{u} (V.HomotopyCategory) + inv_map_hom_map_of_iso + inv_obj_hom_obj_of_iso + isoOfQuivIso + mapHomotopyCategory + oneTruncation₂ + δ0₂ + δ1₂ + δ2₂ + δ_naturality_apply + δ₂ + δ₂_one_comp_σ₂_zero + δ₂_zero_comp_σ₂_zero + ι0₂ + ι1₂ + ι2₂ + σ_naturality_apply + σ₂ ++ ext' ++ isoOfEquiv

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joelriou]

I would suggest moving the file AlgebraicTopology.HomotopyCat to AlgebraicTopology.SimplicialSet.HomotopyCat (and then SimplicalSet should become SimplicialSet.Basic).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#16779~~
• ~~leanprover-community/mathlib4#16780~~
• ~~leanprover-community/mathlib4#16781~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

Note: Moving files to SimplicialSet.* should be done in a separate PR doing only that.

[emilyriehl]

Note: Moving files to SimplicialSet.* should be done in a separate PR doing only that.

See PR #17620.

[emilyriehl]

I think the new file can be wrapped in a namespace SSet.

@jcommelin to clarify, you were suggesting moving HomotopyCat.lean out of the CategoryTheory namespace and into the SSet namespace?

[jcommelin]

Sorry for being unclear. What I had in mind was to nest the namespaces:

namespace CategoryTheory
namespace SSet

...

because almost all the names start with SSet. already.

[joelriou]

I would still insist that there is no reason to duplicate the construction. Before taking the quotient category, the two constructions are defeq. HoRel₂ and HoRel (for the truncation) are obviously not defeq because there are separate types, but it would a very small effort to define HoRel in terms of HoRel₂. What I suggest is define first the homotopy category for 2-truncated simplicial sets. Define the homotopy category of a simplicial set by applying the previous construction to (SimplexCategory.Truncated.inclusion 2).op ⋙ X. Then, you may provide a nice helper API for the second construction if you want to hide the internals. Please note that the truncation has good definitional properties.

[emilyriehl]

@joelriou this makes the cuts that you requested and is now ready for review.

[emilyriehl]

Two comments for @joelriou:

1. For whatever reason I have to write SSet.Truncated.HomotopyCategory.quotientFunctor V even in the SSet.Truncated namespace.
2. I'm not sure how much of this file should be in the Truncated namespace. Eg. right now HoRel₂ is in the Truncated namespace while OneTruncation₂ is not. I'm not sure either of these choices is correct.

[emilyriehl]

I may have figured out the issue: most of this file is actually in the CategoryTheory.SSet.Truncated namespace. Which further suggests I've made the namespaces all wrong.

[joelriou]

I may have figured out the issue: most of this file is actually in the CategoryTheory.SSet.Truncated namespace. Which further suggests I've made the namespaces all wrong.

Yes, it should be SSet.Truncated rather than CategoryTheory.SSet.Truncated.

[emilyriehl]

@joelriou the current version adds the constructions of isomorphisms in Quiv and ReflQuiv as requested.

Then the HomotopyCat file contains two versions of OneTruncation₂.ofNerve₂.natIso for comparison. The first version, starting line 119, is the one that uses the new infrastructure. Note, however, it causes a universe error I wasn't able to fix (though perhaps @digama0 can figure this out). The old version follows starting at line 184. Note I turned around the direction of the initial equivalence, we seemed to help, marginally.

[joelriou]

After these small modifications, I think the PR will be mostly ready to go!

[emilyriehl]

Thanks @joelriou. I really appreciate all your efforts and am sorry this has proven so painful to review! (I'm working now on the final PR in this series to work around the defs I know you won't like...)

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Build failed:

• Build

[joelriou]

Could you merge with master and try to fix the build?

[joelriou]

bors d-

[emilyriehl]

Sorry about that. I don't understand what happened. But it should be fixed now.

[joelriou]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style