Resolution

📁 Source: Mathlib/RepresentationTheory/Homological/Resolution.lean

Statistics

Metric	Count
Definitions barComplex, d, isoStandardComplex, barResolution, extIso, standardComplex, compForgetAugmentedIso, d, forget₂ToModuleCat, forget₂ToModuleCatHomotopyEquiv, xIso, ε, εToSingle₀, standardResolution, extIso, classifyingSpaceUniversalCover, cechNerveTerminalFromIso, cechNerveTerminalFromIsoCompForget, compForgetAugmented, toModule, extraDegeneracyAugmentedCechNerve, extraDegeneracyCompForgetAugmented, extraDegeneracyCompForgetAugmentedToModule	23
Theorems d_comp_diagonalSuccIsoFree_inv_eq, d_def, d_single, barResolution_complex, d_comp_ε, d_eq, d_of, forget₂ToModuleCatHomotopyEquiv_f_0_eq, instQuasiIsoNatεToSingle₀, quasiIso_forget₂_εToSingle₀, x_projective, εToSingle₀_comp_eq, classifyingSpaceUniversalCover_map, classifyingSpaceUniversalCover_obj	14
Total	37

Rep

Definitions

Name	Category	Theorems
barComplex 📖	CompOp	4 math math: barComplex.d_def, barResolution_complex, inhomogeneousCochains.d_eq, groupHomology.inhomogeneousChains.d_eq
barResolution 📖	CompOp	1 math math: barResolution_complex
standardComplex 📖	CompOp	7 math math: standardComplex.d_eq, standardComplex.εToSingle₀_comp_eq, standardComplex.quasiIso_forget₂_εToSingle₀, standardComplex.d_comp_ε, standardComplex.instQuasiIsoNatεToSingle₀, standardComplex.x_projective, barComplex.d_comp_diagonalSuccIsoFree_inv_eq
standardResolution 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
barResolution_complex 📖	mathematical	—	CategoryTheory.ProjectiveResolution.complex Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring barResolution barComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject

Rep.barComplex

Definitions

Name	Category	Theorems
d 📖	CompOp	3 math math: d_def, d_comp_diagonalSuccIsoFree_inv_eq, d_single
isoStandardComplex 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_comp_diagonalSuccIsoFree_inv_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory Rep.free Rep.diagonal d CategoryTheory.Iso.inv Rep.diagonalSuccIsoFree HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Action.instPreadditive ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex HomologicalComplex.d	—	Rep.free_ext AddRightCancelSemigroup.toIsRightCancelAdd d_single Fin.sum_univ_succ zero_add pow_one Finsupp.single_neg Finset.sum_congr map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Rep.diagonalSuccIsoFree_inv_hom_single_single map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Fin.partialProd_contractNth one_smul map_sum RingHomCompTriple.ids Rep.standardComplex.d_eq Rep.standardComplex.d_of pow_zero Finsupp.instIsRightCancelAdd Fin.partialProd_succ'
d_def 📖	mathematical	—	HomologicalComplex.d Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.barComplex d	—	ChainComplex.of_d
d_single 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.free ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom d Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finsupp.instAdd Finsupp.instAddZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid Finset.sum Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ Fin.fintype Fin.contractNth MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	RingHomCompTriple.ids LinearMap.comp.congr_simp map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Representation.finsupp_single Representation.ofMulAction_single map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Finset.sum_congr mul_one Finsupp.uncurry_single Finsupp.linearCombination_single one_mul smul_add one_smul

Rep.barResolution

Definitions

Name	Category	Theorems
extIso 📖	CompOp	—

Rep.standardComplex

Definitions

