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_apply, d_comp_ε, d_eq, d_of, d_single, forget₂ToModuleCatHomotopyEquiv_f_0_eq, instQuasiIsoNatεToSingle₀, quasiIso_forget₂_εToSingle₀, x_projective, εToSingle₀_comp_eq, classifyingSpaceUniversalCover_map, classifyingSpaceUniversalCover_obj	16
Total	39

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	8 math math: standardComplex.d_eq, standardComplex.εToSingle₀_comp_eq, standardComplex.quasiIso_forget₂_εToSingle₀, standardComplex.d_comp_ε, standardComplex.instQuasiIsoNatεToSingle₀, standardComplex.x_projective, standardComplex.d_apply, barComplex.d_comp_diagonalSuccIsoFree_inv_eq
standardResolution 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
barResolution_complex 📖	mathematical	—	CategoryTheory.ProjectiveResolution.complex Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory instHasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive trivial Ring.toAddCommGroup CommRing.toRing Semiring.toModule barResolution barComplex	—	instHasZeroObject

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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.free Rep.diagonal CommRing.toRing d CategoryTheory.Iso.inv Ring.toSemiring Rep.diagonalSuccIsoFree HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.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 Fin.partialProd_succ' CategoryTheory.Iso.trans_assoc CategoryTheory.Category.assoc d_single Rep.mkIso_inv_hom_apply map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass RingHomInvPair.ids Representation.Equiv.instLinearEquivClass Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Finset.sum_congr Representation.IntertwiningMap.instLinearMapClass Representation.linearizeTrivialIso_symm_apply mul_one one_mul Action.diagonalSuccIsoTensorTrivial_inv_hom_apply one_smul Rep.standardComplex.d_apply Fin.partialProd_contractNth Fin.sum_univ_succ zero_add pow_one Finsupp.single_neg Rep.standardComplex.d_of pow_zero
d_def 📖	mathematical	—	HomologicalComplex.d Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.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 Representation.IntertwiningMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.free AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom d Finsupp.single Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	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	4 math math: d_eq, d_of, d_apply, d_single
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_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring HomologicalComplex.X Rep Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom HomologicalComplex.d LinearMap 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	—	AddRightCancelSemigroup.toIsRightCancelAdd Representation.IntertwiningMap.toLinearMap_apply d_eq
d_comp_ε 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Rep CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Category.toCategoryStruct Rep.instCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.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 CommRing.toRing Semiring.toModule HomologicalComplex.d ε Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Rep.instZeroHom	—	Rep.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Representation.IntertwiningMap.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	—	Representation.IntertwiningMap.toLinearMap Rep.V CommSemiring.toSemiring CommRing.toCommSemiring HomologicalComplex.X Rep Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Rep.Hom.hom HomologicalComplex.d d	—	Finsupp.lhom_ext' AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext_ring RingHomCompTriple.ids Fin.strictMono_succAbove LinearMap.comp.congr_simp AlgebraicTopology.alternatingFaceMapComplex_obj_d Finset.sum_congr Int.cast_smul_eq_zsmul Int.cast_pow Int.cast_neg Int.cast_one Representation.IntertwiningMap.sum_apply Representation.linearizeMap_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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Finsupp.sum_single_index zero_smul one_smul
d_single 📖	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 Finset.sum Finset.univ Fin.fintype Fin.succAbove Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	mul_one smul_eq_mul Finsupp.smul_single map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass d_of Finset.smul_sum Finset.sum_congr
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 CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory CategoryTheory.forget₂ Representation.IntertwiningMap Rep.V AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Rep.hasForgetToModuleCat Rep.trivial Ring.toAddCommGroup Semiring.toModule 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 Unique.instSubsingleton SimplexCategory.const_eq_id Unique.eq_default Finsupp.mapDomain_single Finsupp.single_apply Finsupp.linearCombination_single mul_one
instQuasiIsoNatεToSingle₀ 📖	mathematical	—	QuasiIso Rep CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.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₀ Rep.instHasZeroObject Rep.trivial Ring.toAddCommGroup CommRing.toRing Semiring.toModule εToSingle₀ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian Rep.instAbelian HomologicalComplex.sc HomologicalComplex.instHasHomologyObjSingle	—	AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.instHasHomologyObjSingle CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier HomologicalComplex.quasiIso_map_iff_of_preservesHomology CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits Rep.preservesLimits_forget CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits Rep.preservesColimits_forget CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Functor.reflectsMonomorphisms_of_faithful Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier 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 CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory Rep.instPreadditive HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.forget₂ Representation.IntertwiningMap Rep.V AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Rep.hasForgetToModuleCat CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier Rep.standardComplex ChainComplex ChainComplex.single₀ Rep.instHasZeroObject Rep.trivial Ring.toAddCommGroup Semiring.toModule CategoryTheory.Functor.map εToSingle₀ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ModuleCat.abelian HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.instHasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.instHasHomologyObjSingle HomotopyEquiv.quasiIso_hom quasiIso_of_comp_right CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier Rep.instHasZeroObject quasiIso_of_isIso CategoryTheory.NatIso.hom_app_isIso εToSingle₀_comp_eq
x_projective 📖	mathematical	—	CategoryTheory.Projective Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Rep.standardComplex	—	—
ε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 CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory Rep.instPreadditive CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.forget₂ Representation.IntertwiningMap Rep.V AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Rep.hasForgetToModuleCat CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier Rep.standardComplex ChainComplex ChainComplex.single₀ Rep.instHasZeroObject Rep.trivial Ring.toAddCommGroup Semiring.toModule 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 CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier ModuleCat.instHasZeroObject Rep.instHasZeroObject HomologicalComplex.to_single_hom_ext HomologicalComplex.singleMapHomologicalComplex_hom_app_self 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