Documentation Verification Report

Basic

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

Statistics

MetricCount
DefinitionsH, hom, composableArrows₅, instCategory, sc₁, sc₂, sc₃, δ, δ'
9
Theoremscomm, comm_assoc, ext, ext_iff, comp_hom, comp_hom_assoc, composableArrows₅_exact, epi_H_map_twoδ₁Toδ₀, epi_H_map_twoδ₁Toδ₀', exact₁, exact₁', exact₂, exact₂', exact₃, exact₃', id_hom, isIso_H_map_twoδ₁Toδ₀, isIso_H_map_twoδ₁Toδ₀', isZero_H_map_mk₁_of_isIso, mono_H_map_twoδ₁Toδ₀, mono_H_map_twoδ₁Toδ₀', sc₁_X₁, sc₁_X₂, sc₁_X₃, sc₁_f, sc₁_g, sc₂_X₁, sc₂_X₂, sc₂_X₃, sc₂_f, sc₂_g, sc₃_X₁, sc₃_X₂, sc₃_X₃, sc₃_f, sc₃_g, zero₁, zero₁_assoc, zero₂, zero₂_assoc, zero₃, zero₃_assoc, δ_naturality, δ_naturality_assoc, δ_δ, δ_δ_assoc
46
Total55

CategoryTheory.Abelian.SpectralObject

Definitions

