FiniteCyclic

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

Statistics

Metric	Count
Definitions chainComplexFunctor, moduleCatChainComplex, moduleCatCochainComplex, normHomCompSub, resolution, π, subCompNormHom, coinvariantsEquiv	8
Theorems chainComplexFunctor_map_f, chainComplexFunctor_obj, range_applyAsHom_sub_eq_ker_linearCombination, range_applyAsHom_sub_eq_ker_norm, range_norm_eq_ker_applyAsHom_sub, π_f, resolution_complex, resolution_quasiIso, resolution_π, coinvariantsKer_eq_range, coinvariantsKer_leftRegular_eq_ker	11
Total	19

Rep.FiniteCyclicGroup

Definitions

Name	Category	Theorems
chainComplexFunctor 📖	CompOp	5 math math: chainComplexFunctor_obj, chainComplexFunctor_map_f, resolution_complex, resolution_quasiIso, resolution.π_f
moduleCatChainComplex 📖	CompOp	2 math math: coinvariantsTensorResolutionIso_inv_f_hom_apply, coinvariantsTensorResolutionIso_hom_f_hom_apply
moduleCatCochainComplex 📖	CompOp	2 math math: homResolutionIso_hom_f_hom_apply, homResolutionIso_inv_f_hom_apply_hom_hom_apply
normHomCompSub 📖	CompOp	—
resolution 📖	CompOp	6 math math: resolution_complex, homResolutionIso_hom_f_hom_apply, homResolutionIso_inv_f_hom_apply_hom_hom_apply, coinvariantsTensorResolutionIso_inv_f_hom_apply, resolution_π, coinvariantsTensorResolutionIso_hom_f_hom_apply
subCompNormHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chainComplexFunctor_map_f 📖	mathematical	—	HomologicalComplex.Hom.f Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup 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 Nat.instOne HomologicalComplex.alternatingConst Rep.norm Quiver.Hom CommMonoid.toMonoid CommGroup.toCommMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id ComplexShape.instDecidableRelRelDown ComplexShape.down_nat_odd_add CategoryTheory.Functor.map ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd chainComplexFunctor	—	ComplexShape.down_nat_odd_add AddRightCancelSemigroup.toIsRightCancelAdd
chainComplexFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Action.instCategory ModuleCat ModuleCat.moduleCategory ChainComplex Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd chainComplexFunctor HomologicalComplex.alternatingConst Rep.norm Quiver.Hom CommMonoid.toMonoid CommGroup.toCommMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id ComplexShape.instDecidableRelRelDown ComplexShape.down_nat_odd_add	—	AddRightCancelSemigroup.toIsRightCancelAdd
resolution_complex 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	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 Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring resolution CategoryTheory.Functor.obj ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup chainComplexFunctor Rep.leftRegular	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject
resolution_quasiIso 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	QuasiIso 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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory chainComplexFunctor Rep.leftRegular ChainComplex.single₀ CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring resolution.π CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.instHasHomologyObjSingle	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.instHasHomologyObjSingle ChainComplex.quasiIsoAt₀_iff CategoryTheory.ShortComplex.quasiIso_iff_of_zeros' CategoryTheory.Functor.reflects_exact_of_faithful Action.forget_preservesZeroMorphisms Action.instFaithfulForget RingHomSurjective.ids ComplexShape.down_nat_odd_add HomologicalComplex.mkHomToSingle_f CategoryTheory.Category.comp_id zero_add CategoryTheory.ShortComplex.map.congr_simp Representation.isTrivial_def Representation.instIsTrivialTrivial leftRegular.range_applyAsHom_sub_eq_ker_linearCombination Finite.of_fintype Rep.epi_iff_surjective mul_one Finsupp.sum_single_index quasiIsoAt_iff_exactAt' ChainComplex.exactAt_succ_single_obj HomologicalComplex.exactAt_iff' ChainComplex.prev ChainComplex.next_nat_succ CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker LinearMap.range.congr_simp Nat.even_add_one Nat.not_even_iff_odd leftRegular.range_norm_eq_ker_applyAsHom_sub Nat.odd_add_one Nat.not_odd_iff_even leftRegular.range_applyAsHom_sub_eq_ker_norm
resolution_π 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	CategoryTheory.ProjectiveResolution.π 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 Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring resolution resolution.π	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject

Rep.FiniteCyclicGroup.leftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_applyAsHom_sub_eq_ker_linearCombination 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	LinearMap.range ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CommMonoid.toMonoid CommGroup.toCommMonoid Rep.leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isModule Finsupp.module Semiring.toModule RingHom.id RingHomSurjective.ids ModuleCat.Hom.hom Action.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id LinearMap.ker NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.linearCombination AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomSurjective.ids Representation.FiniteCyclicGroup.coinvariantsKer_eq_range
range_applyAsHom_sub_eq_ker_norm 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	LinearMap.range ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory CommMonoid.toMonoid CommGroup.toCommMonoid Rep.leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom Action.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id LinearMap.ker Rep.norm	—	RingHomSurjective.ids Representation.ker_leftRegular_norm_eq range_applyAsHom_sub_eq_ker_linearCombination Finite.of_fintype
range_norm_eq_ker_applyAsHom_sub 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	LinearMap.range ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.leftRegular Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ModuleCat.Hom.hom Action.Hom.hom Rep.norm LinearMap.ker CommMonoid.toMonoid CommGroup.toCommMonoid Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Action.instSubHom ModuleCat.instPreadditive Rep.applyAsHom CategoryTheory.CategoryStruct.id	—	le_antisymm RingHomSurjective.ids Representation.self_norm_apply sub_self Finsupp.ext Finset.sum_congr LinearMap.coe_sum Finset.sum_apply Representation.ofMulAction_single mul_one Finsupp.coe_finset_sum Finsupp.univ_sum_single_apply' Representation.apply_eq_of_leftRegular_eq_of_generator

Rep.FiniteCyclicGroup.resolution

Definitions

Name	Category	Theorems
π 📖	CompOp	3 math math: Rep.FiniteCyclicGroup.resolution_quasiIso, Rep.FiniteCyclicGroup.resolution_π, π_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
π_f 📖	mathematical	—	HomologicalComplex.Hom.f Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup 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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory Rep.FiniteCyclicGroup.chainComplexFunctor Rep.leftRegular ChainComplex.single₀ CategoryTheory.Abelian.hasZeroObject Action.instAbelian ModuleCat.abelian Rep.trivial Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex HomologicalComplex.single CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom HomologicalComplex.XIsoOfEq HomologicalComplex.alternatingConst Rep.norm CommMonoid.toMonoid CommGroup.toCommMonoid Action.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id ComplexShape.instDecidableRelRelDown ComplexShape.down_nat_odd_add Rep.leftRegularHom ModuleCat.carrier Action.V AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CategoryTheory.Iso.inv HomologicalComplex.singleObjXIsoOfEq CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject

Representation.FiniteCyclicGroup

Definitions

Name	Category	Theorems
coinvariantsEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsKer_eq_range 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	Representation.Coinvariants.ker DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap.range CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap LinearMap.instSub DFunLike.coe Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.id	—	le_antisymm RingHomSurjective.ids Submodule.span_le mem_powers_iff_mem_zpowers map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_self pow_zero map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass map_pow Representation.apply_sub_id_partialSum_eq Representation.Coinvariants.sub_mem_ker
coinvariantsKer_leftRegular_eq_ker 📖	mathematical	—	Representation.Coinvariants.ker Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Representation.leftRegular LinearMap.ker Finsupp.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom.id Finsupp.linearCombination AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	le_antisymm Submodule.span_le RingHomInvPair.ids mul_one Finsupp.sum_fintype Finset.sum_congr Representation.ofMulAction_apply Finset.sum_sub_distrib Finset.sum_bijective Group.mulLeft_bijective Finsupp.ext Finsupp.sum_sub Finsupp.sum_single Finsupp.coe_sum Finsupp.sum_apply' Finsupp.single_eq_same sub_zero Finsupp.single_eq_of_ne Finsupp.sum_fun_zero Submodule.finsuppSum_mem Representation.Coinvariants.mem_ker_of_eq Representation.ofMulAction_single

---

← Back to Index