Name	Category	Theorems
compForgetAugmentedIso 📖	CompOp	—
d 📖	CompOp	2 math math: d_eq, d_of
forget₂ToModuleCat 📖	CompOp	2 math math: εToSingle₀_comp_eq, forget₂ToModuleCatHomotopyEquiv_f_0_eq
forget₂ToModuleCatHomotopyEquiv 📖	CompOp	2 math math: εToSingle₀_comp_eq, forget₂ToModuleCatHomotopyEquiv_f_0_eq
xIso 📖	CompOp	—
ε 📖	CompOp	2 math math: d_comp_ε, forget₂ToModuleCatHomotopyEquiv_f_0_eq
εToSingle₀ 📖	CompOp	3 math math: εToSingle₀_comp_eq, quasiIso_forget₂_εToSingle₀, instQuasiIsoNatεToSingle₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_comp_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommRing.toRing CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Action.instPreadditive ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HomologicalComplex.d ε Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Action.instZeroHom	—	Action.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.hom_ext LinearMap.ext ModuleCat.instHasZeroObject forget₂ToModuleCatHomotopyEquiv_f_0_eq HomologicalComplex.Hom.comm' CategoryTheory.Limits.comp_zero LinearMap.ext_iff ModuleCat.hom_ext_iff
d_eq 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory HomologicalComplex.X Rep Action.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Action.instPreadditive ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex HomologicalComplex.d ModuleCat.ofHom Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule d	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids ModuleCat.Algebra.instSMulCommClassCarrier LinearMap.comp.congr_simp Fin.strictMono_succAbove AlgebraicTopology.alternatingFaceMapComplex_obj_d Finset.sum_congr Int.cast_smul_eq_zsmul Int.cast_pow Int.cast_neg Int.cast_one Action.sum_hom ModuleCat.hom_sum LinearMap.coe_sum Finset.sum_apply Finsupp.mapDomain_single Finsupp.smul_single mul_one d_of
d_of 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike d Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Finset.sum Finset.univ Fin.fintype Fin.succAbove Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Finsupp.sum_single_index zero_smul one_smul
forget₂ToModuleCatHomotopyEquiv_f_0_eq 📖	mathematical	—	HomologicalComplex.Hom.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne forget₂ToModuleCat CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ ModuleCat.instHasZeroObject Rep Action.instCategory CategoryTheory.forget₂ Action.HomSubtype LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring HomotopyEquiv.hom forget₂ToModuleCatHomotopyEquiv CategoryTheory.Functor.map Rep.ofMulAction Pi.mulAction Monoid.toMulAction ε	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.instHasZeroObject Finsupp.lhom_ext HomologicalComplex.eqToHom_f CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId CategoryTheory.Limits.Types.instSubsingletonTerminalType SimplexCategory.const_eq_id Unique.eq_default Finsupp.mapDomain_single Finsupp.single_apply Finsupp.linearCombination_single mul_one
instQuasiIsoNatεToSingle₀ 📖	mathematical	—	QuasiIso Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Action.instPreadditive ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring εToSingle₀ CategoryTheory.CategoryWithHomology.hasHomology Action.instHasZeroMorphisms CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.instHasHomologyObjSingle	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.instHasHomologyObjSingle CategoryTheory.Functor.preservesZeroMorphisms_of_additive Action.forget₂_additive HomologicalComplex.quasiIso_map_iff_of_preservesHomology CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.forget₂_faithful CategoryTheory.Functor.reflectsEpimorphisms_of_faithful quasiIso_forget₂_εToSingle₀
quasiIso_forget₂_εToSingle₀ 📖	mathematical	—	QuasiIso ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj HomologicalComplex Rep Action.instCategory Action.instPreadditive HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.forget₂ Action.HomSubtype LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV Action.forget₂_preservesZeroMorphisms Rep.standardComplex ChainComplex ChainComplex.single₀ CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.map εToSingle₀ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.instHasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.instHasHomologyObjSingle HomotopyEquiv.quasiIso_hom quasiIso_of_comp_right Action.forget₂_preservesZeroMorphisms CategoryTheory.Abelian.hasZeroObject quasiIso_of_isIso CategoryTheory.NatIso.hom_app_isIso εToSingle₀_comp_eq
x_projective 📖	mathematical	—	CategoryTheory.Projective Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Action.instPreadditive ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex	—	Rep.diagonal_succ_projective
εToSingle₀_comp_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj Rep Action.instCategory Action.instPreadditive CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.forget₂ Action.HomSubtype LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV Action.instConcreteCategoryHomSubtypeV Action.hasForgetToV Action.forget₂_preservesZeroMorphisms Rep.standardComplex ChainComplex ChainComplex.single₀ CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.comp HomologicalComplex.single ModuleCat.instHasZeroObject CategoryTheory.Functor.map εToSingle₀ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.singleMapHomologicalComplex HomotopyEquiv.hom forget₂ToModuleCat forget₂ToModuleCatHomotopyEquiv	—	AddRightCancelSemigroup.toIsRightCancelAdd Action.forget₂_preservesZeroMorphisms ModuleCat.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomologicalComplex.to_single_hom_ext HomologicalComplex.singleMapHomologicalComplex_hom_app_self CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id forget₂ToModuleCatHomotopyEquiv_f_0_eq

Rep.standardResolution

Definitions

Name	Category	Theorems
extIso 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
classifyingSpaceUniversalCover 📖	CompOp	2 math math: classifyingSpaceUniversalCover_map, classifyingSpaceUniversalCover_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classifyingSpaceUniversalCover_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Action CategoryTheory.types Action.instCategory classifyingSpaceUniversalCover Action.ofMulAction Pi.mulAction SimplexCategory.len Opposite.unop Monoid.toMulAction DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
classifyingSpaceUniversalCover_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Action CategoryTheory.types Action.instCategory classifyingSpaceUniversalCover Action.ofMulAction Pi.mulAction SimplexCategory.len Opposite.unop Monoid.toMulAction	—	—

classifyingSpaceUniversalCover

Definitions

Name	Category	Theorems
cechNerveTerminalFromIso 📖	CompOp	—
cechNerveTerminalFromIsoCompForget 📖	CompOp	—
compForgetAugmented 📖	CompOp	—
extraDegeneracyAugmentedCechNerve 📖	CompOp	—
extraDegeneracyCompForgetAugmented 📖	CompOp	—
extraDegeneracyCompForgetAugmentedToModule 📖	CompOp	—

classifyingSpaceUniversalCover.compForgetAugmented

Definitions

Name	Category	Theorems
toModule 📖	CompOp	—

---

← Back to Index