Differentials

📁 Source: Mathlib/Algebra/Homology/SpectralObject/Differentials.lean

Statistics

Metric	Count
Definitions d, sequenceΨ, Ψ	3
Theorems cyclesMap_Ψ, cyclesMap_Ψ_assoc, cyclesMap_Ψ_exact, d_EIsoH_hom, d_EIsoH_hom_assoc, d_d, d_d_assoc, d_ιE_fromOpcycles, d_ιE_fromOpcycles_assoc, sequenceΨ_exact, toCycles_Ψ, toCycles_Ψ_assoc, toCycles_πE_d, toCycles_πE_d_assoc, Ψ_fromOpcycles, Ψ_fromOpcycles_assoc, Ψ_opcyclesMap, Ψ_opcyclesMap_exact, πE_EIsoH_hom, πE_EIsoH_hom_assoc, πE_d_ιE, πE_d_ιE_assoc	22
Total	25

CategoryTheory.Abelian.SpectralObject

Definitions

Name	Category	Theorems
d 📖	CompOp	19 math math: dCokernelSequence_f, toCycles_πE_d, d_ιE_fromOpcycles, toCycles_πE_d_assoc, map_fourδ₁Toδ₀_d, d_d, d_EIsoH_hom, map_fourδ₁Toδ₀_d_assoc, dShortComplex_g, dShortComplex_f, πE_d_ιE_assoc, d_map_fourδ₄Toδ₃, d_ιE_fromOpcycles_assoc, d_map_fourδ₄Toδ₃_assoc, d_EIsoH_hom_assoc, dKernelSequence_g, SpectralSequence.pageD_eq, d_d_assoc, πE_d_ιE
sequenceΨ 📖	CompOp	1 math math: sequenceΨ_exact
Ψ 📖	CompOp	11 math math: Ψ_opcyclesMap, cyclesMap_Ψ_exact, cyclesMap_Ψ_assoc, Ψ_opcyclesMap_exact, toCycles_Ψ_assoc, Ψ_fromOpcycles_assoc, πE_d_ιE_assoc, Ψ_fromOpcycles, cyclesMap_Ψ, toCycles_Ψ, πE_d_ιE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclesMap_Ψ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles opcycles cyclesMap CategoryTheory.ComposableArrows.threeδ₁Toδ₀ Ψ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.cancel_epi instEpiToCycles CategoryTheory.Limits.comp_zero toCycles_cyclesMap_assoc toCycles_Ψ zero₃_assoc CategoryTheory.Limits.zero_comp
cyclesMap_Ψ_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles cyclesMap CategoryTheory.ComposableArrows.threeδ₁Toδ₀ opcycles Ψ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_Ψ
cyclesMap_Ψ_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cycles opcycles cyclesMap CategoryTheory.ComposableArrows.threeδ₁Toδ₀ Ψ cyclesMap_Ψ	—	cyclesMap_Ψ CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.instEpiId CategoryTheory.Category.assoc Ψ_fromOpcycles Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.id_comp cyclesMap_i CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id liftCycles_i
d_EIsoH_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ d CategoryTheory.Iso.hom EIsoH δ	—	CategoryTheory.cancel_epi CategoryTheory.Category.id_comp instEpiToCycles toCycles_πE_d_assoc πE_EIsoH_hom πE_EIsoH_hom_assoc cyclesIsoH_inv_hom_id CategoryTheory.Category.comp_id cyclesIsoH_inv_hom_id_assoc
d_EIsoH_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.CategoryStruct.id d CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom EIsoH δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_EIsoH_hom
d_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_epi instEpiToCycles CategoryTheory.Limits.comp_zero toCycles_πE_d_assoc toCycles_πE_d δ_δ_assoc CategoryTheory.Limits.zero_comp
d_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_d
d_ιE_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ d opcycles ιE fromOpcycles δ	—	CategoryTheory.cancel_epi instEpiToCycles toCycles_πE_d_assoc πE_ιE_assoc p_fromOpcycles toCycles_i_assoc fromOpcyles_δ pOpcycles_δFromOpcycles CategoryTheory.Functor.map_comp δ_naturality CategoryTheory.Category.id_comp
d_ιE_fromOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E d opcycles ιE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_ιE_fromOpcycles
sequenceΨ_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive sequenceΨ	—	CategoryTheory.ComposableArrows.exact_of_δ₀ CategoryTheory.ShortComplex.Exact.exact_toComposableArrows cyclesMap_Ψ cyclesMap_Ψ_exact Ψ_opcyclesMap Ψ_opcyclesMap_exact
toCycles_Ψ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles opcycles toCycles Ψ δ pOpcycles	—	toCycles_descCycles
toCycles_Ψ_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles opcycles Ψ δ pOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_Ψ
toCycles_πE_d 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles E toCycles πE d δ	—	δ_toCycles_assoc descE.congr_simp toCycles_πE_descE
toCycles_πE_d_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles E πE d δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_πE_d
Ψ_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ Ψ fromOpcycles iCycles δ	—	CategoryTheory.cancel_epi instEpiToCycles toCycles_Ψ_assoc p_fromOpcycles toCycles_i_assoc δ_naturality
Ψ_fromOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles opcycles Ψ CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles iCycles δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Ψ_fromOpcycles
Ψ_opcyclesMap 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles opcycles Ψ opcyclesMap CategoryTheory.ComposableArrows.threeδ₃Toδ₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_mono instMonoFromOpcycles CategoryTheory.Limits.zero_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap_fromOpcycles Ψ_fromOpcycles_assoc zero₁ CategoryTheory.Limits.comp_zero
Ψ_opcyclesMap_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cycles opcycles Ψ opcyclesMap CategoryTheory.ComposableArrows.threeδ₃Toδ₂ Ψ_opcyclesMap	—	Ψ_opcyclesMap CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.surjective_up_to_refinements_of_epi instEpiPOpcycles CategoryTheory.ShortComplex.Exact.exact_up_to_refinements cokernelSequenceOpcycles_exact p_opcyclesMap CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.comp_zero CategoryTheory.epi_comp CategoryTheory.cancel_mono instMonoFromOpcycles toCycles_Ψ_assoc p_fromOpcycles
πE_EIsoH_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.CategoryStruct.id E CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ πE CategoryTheory.Iso.hom EIsoH cyclesIsoH	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom CategoryTheory.Category.comp_id
πE_EIsoH_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.CategoryStruct.id E πE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom EIsoH cyclesIsoH	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πE_EIsoH_hom
πE_d_ιE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E opcycles πE d ιE Ψ	—	CategoryTheory.cancel_epi instEpiToCycles toCycles_Ψ toCycles_πE_d_assoc πE_ιE toCycles_i_assoc δ_naturality_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
πE_d_ιE_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E πE d opcycles ιE Ψ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πE_d_ιE

---

← Back to Index