Revision #3533 → #4057 · back to history
modifiedChain complexc879111f5fb9
| Field | From #3533 | To #4057 |
|---|
| note | `HomologicalComplex` (and its `ChainComplex` specialization) is exactly a sequence of objects with differentials satisfying `d ∘ d = 0`. | `ChainComplex` (specialization of `HomologicalComplex`) is exactly a sequence of objects with differentials satisfying `d ∘ d = 0`. |
modifiedn-chains and boundary mapsc37ed8a743a4
| Field | From #3533 | To #4057 |
|---|
| note | The objects `X i` and differentials `d i j` are the fields of the `HomologicalComplex` structure. | `HomologicalComplex.d` is the differential/boundary map field of the complex, with the objects `X i` giving the n-chains. |
modifiedCycles and boundariesf8e46f90ee14
| Field | From #3533 | To #4057 |
|---|
| note | Cycles `Ker dₙ` are formalized as `HomologicalComplex.cycles`, but boundaries are not a standalone named subobject (handled implicitly via `toCycles`/homology). | `HomologicalComplex.cycles` gives `Ker dₙ`, but boundaries are not a standalone named subobject (only via the short complex / opcycles machinery). |
modifiedAcyclic / exact sequencecd25f61a83e9
| Field | From #3533 | To #4057 |
|---|
| note | `HomologicalComplex.Acyclic` is `∀ i, K.ExactAt i`, i.e. vanishing homology everywhere, matching the acyclic/exact-sequence notion. | `HomologicalComplex.Acyclic` asserts `ExactAt` at every index, i.e. vanishing homology everywhere. |
modifiedExact sequencec390b873bdb5
| Field | From #3533 | To #4057 |
|---|
| note | `ShortComplex.Exact` (and `ComposableArrows.Exact` for longer chains) expresses image equals kernel at each spot. | `ShortComplex.Exact` (with `ComposableArrows.Exact` for longer chains) expresses image equals kernel at each spot. |
modifiedFive lemmade11a4b8b830
| Field | From #3533 | To #4057 |
|---|
| note | This lemma is the five lemma for abelian categories, proving the middle map is an isomorphism given exact rows and iso outer maps. | This is the five lemma in an abelian category, concluding the middle map is an iso from exact rows and iso outer maps. |
modifiedAbelian category44eed20fc231
| Field | From #3533 | To #4057 |
|---|
| note | `CategoryTheory.Abelian` is the standard abelian-category typeclass extending preadditive with normal mono/epi, finite products, kernels and cokernels. | `CategoryTheory.Abelian` is the standard typeclass extending preadditive with normal mono/epi, finite products, kernels and cokernels. |
modifiedAbelian category (concrete characterization)d0275330a19c
| Field | From #3533 | To #4057 |
|---|
| note | Mathlib's `Abelian` definition is exactly this concrete characterization: zero object, kernels/cokernels, every mono a kernel and every epi a cokernel. | Mathlib's `Abelian` definition matches the concrete characterization: zero object, kernels/cokernels, every mono a kernel and every epi a cokernel. |
modifiedRight derived functors54b762863f65
| Field | From #3533 | To #4057 |
|---|
| note | `Functor.rightDerived F n` is defined via injective resolutions and homology of the homotopy category. | `Functor.rightDerived F n` is defined via injective resolutions and homology in the homotopy category. |
modifiedInduced homomorphism on homologyba54ffc8b2d0
| Field | From #3533 | To #4057 |
|---|
| note | `singularHomologyFunctor` is functorial in `TopCat`, so a continuous map induces a map on singular homology. | `singularHomologyFunctor` is functorial on `TopCat`, so a continuous map induces a map on singular homology. |
addedCategory of modules0a855873f6ce
addedInjective resolution6a9da94f8858
addedProjective resolutiona16411d97115
addedLeft exact functor09d5dbec00a0