LongExactSequence

📁 Source: Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean

Statistics

Metric	Count
Definitions cocyclesMkOfCompEqD, mapShortComplex₁, mapShortComplex₂, mapShortComplex₃, δ	5
Theorems epi_δ_of_isZero, isIso_δ_of_isZero, mapShortComplex₁_exact, mapShortComplex₂_exact, mapShortComplex₃_exact, map_cochainsFunctor_shortExact, mem_cocycles₁_of_comp_eq_d₀₁, mem_cocycles₂_of_comp_eq_d₁₂, mono_δ_of_isZero, δ_apply, δ₀_apply, δ₁_apply	12
Total	17

groupCohomology

Definitions

Name	Category	Theorems
cocyclesMkOfCompEqD 📖	CompOp	1 math math: δ_apply
mapShortComplex₁ 📖	CompOp	1 math math: mapShortComplex₁_exact
mapShortComplex₂ 📖	CompOp	1 math math: mapShortComplex₂_exact
mapShortComplex₃ 📖	CompOp	1 math math: mapShortComplex₃_exact
δ 📖	CompOp	6 math math: δ_apply, δ₁_apply, epi_δ_of_isZero, δ₀_apply, mono_δ_of_isZero, isIso_δ_of_isZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_δ_of_isZero 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.Limits.IsZero ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₂	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.ShortComplex.X₁ δ	—	CategoryTheory.ShortComplex.SnakeInput.epi_δ instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact
isIso_δ_of_isZero 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.Limits.IsZero ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₂	CategoryTheory.IsIso ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.ShortComplex.X₁ δ	—	CategoryTheory.ShortComplex.SnakeInput.isIso_δ instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact
mapShortComplex₁_exact 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ModuleCat.abelian mapShortComplex₁	—	CategoryTheory.ShortComplex.ShortExact.homology_exact₁ AddRightCancelSemigroup.toIsRightCancelAdd instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact
mapShortComplex₂_exact 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive mapShortComplex₂	—	CategoryTheory.ShortComplex.ShortExact.homology_exact₂ AddRightCancelSemigroup.toIsRightCancelAdd instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact
mapShortComplex₃_exact 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ModuleCat.abelian mapShortComplex₃	—	CategoryTheory.ShortComplex.ShortExact.homology_exact₃ AddRightCancelSemigroup.toIsRightCancelAdd instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact
map_cochainsFunctor_shortExact 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive	CategoryTheory.ShortComplex.ShortExact CochainComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasZeroMorphisms CategoryTheory.ShortComplex.map Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory Rep.instPreadditive cochainsFunctor instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor	—	HomologicalComplex.shortExact_of_degreewise_shortExact AddRightCancelSemigroup.toIsRightCancelAdd instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor HomologicalComplex.instPreservesZeroMorphismsEval RingHomSurjective.ids CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker CategoryTheory.Functor.preservesZeroMorphisms_of_additive Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier CategoryTheory.ShortComplex.Exact.map CategoryTheory.ShortComplex.ShortExact.exact CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits Rep.preservesLimits_forget CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits Rep.preservesColimits_forget CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf LinearMap.range_compLeft LinearMap.ker_compLeft cochainsMap_id_f_map_mono CategoryTheory.ShortComplex.ShortExact.mono_f cochainsMap_id_f_map_epi CategoryTheory.ShortComplex.ShortExact.epi_g
mem_cocycles₁_of_comp_eq_d₀₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive Rep.V CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ DFunLike.coe Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom CategoryTheory.ShortComplex.f ModuleCat.of CommRing.toRing Pi.addCommGroup Pi.Function.module Ring.toSemiring ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₀₁	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Rep.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.ShortComplex.X₁ Rep Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive AddCommGroup.toAddCommMonoid Rep.hV1 Pi.Function.module Rep.hV2 SetLike.instMembership Submodule.setLike cocycles₁	—	Function.Injective.comp_left Rep.mono_iff_injective CategoryTheory.ShortComplex.ShortExact.mono_f CategoryTheory.ShortComplex.Hom.comm₂₃ RingHomCompTriple.ids CategoryTheory.Category.assoc d₀₁_comp_d₁₂_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Representation.IntertwiningMap.instLinearMapClass
mem_cocycles₂_of_comp_eq_d₁₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive Rep.V CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ DFunLike.coe Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom CategoryTheory.ShortComplex.f ModuleCat.of CommRing.toRing Pi.addCommGroup Pi.Function.module Ring.toSemiring ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₁₂	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Rep.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.ShortComplex.X₁ Rep Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive AddCommGroup.toAddCommMonoid Rep.hV1 Pi.Function.module Rep.hV2 SetLike.instMembership Submodule.setLike cocycles₂	—	Function.Injective.comp_left Rep.mono_iff_injective CategoryTheory.ShortComplex.ShortExact.mono_f CategoryTheory.ShortComplex.Hom.comm₂₃ RingHomCompTriple.ids CategoryTheory.Category.assoc d₁₂_comp_d₂₃_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Representation.IntertwiningMap.instLinearMapClass
mono_δ_of_isZero 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.Limits.IsZero ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₂	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory groupCohomology CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.ShortComplex.X₁ δ	—	CategoryTheory.ShortComplex.SnakeInput.mono_δ instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact
δ_apply 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive DFunLike.coe HomologicalComplex.X ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.ShortComplex.X₃ ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier HomologicalComplex.d NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HomologicalComplex.Hom.f cochainsMap MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.ShortComplex.g Rep.V CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ Representation.IntertwiningMap Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom CategoryTheory.ShortComplex.f	DFunLike.coe groupCohomology CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.ShortComplex.X₁ ModuleCat.carrier CommRing.toRing CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier δ cocycles π cocyclesMk cocyclesMkOfCompEqD	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.ShortExact.δ_apply ModuleCat.forget₂_addCommGrp_additive CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor map_cochainsFunctor_shortExact CochainComplex.next
δ₀_apply 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive DFunLike.coe Representation.IntertwiningMap Rep.V CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom CategoryTheory.ShortComplex.g Submodule SetLike.instMembership Submodule.setLike Representation.invariants CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f ModuleCat.of CommRing.toRing Pi.addCommGroup Pi.Function.module Ring.toSemiring ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₀₁	DFunLike.coe groupCohomology CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.ShortComplex.X₁ ModuleCat.carrier CommRing.toRing CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier δ ModuleCat.of Rep.V Submodule Rep.hV1 Rep.hV2 SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup Submodule.module H0 CategoryTheory.Iso.inv H0Iso Pi.addCommMonoid Pi.Function.module cocycles₁ Pi.addCommGroup H1 H1π mem_cocycles₁_of_comp_eq_d₀₁	—	mem_cocycles₁_of_comp_eq_d₀₁ AddRightCancelSemigroup.toIsRightCancelAdd cocyclesMk₀_eq cocyclesMk₁_eq δ_apply eq_d₀₁_comp_inv_apply subtype_comp_d₀₁_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass inhomogeneousCochains.ext Fin.isEmpty' CategoryTheory.CommSq.w CategoryTheory.CommSq.vert_inv cochainsMap_f_1_comp_cochainsIso₁ RingHomCompTriple.ids CategoryTheory.Category.assoc Mathlib.Tactic.TermCongr.cHole.congr_simp
δ₁_apply 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive Rep.V CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ DFunLike.coe Representation.IntertwiningMap AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.Hom.hom CategoryTheory.ShortComplex.g Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallVMemSubmoduleCocycles₁ CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f ModuleCat.of CommRing.toRing Pi.addCommGroup Ring.toSemiring ModuleCat.carrier CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₁₂	DFunLike.coe groupCohomology CategoryTheory.ShortComplex.X₃ Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Rep.instPreadditive CategoryTheory.ShortComplex.X₁ ModuleCat.carrier CommRing.toRing CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier δ ModuleCat.of Submodule Pi.addCommMonoid Rep.V Rep.hV1 Pi.Function.module Rep.hV2 SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 H1π cocycles₂ H2 H2π mem_cocycles₂_of_comp_eq_d₁₂	—	mem_cocycles₂_of_comp_eq_d₁₂ AddRightCancelSemigroup.toIsRightCancelAdd cocyclesMk₁_eq cocyclesMk₂_eq δ_apply eq_d₁₂_comp_inv_apply cocycles₁.d₁₂_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass inhomogeneousCochains.ext CategoryTheory.CommSq.w CategoryTheory.CommSq.vert_inv cochainsMap_f_2_comp_cochainsIso₂ RingHomCompTriple.ids CategoryTheory.Category.assoc Mathlib.Tactic.TermCongr.cHole.congr_simp

---

← Back to Index