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_inv_f_hom_apply_hom_toFun, homResolutionIso_hom_f_hom_apply
normHomCompSub 📖	CompOp	—
resolution 📖	CompOp	6 math math: homResolutionIso_inv_f_hom_apply_hom_toFun, resolution_complex, homResolutionIso_hom_f_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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.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 Rep.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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.instCategory ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.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 Rep.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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.instCategory Rep.instHasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive Rep.trivial Ring.toAddCommGroup CommRing.toRing Semiring.toModule 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	—	Rep.instHasZeroObject
resolution_quasiIso 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	QuasiIso Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup 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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory chainComplexFunctor Rep.leftRegular CommRing.toRing ChainComplex.single₀ Rep.instHasZeroObject Rep.trivial Ring.toAddCommGroup Semiring.toModule resolution.π 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 ChainComplex.quasiIsoAt₀_iff CategoryTheory.ShortComplex.quasiIso_iff_of_zeros' CategoryTheory.Functor.reflects_exact_of_faithful CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier ComplexShape.down_nat_odd_add HomologicalComplex.mkHomToSingle_f CategoryTheory.Category.comp_id zero_add RingHomSurjective.ids CategoryTheory.ShortComplex.map.congr_simp RingHomCompTriple.ids Representation.isTrivial_def Rep.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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.instCategory Rep.instHasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive Rep.trivial Ring.toAddCommGroup CommRing.toRing Semiring.toModule resolution resolution.π	—	AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject

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 Rep.V Ring.toSemiring CommRing.toRing CommMonoid.toMonoid CommGroup.toCommMonoid Rep.leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.hV1 Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Rep.hV2 Finsupp.module Semiring.toModule RingHom.id RingHomSurjective.ids Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.instSubHom 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 Rep.V Ring.toSemiring CommRing.toRing CommMonoid.toMonoid CommGroup.toCommMonoid Rep.leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id LinearMap.ker Rep.norm	—	RingHomSurjective.ids range_applyAsHom_sub_eq_ker_linearCombination Finite.of_fintype Representation.ker_leftRegular_norm_eq
range_norm_eq_ker_applyAsHom_sub 📖	mathematical	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	LinearMap.range Rep.V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Rep.leftRegular CommRing.toRing AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Representation.IntertwiningMap.toLinearMap Rep.ρ Rep.Hom.hom Rep.norm LinearMap.ker Ring.toSemiring CommMonoid.toMonoid CommGroup.toCommMonoid Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id	—	le_antisymm RingHomSurjective.ids Rep.applyAsHom_apply Representation.self_norm_apply sub_self Finsupp.ext Representation.apply_eq_of_leftRegular_eq_of_generator RingHomCompTriple.ids Finset.sum_congr LinearMap.coe_sum Finset.sum_apply Representation.ofMulAction_single mul_one Finsupp.coe_finset_sum Finsupp.univ_sum_single_apply'

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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup 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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory Rep.FiniteCyclicGroup.chainComplexFunctor Rep.leftRegular CommRing.toRing ChainComplex.single₀ Rep.instHasZeroObject Rep.trivial Ring.toAddCommGroup Semiring.toModule π 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 Rep.instSubHom Rep.applyAsHom CategoryTheory.CategoryStruct.id ComplexShape.instDecidableRelRelDown ComplexShape.down_nat_odd_add Rep.leftRegularHom Rep.V Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CategoryTheory.Iso.inv HomologicalComplex.singleObjXIsoOfEq CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd Rep.instHasZeroObject

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