NameCategoryTheorems
H 📖CompOp
198 mathmath: δ_eq_zero_of_isIso₂, H_map_twoδ₂Toδ₁_toCycles_assoc, exact₁', δToCycles_iCycles, leftHomologyDataShortComplex_H, homologyDataIdId_left_π, EIsoH_hom_opcyclesIsoH_inv_assoc, liftOpcycles_fromOpcycles_assoc, zero₂_assoc, cokernelSequenceCycles_X₁, cokernelSequenceCyclesEIso_hom_τ₁, instMonoFromOpcycles, sc₂_X₃, cokernelSequenceOpcycles_X₂, toCycles_πE_d, δToCycles_πE, shortComplex_X₂, d_ιE_fromOpcycles, toCycles_πE_d_assoc, mono_H_map_twoδ₁Toδ₀, δ_toCycles, δ_δ_assoc, opcyclesIso_hom_δFromOpcycles, homologyDataIdId_left_i, cyclesIsoH_hom_EIsoH_inv, homologyDataIdId_left_H, isZero_H_obj_mk₁_i₀_le', δToCycles_cyclesIso_inv_assoc, cyclesIso_hom_i, pOpcycles_δFromOpcycles, homologyDataIdId_iso_inv, δ_δ, cyclesMap_i, cyclesIso_hom_i_assoc, HasSpectralSequence.isZero_H_obj_mk₁_i₀_le, toCycles_descCycles, fromOpcycles_H_map_twoδ₁Toδ₀, isZero_H_obj_mk₁_i₃_le', comp_hom, EToCycles_i_assoc, epi_H_map_twoδ₁Toδ₀', toCycles_cyclesMap, homologyDataIdId_iso_hom, IsFirstQuadrant.isZero₂, comp_hom_assoc, πE_ιE, fromOpcycles_H_map_twoδ₁Toδ₀_assoc, p_opcyclesIso_inv, πE_EIsoH_hom_assoc, kernelSequenceOpcyclesE_X₃, d_EIsoH_hom, isIso_H_map_twoδ₁Toδ₀, isIso_fromOpcycles, zero₃, rightHomologyDataShortComplex_ι, cokernelSequenceE_g, kernelSequenceE_g, toCycles_cyclesMap_assoc, exact₂', homologyDataIdId_right_p, p_opcyclesToE, rightHomologyDataShortComplex_H, cyclesIsoH_inv_hom_id, ιE_δFromOpcycles_assoc, isIso_toCycles, liftE_ιE_fromOpcycles, isZero_H_obj_mk₁_i₀_le, kernelSequenceOpcyclesEIso_hom_τ₃, isZero₁_of_isFirstQuadrant, kernelSequenceOpcycles_X₂, kernelSequenceCyclesE_g, fromOpcyles_δ_assoc, cokernelSequenceCycles_X₂, sc₂_g, cyclesIsoH_inv_hom_id_assoc, toCycles_Ψ_assoc, isZero₁_of_isThirdQuadrant, H_map_twoδ₂Toδ₁_toCycles, δToCycles_πE_assoc, sc₁_X₁, cokernelSequenceCycles_f, zero₂, toCycles_πE_descE_assoc, opcyclesIsoH_hom, cyclesIsoH_hom_EIsoH_inv_assoc, opcyclesMap_fromOpcycles, cokernelSequenceE_X₂, instEpiToCycles, cokernelSequenceCyclesE_X₁, Ψ_fromOpcycles_assoc, homologyDataIdId_right_ι, exact₃', p_fromOpcycles_assoc, πE_EIsoH_hom, isZero₂_of_isFirstQuadrant, IsFirstQuadrant.isZero₁, liftOpcycles_fromOpcycles, IsThirdQuadrant.isZero₂, cokernelIsoCycles_hom_fac_assoc, iCycles_δ, cokernelSequenceCyclesEIso_inv_τ₁, Hom.comm, kernelSequenceE_f, kernelSequenceCycles_X₂, p_opcyclesMap_assoc, d_ιE_fromOpcycles_assoc, sc₂_X₁, opcyclesIsoH_inv_hom_id_assoc, zero₁, δ_naturality_assoc, δ_naturality, d_EIsoH_hom_assoc, sc₃_X₁, leftHomologyDataShortComplex_π, p_opcyclesIso_inv_assoc, shortComplexMap_τ₂, homologyDataIdId_left_K, δ_pOpcycles_assoc, id_hom, shortComplexMap_τ₃, sc₂_X₂, cokernelIsoCycles_hom_fac, δToCycles_cyclesIso_inv, p_descOpcycles, cokernelSequenceOpcyclesE_X₁, πE_ιE_assoc, kernelSequenceOpcycles_g, Hom.comm_assoc, opcyclesIsoKernel_hom_fac, sc₁_X₃, δ_toCycles_assoc, opcyclesIsoH_inv_hom_id, p_descOpcycles_assoc, p_fromOpcycles, Ψ_fromOpcycles, p_opcyclesMap, opcyclesIso_hom_δFromOpcycles_assoc, isZero_H_obj_of_isIso, instEpiPOpcycles, opcyclesIsoKernel_hom_fac_assoc, ιE_δFromOpcycles, homologyDataIdId_right_H, δToCycles_iCycles_assoc, shortComplexMap_τ₁, liftCycles_i, cyclesIsoH_hom_inv_id_assoc, EToCycles_i, zero₃_assoc, mono_H_map_twoδ₁Toδ₀', isZero_H_obj_mk₁_i₃_le, shortComplex_X₁, isIso_H_map_twoδ₁Toδ₀', cokernelSequenceOpcycles_X₁, opcyclesIsoH_hom_inv_id, sc₃_X₃, homologyDataIdId_right_Q, shortComplex_X₃, sc₃_X₂, kernelSequenceCycles_X₃, p_opcyclesToE_assoc, δ_pOpcycles, EIsoH_hom_opcyclesIsoH_inv, δ_eq_zero_of_isIso₁, cokernelSequenceE_X₁, toCycles_Ψ, kernelSequenceOpcyclesEIso_inv_τ₃, kernelSequenceE_X₂, opcyclesIsoH_hom_inv_id_assoc, liftCycles_i_assoc, cokernelSequenceE_f, cyclesIsoH_hom_inv_id, sc₁_X₂, sc₂_f, isZero₂_of_isThirdQuadrant, toCycles_πE_descE, EIsoH_hom_naturality, kernelSequenceE_X₃, cokernelSequenceOpcyclesE_f, cyclesIsoH_inv, cyclesMap_i_assoc, liftE_ιE_fromOpcycles_assoc, sc₃_f, iCycles_δ_assoc, zero₁_assoc, kernelSequenceCyclesE_X₃, opcyclesMap_fromOpcycles_assoc, pOpcycles_δFromOpcycles_assoc, instMonoICycles, fromOpcyles_δ, epi_H_map_twoδ₁Toδ₀, toCycles_descCycles_assoc, IsThirdQuadrant.isZero₁, isZero_H_map_mk₁_of_isIso, HasSpectralSequence.isZero_H_obj_mk₁_i₃_le, sc₁_g, kernelSequenceOpcycles_X₃, toCycles_i, toCycles_i_assoc
composableArrows₅ 📖CompOp
1 mathmath: composableArrows₅_exact
instCategory 📖CompOp
3 mathmath: comp_hom, comp_hom_assoc, id_hom
sc₁ 📖CompOp
6 mathmath: sc₁_f, sc₁_X₁, sc₁_X₃, sc₁_X₂, exact₁, sc₁_g
sc₂ 📖CompOp
6 mathmath: sc₂_X₃, exact₂, sc₂_g, sc₂_X₁, sc₂_X₂, sc₂_f
sc₃ 📖CompOp
6 mathmath: sc₃_g, sc₃_X₁, exact₃, sc₃_X₃, sc₃_X₂, sc₃_f
δ 📖CompOp
42 mathmath: δ_eq_zero_of_isIso₂, δToCycles_iCycles, toCycles_πE_d, d_ιE_fromOpcycles, toCycles_πE_d_assoc, δ_toCycles, sc₁_f, δ_δ_assoc, pOpcycles_δFromOpcycles, kernelSequenceCycles_g, δ_δ, shortComplex_g, sc₃_g, d_EIsoH_hom, zero₃, kernelSequenceE_g, fromOpcyles_δ_assoc, toCycles_Ψ_assoc, Ψ_fromOpcycles_assoc, iCycles_δ, Hom.comm, d_ιE_fromOpcycles_assoc, zero₁, δ_naturality_assoc, δ_naturality, d_EIsoH_hom_assoc, shortComplex_f, δ_pOpcycles_assoc, Hom.comm_assoc, δ_toCycles_assoc, Ψ_fromOpcycles, δToCycles_iCycles_assoc, zero₃_assoc, cokernelSequenceOpcycles_f, δ_pOpcycles, δ_eq_zero_of_isIso₁, toCycles_Ψ, cokernelSequenceE_f, iCycles_δ_assoc, zero₁_assoc, pOpcycles_δFromOpcycles_assoc, fromOpcyles_δ
δ' 📖CompOp
2 mathmath: exact₁', exact₃'

