Homology

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

Statistics

Metric	Count
Definitions dCokernelSequence, dHomologyData, dHomologyIso, dKernelSequence, dShortComplex	5
Theorems dCokernelSequence_X₁, dCokernelSequence_X₂, dCokernelSequence_X₃, dCokernelSequence_exact, dCokernelSequence_f, dCokernelSequence_g, dHomologyData_iso_hom, dHomologyData_iso_inv, dHomologyData_left_H, dHomologyData_left_K, dHomologyData_left_i, dHomologyData_left_π, dHomologyData_right_H, dHomologyData_right_Q, dHomologyData_right_p, dHomologyData_right_ι, dKernelSequence_X₁, dKernelSequence_X₂, dKernelSequence_X₃, dKernelSequence_exact, dKernelSequence_f, dKernelSequence_g, dShortComplex_X₁, dShortComplex_X₂, dShortComplex_X₃, dShortComplex_f, dShortComplex_g, instEpiGDCokernelSequence, instMonoFDKernelSequence, map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃, map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc	31
Total	36

CategoryTheory.Abelian.SpectralObject

Definitions

Name	Category	Theorems
dCokernelSequence 📖	CompOp	9 math math: dCokernelSequence_f, dCokernelSequence_X₂, dHomologyData_iso_inv, dCokernelSequence_X₁, instEpiGDCokernelSequence, dCokernelSequence_exact, dHomologyData_iso_hom, dCokernelSequence_X₃, dCokernelSequence_g
dHomologyData 📖	CompOp	10 math math: dHomologyData_iso_inv, dHomologyData_left_i, dHomologyData_right_Q, dHomologyData_left_H, dHomologyData_right_ι, dHomologyData_right_H, dHomologyData_right_p, dHomologyData_left_K, dHomologyData_left_π, dHomologyData_iso_hom
dHomologyIso 📖	CompOp	—
dKernelSequence 📖	CompOp	9 math math: dKernelSequence_exact, dKernelSequence_X₂, dHomologyData_iso_inv, dKernelSequence_X₃, dKernelSequence_g, dKernelSequence_X₁, dKernelSequence_f, dHomologyData_iso_hom, instMonoFDKernelSequence
dShortComplex 📖	CompOp	15 math math: dHomologyData_iso_inv, dHomologyData_left_i, dShortComplex_g, dHomologyData_right_Q, dShortComplex_f, dHomologyData_left_H, dHomologyData_right_ι, dHomologyData_right_H, dHomologyData_right_p, dHomologyData_left_K, dShortComplex_X₃, dHomologyData_left_π, dHomologyData_iso_hom, dShortComplex_X₂, dShortComplex_X₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dCokernelSequence_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence E	—	—
dCokernelSequence_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence E	—	—
dCokernelSequence_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence E	—	—
dCokernelSequence_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.eq_whisker CategoryTheory.ComposableArrows.Exact.toIsComplex sequenceΨ_exact CategoryTheory.ShortComplex.Exact.exact_up_to_refinements CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp map_ιE CategoryTheory.ComposableArrows.naturality' CategoryTheory.cancel_mono πE_d_ιE
dCokernelSequence_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence d	—	—
dCokernelSequence_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence map CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	—
dHomologyData_iso_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData CategoryTheory.Limits.KernelFork.ofι CategoryTheory.ShortComplex.X₂ dKernelSequence CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.CokernelCofork.ofπ dCokernelSequence CategoryTheory.ShortComplex.Exact.fIsKernel CategoryTheory.ShortComplex.Exact.gIsCokernel E map CategoryTheory.ComposableArrows.fourδ₄Toδ₃ CategoryTheory.ComposableArrows.fourδ₁Toδ₀ CategoryTheory.ShortComplex.HomologyData.iso dHomologyData CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
dHomologyData_iso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.inv CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData CategoryTheory.Limits.KernelFork.ofι CategoryTheory.ShortComplex.X₂ dKernelSequence CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.CokernelCofork.ofπ dCokernelSequence CategoryTheory.ShortComplex.Exact.fIsKernel CategoryTheory.ShortComplex.Exact.gIsCokernel E map CategoryTheory.ComposableArrows.fourδ₄Toδ₃ CategoryTheory.ComposableArrows.fourδ₁Toδ₀ CategoryTheory.ShortComplex.HomologyData.iso dHomologyData CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
dHomologyData_left_H 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.left dHomologyData E	—	—
dHomologyData_left_K 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.left dHomologyData E	—	—
dHomologyData_left_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.left dHomologyData map CategoryTheory.ComposableArrows.fourδ₁Toδ₀	—	—
dHomologyData_left_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.left dHomologyData map CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	—
dHomologyData_right_H 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.right dHomologyData E	—	—
dHomologyData_right_Q 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.right dHomologyData E	—	—
dHomologyData_right_p 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.RightHomologyData.p CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.right dHomologyData map CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	—
dHomologyData_right_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.RightHomologyData.ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex CategoryTheory.ShortComplex.HomologyData.right dHomologyData map CategoryTheory.ComposableArrows.fourδ₁Toδ₀	—	—
dKernelSequence_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence E	—	—
dKernelSequence_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence E	—	—
dKernelSequence_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence E	—	—
dKernelSequence_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.surjective_up_to_refinements_of_epi CategoryTheory.eq_whisker CategoryTheory.ComposableArrows.Exact.toIsComplex sequenceΨ_exact CategoryTheory.ShortComplex.Exact.exact_up_to_refinements CategoryTheory.ComposableArrows.Exact.exact CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero πE_d_ιE CategoryTheory.epi_comp πE_map CategoryTheory.ComposableArrows.naturality'
dKernelSequence_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence map CategoryTheory.ComposableArrows.fourδ₁Toδ₀	—	—
dKernelSequence_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence d	—	—
dShortComplex_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex E	—	—
dShortComplex_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex E	—	—
dShortComplex_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex E	—	—
dShortComplex_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex d	—	—
dShortComplex_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dShortComplex d	—	—
instEpiGDCokernelSequence 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dCokernelSequence CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
instMonoFDKernelSequence 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive dKernelSequence CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	—
map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀ CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	—
map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E map CategoryTheory.ComposableArrows.fourδ₁Toδ₀ CategoryTheory.ComposableArrows.fourδ₄Toδ₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃

---

← Back to Index