Mathlib Map

Theorems · Definition · category theory

CategoryTheory.ShortComplex.moduleCatCyclesIso

{R : Type u} →
  [inst : Ring R] → (S : CategoryTheory.ShortComplex (ModuleCat R)) → S.cycles ≅ S.moduleCatLeftHomologyData.K

Given a short complex S of modules, this is the isomorphism between the abstract S.cycles of the homology API and the more concrete description as LinearMap.ker S.g.

Defined in
Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Cited by
20 results in Mathlib
Foundations
Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Ring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc · cited by 5ShortComplex.moduleCatCyc…Rep.FiniteCyclicGroup.groupCohomologyπOdd · cited by 3FiniteCyclicGroup.groupCo…CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i · cited by 3ShortComplex.moduleCatCyc…CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom · cited by 2ShortComplex.π_moduleCatC…Rep.FiniteCyclicGroup.groupCohomologyπEven · cited by 2FiniteCyclicGroup.groupCo…Rep.FiniteCyclicGroup.groupHomologyπEven · cited by 2FiniteCyclicGroup.groupHo…Rep.FiniteCyclicGroup.groupHomologyπOdd · cited by 2FiniteCyclicGroup.groupHo…CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles · cited by 2ShortComplex.moduleCatCyc…CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π · cited by 2ShortComplex.moduleCatCyc…CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom · cited by 2ShortComplex.toCycles_mod…CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc · cited by 1ShortComplex.π_moduleCatC…CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc · cited by 1ShortComplex.moduleCatCyc…CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc · cited by 1ShortComplex.moduleCatCyc…CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc · cited by 1ShortComplex.toCycles_mod…CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply · cited by 0ShortComplex.π_moduleCatC…Ring · cited by 7463RingCategoryTheory.Iso · cited by 3963CategoryTheory.IsoCategoryTheory.ShortComplex · cited by 1850CategoryTheory.ShortCompl…ModuleCat · cited by 1429ModuleCatCategoryTheory.ShortComplex.LeftHomologyData.K · cited by 233LeftHomologyData.KCategoryTheory.ShortComplex.cycles · cited by 220ShortComplex.cyclesCategoryTheory.ShortComplex.moduleCatLeftHomologyData · cited by 106ShortComplex.moduleCatLef…CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso · cited by 28LeftHomologyData.cyclesIsoShortComplex.moduleCatCyclesI…CITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by24

Results whose statement or proof uses this declaration.