-
Notifications
You must be signed in to change notification settings - Fork 316
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(AlgebraicTopology/Nerve): nerve is 2-coskeletal #16782
base: master
Are you sure you want to change the base?
Conversation
Co-Authored-By: Emily Riehl <[email protected]>
PR summary a278788f95
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.AlgebraicTopology.SimplicialSet | 785 | 791 | +6 (+0.76%) |
Mathlib.AlgebraicTopology.Nerve | 790 | 796 | +6 (+0.76%) |
Import changes for all files
Files | Import difference |
---|---|
6 filesMathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.AlgebraicTopology.SingularSet Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.AlgebraicTopology.ExtraDegeneracy |
3 |
Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialCategory.Basic |
5 |
4 filesMathlib.AlgebraicTopology.SimplicialSet Mathlib.AlgebraicTopology.Quasicategory Mathlib.AlgebraicTopology.Nerve Mathlib.AlgebraicTopology.KanComplex |
6 |
Declarations diff
+ Fin.hom_succ
+ Fin.le_succ
+ Hom.ext
+ Truncated.uliftFunctor
+ ar
+ ar'
+ ar'succ
+ const_fac_thru_zero
+ cosk2Iso
+ cosk2NatIso.component
+ cosk2NatTrans
+ cosk2RightExtension.component.hom.iso
+ cosk2RightExtension.hom
+ cosk2RightExtension.hom_isIso
+ coskAdj
+ coskAdj.reflective
+ coskeleton.faithful
+ coskeleton.full
+ coskeleton.fullyFaithful
+ coskeleton_reflective
+ eq_const_of_zero
+ eq_const_to_zero
+ eq_of_one_to_one
+ eq_of_one_to_two
+ exists_eq_const_of_zero
+ fact.map.arr
+ fact.obj.arr
+ inclusion.fullyFaithful
+ isPointwiseRightKanExtension
+ isPointwiseRightKanExtension.isUniversal
+ isPointwiseRightKanExtensionAt
+ isRightKanExtension
+ mkOfLe
+ mkOfLeComp
+ mkOfSucc
+ nerveFunctor₂
+ nerveRightExtension
+ nerveRightExtension.coneAt
+ nerve₂
+ nerve₂RestrictedIso
+ nerve₂_restrictedNerve
+ pt
+ pt'
+ ran.lift
+ ran.lift'
+ ran.lift.eq
+ ran.lift.eq₂
+ ran.lift.map
+ skAdj
+ skAdj.coreflective
+ skeleton.faithful
+ skeleton.full
+ skeleton.fullyFaithful
+ skeleton_reflective
+ strArr.homEv
+ strArr.homEv.map
+ strArr.homEvSucc
+ Δ
+ Δ.ι
++ truncation
-- sk
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.
Co-authored-by: Kim Morrison <[email protected]>
Co-Authored-By: Emily Riehl <[email protected]>
This PR/issue depends on: |
The
nerve
functor is 2-coskeletal. This is a major lemma in the construction of the nerve adjunction.Co-Authored-By: Emily Riehl [email protected] and Pietro Monticone [email protected]