Documentation Verification Report

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` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `CategoryTheory.Limits.IsZero` `groupCohomology` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.SnakeInput.epi_δ` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `map_cochainsFunctor_shortExact`
`isIso_δ_of_isZero` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `CategoryTheory.Limits.IsZero` `groupCohomology` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.IsIso` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.SnakeInput.isIso_δ` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `map_cochainsFunctor_shortExact`
`mapShortComplex₁_exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Abelian.toPreadditive` `ModuleCat.abelian` `mapShortComplex₁`	—	`CategoryTheory.ShortComplex.ShortExact.homology_exact₁` `AddRightCancelSemigroup.toIsRightCancelAdd` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `map_cochainsFunctor_shortExact`
`mapShortComplex₂_exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive`	`CategoryTheory.ShortComplex.Exact` `mapShortComplex₂`	—	`CategoryTheory.ShortComplex.ShortExact.homology_exact₂` `AddRightCancelSemigroup.toIsRightCancelAdd` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `map_cochainsFunctor_shortExact`
`mapShortComplex₃_exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive`	`CategoryTheory.ShortComplex.Exact` `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` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive`	`CochainComplex` `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` `cochainsFunctor` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor`	—	`HomologicalComplex.shortExact_of_degreewise_shortExact` `AddRightCancelSemigroup.toIsRightCancelAdd` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `HomologicalComplex.instPreservesZeroMorphismsEval` `RingHomSurjective.ids` `CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker` `Action.forget₂_preservesZeroMorphisms` `CategoryTheory.ShortComplex.Exact.map` `CategoryTheory.ShortComplex.ShortExact.exact` `CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV` `CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf` `LinearMap.range.congr_simp` `cochainsMap_id_f_hom_eq_compLeft` `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` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `ModuleCat.carrier` `Action.V` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Action.Hom.hom` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `Pi.addCommGroup` `Rep.instAddCommGroupCarrierVModuleCat` `Pi.Function.module` `d₀₁`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `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` `LinearMap.semilinearMapClass`
`mem_cocycles₂_of_comp_eq_d₁₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `ModuleCat.carrier` `Action.V` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Action.Hom.hom` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `Pi.addCommGroup` `Rep.instAddCommGroupCarrierVModuleCat` `Pi.Function.module` `d₁₂`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `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` `LinearMap.semilinearMapClass`
`mono_δ_of_isZero` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `CategoryTheory.Limits.IsZero` `groupCohomology` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.SnakeInput.mono_δ` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `map_cochainsFunctor_shortExact`
`δ_apply` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `DFunLike.coe` `HomologicalComplex.X` `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` `Action.V` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₂` `Action.Hom.hom` `CategoryTheory.ShortComplex.f`	`groupCohomology` `δ` `cocycles` `π` `cocyclesMk` `cocyclesMkOfCompEqD`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.ShortExact.δ_apply` `ModuleCat.forget₂_addCommGrp_additive` `CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier` `instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor` `map_cochainsFunctor_shortExact` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddMonoidHomClass.toAddMonoidHom.congr_simp` `cochainsMap_id_f_hom_eq_compLeft` `CochainComplex.next`
`δ₀_apply` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `DFunLike.coe` `Action.V` `CategoryTheory.ShortComplex.X₂` `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` `Action.Hom.hom` `CategoryTheory.ShortComplex.g` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Rep.instAddCommGroupCarrierVModuleCat` `SetLike.instMembership` `Submodule.setLike` `Representation.invariants` `Rep.ρ` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `Pi.addCommGroup` `Pi.Function.module` `d₀₁`	`groupCohomology` `δ` `Submodule.addCommGroup` `Submodule.module` `H0` `CategoryTheory.Iso.inv` `H0Iso` `Pi.addCommMonoid` `cocycles₁` `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'` `cochainsMap_id_f_hom_eq_compLeft` `CategoryTheory.CommSq.w` `CategoryTheory.CommSq.vert_inv` `cochainsMap_f_1_comp_cochainsIso₁` `RingHomCompTriple.ids` `CategoryTheory.Category.assoc` `Mathlib.Tactic.TermCongr.cHole.congr_simp` `LinearMap.comp.congr_simp`
`δ₁_apply` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive` `ModuleCat.carrier` `Action.V` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₃` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Action.Hom.hom` `CategoryTheory.ShortComplex.g` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Pi.Function.module` `SetLike.instMembership` `Submodule.setLike` `cocycles₁` `instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `Pi.addCommGroup` `d₁₂`	`groupCohomology` `δ` `Submodule.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` `cochainsMap_id_f_hom_eq_compLeft` `CategoryTheory.CommSq.w` `CategoryTheory.CommSq.vert_inv` `cochainsMap_f_2_comp_cochainsIso₂` `RingHomCompTriple.ids` `CategoryTheory.Category.assoc` `Mathlib.Tactic.TermCongr.cHole.congr_simp` `LinearMap.comp.congr_simp`

---

← Back to Index