OAI/CategoryTheory/Thomason/Simplicial/
3018 declarations, 0 contain sorry, 0 declared as axioms; 58 files
Files
- AcyclicKanSimplexLifting.lean 47 declarations
- BarycentricSortedCoordinates.lean 67 declarations
- BarycentricSupportInclusion.lean 40 declarations
- CanonicalExtensionAnodyneHorn.lean 53 declarations
- CanonicalExtensionCartesian.lean 90 declarations
- CanonicalExtensionImageLattice.lean 62 declarations
- CobaseChangeCellularClosure.lean 37 declarations
- ConstructedExtensionLocalizer.lean 58 declarations
- ConstructedPosetCosieves.lean 57 declarations
- DoubleSubdivisionStability.lean 3 declarations
- ExhaustionWeakEquivalence.lean 52 declarations
- FaceSimplexLift.lean 95 declarations
- FiniteKanBaseChangeApproximation.lean 21 declarations
- FinitePosetCoordinates.lean 67 declarations
- FinitePosetUnitInduction.lean 2 declarations
- FinitePosetUnitReduction.lean 19 declarations
- FiniteRelativeRealizationLifting.lean 38 declarations
- FiniteSingularRelativeLifting.lean 41 declarations
- FixedInternalPathMaps.lean 73 declarations
- HomotopyFiberPathEquivalence.lean 47 declarations
- HornWeakEquivalences.lean 59 declarations
- InfiniteExtensionBaseChange.lean 49 declarations
- InfiniteExtensionKan.lean 79 declarations
- KanBaseChangeExhaustion.lean 36 declarations
- KanContractedFamilyLifting.lean 48 declarations
- KanFiberComponentTransport.lean 48 declarations
- KanFinitePosetExtension.lean 29 declarations
- KanRealizedEdgeComposition.lean 58 declarations
- KanSimplexContinuousFibers.lean 47 declarations
- LastVertexWeakEquivalence.lean 61 declarations
- LoopDimensionShift.lean 92 declarations
- NonsingularFaceCarriers.lean 85 declarations
- PosetSieveNaturality.lean 16 declarations
- PosetSubcomplexHomotopy.lean 24 declarations
- RealizationCellClosure.lean 56 declarations
- RealizationSubcomplexSemantics.lean 60 declarations
- RealizationTopology.lean 74 declarations
- RealizedSimplexWeakEquivalences.lean 58 declarations
- SieveFiberPresentation.lean 51 declarations
- SimplexCubeRetract.lean 57 declarations
- SimplicialApproximation.lean 21 declarations
- SimplicialSpanFactorization.lean 76 declarations
- SingularAcyclicFibers.lean 19 declarations
- SingularCounitSurjectivity.lean 56 declarations
- SingularCubeNaturality.lean 73 declarations
- SingularKanComplex.lean 76 declarations
- SingularPathSpaceAdjunction.lean 49 declarations
- SkeletalWeakEquivalences.lean 77 declarations
- SubcomplexFaceLifting.lean 35 declarations
- SubdivisionFaceImages.lean 61 declarations
- SubdivisionUnions.lean 56 declarations
- SubdivisionWeakLifting.lean 51 declarations
- TerminalConeUniversal.lean 75 declarations
- TopologicalDeformationTransport.lean 52 declarations
- TruncatedLocalPresentability.lean 38 declarations
- TruncationCongruence.lean 34 declarations
- TruncationQuotientComposition.lean 59 declarations
- WeakPathSurjectivity.lean 54 declarations