Theorems

NameKindAssumesProvesValidatesDepends On
comp_hom 📖mathematicalHom.hom
CategoryTheory.CategoryStruct.comp
CategoryTheory.Abelian.SpectralObject
CategoryTheory.Category.toCategoryStruct
instCategory
CategoryTheory.Functor
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
comp_hom_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Functor
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
CategoryTheory.Category.toCategoryStruct
H
Hom.hom
CategoryTheory.Abelian.SpectralObject
instCategory
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
comp_hom
composableArrows₅_exact 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ComposableArrows.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
composableArrows₅
CategoryTheory.ComposableArrows.exact_of_δ₀
CategoryTheory.ShortComplex.Exact.exact_toComposableArrows
exact₂
exact₃
exact₁
epi_H_map_twoδ₁Toδ₀ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Epi
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
CategoryTheory.ShortComplex.Exact.epi_f
exact₃
CategoryTheory.Limits.IsZero.eq_of_tgt
epi_H_map_twoδ₁Toδ₀' 📖mathematicalPreorder.toLE
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
Preorder.smallCategory
CategoryTheory.Functor.category
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.homOfLE
CategoryTheory.Epi
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
Preorder.smallCategory
CategoryTheory.Functor.category
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.homOfLE
LE.le.trans
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀'
epi_H_map_twoδ₁Toδ₀
LE.le.trans
exact₁ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₁
CategoryTheory.ComposableArrows.Exact.exact
exact₁'
exact₁' 📖mathematicalCategoryTheory.ComposableArrows.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.ComposableArrows.mk₂
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
CategoryTheory.Functor.comp
CategoryTheory.ComposableArrows.functorArrows
H
CategoryTheory.NatTrans.app
δ'
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.mapFunctorArrows
exact₂ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₂
CategoryTheory.ComposableArrows.Exact.exact
exact₂'
exact₂' 📖mathematicalCategoryTheory.ComposableArrows.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.ComposableArrows.mk₂
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.functorArrows
CategoryTheory.Functor.map
CategoryTheory.NatTrans.app
CategoryTheory.ComposableArrows.mapFunctorArrows
exact₃ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₃
CategoryTheory.ComposableArrows.Exact.exact
exact₃'
exact₃' 📖mathematicalCategoryTheory.ComposableArrows.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.ComposableArrows.mk₂
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.functorArrows
CategoryTheory.Functor.comp
CategoryTheory.Functor.map
CategoryTheory.NatTrans.app
CategoryTheory.ComposableArrows.mapFunctorArrows
δ'
id_hom 📖mathematicalHom.hom
CategoryTheory.CategoryStruct.id
CategoryTheory.Abelian.SpectralObject
CategoryTheory.Category.toCategoryStruct
instCategory
CategoryTheory.Functor
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
isIso_H_map_twoδ₁Toδ₀ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.IsIso
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
mono_H_map_twoδ₁Toδ₀
epi_H_map_twoδ₁Toδ₀
CategoryTheory.isIso_of_mono_of_epi
CategoryTheory.balanced_of_strongMonoCategory
CategoryTheory.strongMonoCategory_of_regularMonoCategory
CategoryTheory.regularMonoCategoryOfNormalMonoCategory
CategoryTheory.Abelian.toIsNormalMonoCategory
isIso_H_map_twoδ₁Toδ₀' 📖mathematicalPreorder.toLE
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
Preorder.smallCategory
CategoryTheory.Functor.category
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.homOfLE
CategoryTheory.IsIso
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
Preorder.smallCategory
CategoryTheory.Functor.category
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.homOfLE
LE.le.trans
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀'
isIso_H_map_twoδ₁Toδ₀
LE.le.trans
isZero_H_map_mk₁_of_isIso 📖mathematicalCategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.IsIso.hom_inv_id
CategoryTheory.ComposableArrows.isIso_iff₁
CategoryTheory.IsIso.comp_isIso
CategoryTheory.IsIso.id
CategoryTheory.IsIso.inv_isIso
CategoryTheory.Limits.IsZero.iff_id_eq_zero
CategoryTheory.cancel_mono
CategoryTheory.mono_of_strongMono
CategoryTheory.instStrongMonoOfIsRegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono
CategoryTheory.instIsSplitMonoMap
CategoryTheory.instIsSplitMonoComp
CategoryTheory.IsSplitMono.of_iso
CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁
CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀
CategoryTheory.Category.id_comp
CategoryTheory.Limits.zero_comp
zero₂
CategoryTheory.Functor.map_comp
mono_H_map_twoδ₁Toδ₀ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Mono
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
CategoryTheory.ShortComplex.Exact.mono_g
exact₂
CategoryTheory.Limits.IsZero.eq_of_src
mono_H_map_twoδ₁Toδ₀' 📖mathematicalPreorder.toLE
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
Preorder.smallCategory
CategoryTheory.Functor.category
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.homOfLE
CategoryTheory.Mono
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
Preorder.smallCategory
CategoryTheory.Functor.category
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.homOfLE
LE.le.trans
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀'
mono_H_map_twoδ₁Toδ₀
LE.le.trans
sc₁_X₁ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₁
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₁
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₁_X₂ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₂
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₁
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₁_X₃ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₃
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₁
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₁_f 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.f
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₁
δ
sc₁_g 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.g
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.ComposableArrows.twoδ₂Toδ₁
sc₂_X₁ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₁
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₂
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₂_X₂ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₂
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₂
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₂_X₃ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₃
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₂
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₂_f 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.f
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₂
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.ComposableArrows.twoδ₂Toδ₁
sc₂_g 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.g
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₂
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
sc₃_X₁ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₁
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₃
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₃_X₂ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₂
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₃
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₃_X₃ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.X₃
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₃
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
sc₃_f 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.f
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₃
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
sc₃_g 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.g
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
sc₃
δ
zero₁ 📖mathematicalCategoryTheory.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₁
δ
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₂Toδ₁
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.ComposableArrows.IsComplex.zero
CategoryTheory.ComposableArrows.Exact.toIsComplex
exact₁'
zero₁_assoc 📖mathematicalCategoryTheory.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₁
δ
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₂Toδ₁
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
zero₁
zero₂ 📖mathematicalCategoryTheory.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₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₂Toδ₁
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.ComposableArrows.IsComplex.zero
CategoryTheory.ComposableArrows.Exact.toIsComplex
exact₂'
zero₂_assoc 📖mathematicalCategoryTheory.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₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₂Toδ₁
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
zero₂
zero₃ 📖mathematicalCategoryTheory.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₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
δ
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.ComposableArrows.IsComplex.zero
CategoryTheory.ComposableArrows.Exact.toIsComplex
exact₃'
zero₃_assoc 📖mathematicalCategoryTheory.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₁
CategoryTheory.Functor.map
CategoryTheory.ComposableArrows.twoδ₁Toδ₀
δ
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
zero₃
δ_naturality 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.NatTrans.app
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Functor.map
δ
CategoryTheory.ComposableArrows.naturality'
le_rfl
CategoryTheory.NatTrans.naturality
CategoryTheory.ComposableArrows.homMk₁.congr_simp
CategoryTheory.ComposableArrows.hom_ext₁
δ_naturality_assoc 📖mathematicalQuiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.NatTrans.app
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Functor.map
δ
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
δ_naturality
δ_δ 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
δ
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
δ_naturality
CategoryTheory.Category.comp_id
CategoryTheory.Functor.map_id
zero₁_assoc
CategoryTheory.Limits.zero_comp
δ_δ_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
H
CategoryTheory.ComposableArrows.mk₁
δ
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
δ_δ

CategoryTheory.Abelian.SpectralObject.Hom

Definitions

NameCategoryTheorems
hom 📖CompOp
6 mathmath: CategoryTheory.Abelian.SpectralObject.comp_hom, CategoryTheory.Abelian.SpectralObject.comp_hom_assoc, comm, CategoryTheory.Abelian.SpectralObject.id_hom, comm_assoc, ext_iff

Theorems

NameKindAssumesProvesValidatesDepends On
comm 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
CategoryTheory.Abelian.SpectralObject.H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Abelian.SpectralObject.δ
CategoryTheory.NatTrans.app
hom
comm_assoc 📖mathematicalCategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Functor.obj
CategoryTheory.ComposableArrows
CategoryTheory.Functor.category
Preorder.smallCategory
PartialOrder.toPreorder
Fin.instPartialOrder
CategoryTheory.Abelian.SpectralObject.H
CategoryTheory.ComposableArrows.mk₁
CategoryTheory.Abelian.SpectralObject.δ
CategoryTheory.NatTrans.app
hom
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
comm
ext 📖hom
ext_iff 📖mathematicalhomext

---

← Back to Index