Documentation Verification Report

LongExactSequence

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

Statistics

Metric	Count
Definitions `cyclesMkOfCompEqD`, `mapShortComplex₁`, `mapShortComplex₂`, `mapShortComplex₃`, `δ`	5
Theorems `epi_δ_of_isZero`, `isIso_δ_of_isZero`, `mapShortComplex₁_exact`, `mapShortComplex₂_exact`, `mapShortComplex₃_exact`, `map_chainsFunctor_shortExact`, `mem_cycles₁_of_comp_eq_d₂₁`, `mono_δ_of_isZero`, `δ_apply`, `δ₀_apply`, `δ₁_apply`	11
Total	16

groupHomology

Definitions

Name	Category	Theorems
`cyclesMkOfCompEqD` 📖	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: `mono_δ_of_isZero`, `δ₀_apply`, `epi_δ_of_isZero`, `δ_apply`, `isIso_δ_of_isZero`, `δ₁_apply`

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` `groupHomology` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.SnakeInput.epi_δ` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_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` `groupHomology` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.IsIso` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.SnakeInput.isIso_δ` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_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` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_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` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_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` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_shortExact`
`map_chainsFunctor_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `Rep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Action.instCategory` `ModuleCat` `ModuleCat.moduleCategory` `Action.instHasZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ModuleCat.instPreadditive`	`ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.map` `chainsFunctor` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor`	—	`HomologicalComplex.shortExact_of_degreewise_shortExact` `AddRightCancelSemigroup.toIsRightCancelAdd` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `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` `chainsMap_id_f_hom_eq_mapRange` `Finsupp.range_mapRange_linearMap` `LinearMap.ker_eq_bot` `ModuleCat.mono_iff_injective` `Rep.instMonoModuleCatHom` `CategoryTheory.ShortComplex.ShortExact.mono_f` `Finsupp.ker_mapRange` `chainsMap_id_f_map_mono` `chainsMap_id_f_map_epi` `CategoryTheory.ShortComplex.ShortExact.epi_g`
`mem_cycles₁_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` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `ModuleCat.carrier` `Action.V` `CategoryTheory.ShortComplex.X₁` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `CategoryTheory.ShortComplex.X₂` `Finsupp.instAddCommMonoid` `Finsupp.module` `ModuleCat.isModule` `LinearMap.instFunLike` `Finsupp.mapRange.linearMap` `ModuleCat.Hom.hom` `Action.Hom.hom` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Finsupp.instAddCommGroup` `CategoryTheory.ConcreteCategory.hom` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `d₂₁`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `cycles₁`	—	`LinearMap.mem_ker` `Rep.mono_iff_injective` `CategoryTheory.ShortComplex.ShortExact.mono_f` `CategoryTheory.ShortComplex.Hom.comm₂₃` `RingHomCompTriple.ids` `Finsupp.lmapDomain_id` `CategoryTheory.Category.id_comp` `LinearMap.map_zero` `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` `groupHomology` `CategoryTheory.ShortComplex.X₂`	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.SnakeInput.mono_δ` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_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.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `inhomogeneousChains` `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` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.Hom.f` `chainsMap` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.ShortComplex.g` `Finsupp` `Action.V` `CategoryTheory.ShortComplex.X₁` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Finsupp.mapRange.linearMap` `ModuleCat.Hom.hom` `Action.Hom.hom` `CategoryTheory.ShortComplex.f`	`groupHomology` `δ` `cycles` `π` `cyclesMk` `cyclesMkOfCompEqD`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ShortComplex.ShortExact.δ_apply` `ModuleCat.forget₂_addCommGrp_additive` `CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier` `instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor` `map_chainsFunctor_shortExact` `LinearMap.map_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddMonoidHomClass.toAddMonoidHom.congr_simp` `chainsMap_id_f_hom_eq_mapRange`
`δ₀_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` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `ModuleCat.carrier` `Action.V` `CategoryTheory.ShortComplex.X₂` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `CategoryTheory.ShortComplex.X₃` `Finsupp.instAddCommMonoid` `Finsupp.module` `ModuleCat.isModule` `LinearMap.instFunLike` `Finsupp.mapRange.linearMap` `ModuleCat.Hom.hom` `Action.Hom.hom` `CategoryTheory.ShortComplex.g` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `cycles₁` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ConcreteCategory.hom` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `Finsupp.instAddCommGroup` `d₁₀`	`groupHomology` `δ` `Submodule.addCommGroup` `Submodule.module` `H1` `H1π` `H0` `H0π`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `cyclesMk₁_eq` `cyclesMk₀_eq` `δ_apply` `eq_d₁₀_comp_inv_apply` `LinearMap.map_coe_ker` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.ext` `LinearMap.map_zero` `chainsMap_id_f_hom_eq_mapRange` `Finsupp.domLCongr_symm` `Fin.isEmpty'` `Finsupp.LinearEquiv.finsuppUnique_symm_apply` `Finsupp.mapRange_single`
`δ₁_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` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `ModuleCat.carrier` `Action.V` `CategoryTheory.ShortComplex.X₂` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `CategoryTheory.ShortComplex.X₃` `Finsupp.instAddCommMonoid` `Finsupp.module` `ModuleCat.isModule` `LinearMap.instFunLike` `Finsupp.mapRange.linearMap` `ModuleCat.Hom.hom` `Action.Hom.hom` `CategoryTheory.ShortComplex.g` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Rep.instAddCommGroupCarrierVModuleCat` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `cycles₂` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.f` `ModuleCat.of` `Finsupp.instAddCommGroup` `CategoryTheory.ConcreteCategory.hom` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `d₂₁`	`groupHomology` `δ` `Submodule.addCommGroup` `Submodule.module` `H2` `H2π` `cycles₁` `H1` `H1π` `mem_cycles₁_of_comp_eq_d₂₁`	—	`mem_cycles₁_of_comp_eq_d₂₁` `AddRightCancelSemigroup.toIsRightCancelAdd` `cyclesMk₂_eq` `cyclesMk₁_eq` `δ_apply` `eq_d₂₁_comp_inv_apply` `LinearMap.map_coe_ker` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.ext` `LinearMap.map_zero` `chainsMap_id_f_hom_eq_mapRange` `Finsupp.domLCongr_symm`

---

← Back to Index