HasSpectralSequence

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

Statistics

Metric	Count
Definitions HasSpectralSequence, IsFirstQuadrant, IsThirdQuadrant, SpectralSequenceDataCore, deg, i₀, i₁, i₂, i₃, coreE₂Cohomological, coreE₂CohomologicalFin, coreE₂CohomologicalNat, coreE₂HomologicalNat	13
Theorems isZero_H_obj_mk₁_i₀_le, isZero_H_obj_mk₁_i₃_le, isZero₁, isZero₂, isZero₁, isZero₂, antitone_i₀, hc, hc₀₂, hc₁₃, i₀_le, i₀_le', i₀_prev, i₃_le, i₃_next, le₀₁, le₀₁', le₁₂, le₁₂', le₂₃, le₂₃', le₃₃', monotone_i₃, coreE₂CohomologicalFin_deg, coreE₂CohomologicalFin_i₀, coreE₂CohomologicalFin_i₁, coreE₂CohomologicalFin_i₂, coreE₂CohomologicalFin_i₃, coreE₂CohomologicalNat_deg, coreE₂CohomologicalNat_i₀, coreE₂CohomologicalNat_i₁, coreE₂CohomologicalNat_i₂, coreE₂CohomologicalNat_i₃, coreE₂Cohomological_deg, coreE₂Cohomological_i₀, coreE₂Cohomological_i₁, coreE₂Cohomological_i₂, coreE₂Cohomological_i₃, coreE₂HomologicalNat_deg, coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_i₁, coreE₂HomologicalNat_i₂, coreE₂HomologicalNat_i₃, instHasSpectralSequenceEIntProdIntCoreE₂Cohomological, instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat, instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat, instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin, isZero_H_obj_mk₁_i₀_le, isZero_H_obj_mk₁_i₀_le', isZero_H_obj_mk₁_i₃_le, isZero_H_obj_mk₁_i₃_le', isZero₁_of_isFirstQuadrant, isZero₁_of_isThirdQuadrant, isZero₂_of_isFirstQuadrant, isZero₂_of_isThirdQuadrant	55
Total	68

CategoryTheory.Abelian.SpectralObject

Definitions

Name	Category	Theorems
HasSpectralSequence 📖	CompData	4 math math: instHasSpectralSequenceEIntProdIntCoreE₂Cohomological, instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat, instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin, instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat
IsFirstQuadrant 📖	CompData	—
IsThirdQuadrant 📖	CompData	—
SpectralSequenceDataCore 📖	CompData	—
coreE₂Cohomological 📖	CompOp	6 math math: coreE₂Cohomological_i₃, instHasSpectralSequenceEIntProdIntCoreE₂Cohomological, coreE₂Cohomological_i₂, coreE₂Cohomological_deg, coreE₂Cohomological_i₀, coreE₂Cohomological_i₁
coreE₂CohomologicalFin 📖	CompOp	6 math math: coreE₂CohomologicalFin_deg, coreE₂CohomologicalFin_i₃, coreE₂CohomologicalFin_i₀, coreE₂CohomologicalFin_i₂, coreE₂CohomologicalFin_i₁, instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin
coreE₂CohomologicalNat 📖	CompOp	6 math math: coreE₂CohomologicalNat_i₂, coreE₂CohomologicalNat_deg, coreE₂CohomologicalNat_i₁, coreE₂CohomologicalNat_i₀, coreE₂CohomologicalNat_i₃, instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat
coreE₂HomologicalNat 📖	CompOp	6 math math: coreE₂HomologicalNat_deg, coreE₂HomologicalNat_i₂, instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat, coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_i₁, coreE₂HomologicalNat_i₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreE₂CohomologicalFin_deg 📖	mathematical	—	SpectralSequenceDataCore.deg PartialOrder.toPreorder Fin.instPartialOrder ComplexShape.spectralSequenceFin coreE₂CohomologicalFin	—	—
coreE₂CohomologicalFin_i₀ 📖	mathematical	—	SpectralSequenceDataCore.i₀ PartialOrder.toPreorder Fin.instPartialOrder ComplexShape.spectralSequenceFin coreE₂CohomologicalFin	—	—
coreE₂CohomologicalFin_i₁ 📖	mathematical	—	SpectralSequenceDataCore.i₁ PartialOrder.toPreorder Fin.instPartialOrder ComplexShape.spectralSequenceFin coreE₂CohomologicalFin	—	—
coreE₂CohomologicalFin_i₂ 📖	mathematical	—	SpectralSequenceDataCore.i₂ PartialOrder.toPreorder Fin.instPartialOrder ComplexShape.spectralSequenceFin coreE₂CohomologicalFin	—	—
coreE₂CohomologicalFin_i₃ 📖	mathematical	—	SpectralSequenceDataCore.i₃ PartialOrder.toPreorder Fin.instPartialOrder ComplexShape.spectralSequenceFin coreE₂CohomologicalFin	—	—
coreE₂CohomologicalNat_deg 📖	mathematical	—	SpectralSequenceDataCore.deg EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂CohomologicalNat	—	—
coreE₂CohomologicalNat_i₀ 📖	mathematical	—	SpectralSequenceDataCore.i₀ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂CohomologicalNat WithBotTop.coe	—	—
coreE₂CohomologicalNat_i₁ 📖	mathematical	—	SpectralSequenceDataCore.i₁ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂CohomologicalNat WithBotTop.coe	—	—
coreE₂CohomologicalNat_i₂ 📖	mathematical	—	SpectralSequenceDataCore.i₂ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂CohomologicalNat WithBotTop.coe	—	—
coreE₂CohomologicalNat_i₃ 📖	mathematical	—	SpectralSequenceDataCore.i₃ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂CohomologicalNat WithBotTop.coe	—	—
coreE₂Cohomological_deg 📖	mathematical	—	SpectralSequenceDataCore.deg EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.up' Prod.instAdd Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add Preorder.toLE Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddGroup Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instLinearOrder coreE₂Cohomological	—	Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono contravariant_lt_of_covariant_le
coreE₂Cohomological_i₀ 📖	mathematical	—	SpectralSequenceDataCore.i₀ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.up' Prod.instAdd Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add Preorder.toLE Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddGroup Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instLinearOrder coreE₂Cohomological WithBotTop.coe	—	Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono contravariant_lt_of_covariant_le
coreE₂Cohomological_i₁ 📖	mathematical	—	SpectralSequenceDataCore.i₁ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.up' Prod.instAdd Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add Preorder.toLE Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddGroup Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instLinearOrder coreE₂Cohomological WithBotTop.coe	—	Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono contravariant_lt_of_covariant_le
coreE₂Cohomological_i₂ 📖	mathematical	—	SpectralSequenceDataCore.i₂ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.up' Prod.instAdd Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add Preorder.toLE Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddGroup Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instLinearOrder coreE₂Cohomological WithBotTop.coe	—	Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono contravariant_lt_of_covariant_le
coreE₂Cohomological_i₃ 📖	mathematical	—	SpectralSequenceDataCore.i₃ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.up' Prod.instAdd Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add Preorder.toLE Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddGroup Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instLinearOrder coreE₂Cohomological WithBotTop.coe	—	Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono contravariant_lt_of_covariant_le
coreE₂HomologicalNat_deg 📖	mathematical	—	SpectralSequenceDataCore.deg EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂HomologicalNat	—	—
coreE₂HomologicalNat_i₀ 📖	mathematical	—	SpectralSequenceDataCore.i₀ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂HomologicalNat WithBotTop.coe	—	—
coreE₂HomologicalNat_i₁ 📖	mathematical	—	SpectralSequenceDataCore.i₁ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂HomologicalNat WithBotTop.coe	—	—
coreE₂HomologicalNat_i₂ 📖	mathematical	—	SpectralSequenceDataCore.i₂ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂HomologicalNat WithBotTop.coe	—	—
coreE₂HomologicalNat_i₃ 📖	mathematical	—	SpectralSequenceDataCore.i₃ EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂HomologicalNat WithBotTop.coe	—	—
instHasSpectralSequenceEIntProdIntCoreE₂Cohomological 📖	mathematical	—	HasSpectralSequence EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.up' Prod.instAdd Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add Preorder.toLE Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddGroup Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instLinearOrder coreE₂Cohomological	—	Prod.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono contravariant_lt_of_covariant_le SpectralSequenceDataCore.i₀_le SpectralSequenceDataCore.i₃_le sub_add_cancel
instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat 📖	mathematical	—	HasSpectralSequence EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂CohomologicalNat	—	SpectralSequenceDataCore.i₀_le isZero₁_of_isFirstQuadrant SpectralSequenceDataCore.i₃_le isZero₂_of_isFirstQuadrant
instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat 📖	mathematical	—	HasSpectralSequence EInt WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt ComplexShape.spectralSequenceNat coreE₂HomologicalNat	—	SpectralSequenceDataCore.i₀_le isZero₂_of_isThirdQuadrant SpectralSequenceDataCore.i₃_le isZero₁_of_isThirdQuadrant
instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin 📖	mathematical	—	HasSpectralSequence PartialOrder.toPreorder Fin.instPartialOrder ComplexShape.spectralSequenceFin coreE₂CohomologicalFin	—	Nat.cast_add Nat.cast_one add_sub_cancel_left CategoryTheory.isIso_homOfLE isZero_H_map_mk₁_of_isIso SpectralSequenceDataCore.i₀_le add_sub_cancel_right Fin.clamp_eq_last SpectralSequenceDataCore.i₃_le
isZero_H_obj_mk₁_i₀_le 📖	mathematical	ComplexShape.Rel SpectralSequenceDataCore.deg	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ SpectralSequenceDataCore.i₀ CategoryTheory.homOfLE SpectralSequenceDataCore.i₀_le	—	HasSpectralSequence.isZero_H_obj_mk₁_i₀_le
isZero_H_obj_mk₁_i₀_le' 📖	mathematical	ComplexShape.Rel SpectralSequenceDataCore.deg SpectralSequenceDataCore.i₀	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	HasSpectralSequence.isZero_H_obj_mk₁_i₀_le
isZero_H_obj_mk₁_i₃_le 📖	mathematical	ComplexShape.Rel SpectralSequenceDataCore.deg	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ SpectralSequenceDataCore.i₃ CategoryTheory.homOfLE SpectralSequenceDataCore.i₃_le	—	HasSpectralSequence.isZero_H_obj_mk₁_i₃_le
isZero_H_obj_mk₁_i₃_le' 📖	mathematical	ComplexShape.Rel SpectralSequenceDataCore.deg SpectralSequenceDataCore.i₃	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	HasSpectralSequence.isZero_H_obj_mk₁_i₃_le
isZero₁_of_isFirstQuadrant 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	IsFirstQuadrant.isZero₁
isZero₁_of_isThirdQuadrant 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop Preorder.toLT WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	IsThirdQuadrant.isZero₁
isZero₂_of_isFirstQuadrant 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop Preorder.toLT WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	IsFirstQuadrant.isZero₂
isZero₂_of_isThirdQuadrant 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	IsThirdQuadrant.isZero₂

CategoryTheory.Abelian.SpectralObject.HasSpectralSequence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_H_obj_mk₁_i₀_le 📖	mathematical	ComplexShape.Rel CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Abelian.SpectralObject.H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀ CategoryTheory.homOfLE CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le	—	—
isZero_H_obj_mk₁_i₃_le 📖	mathematical	ComplexShape.Rel CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Preorder.smallCategory CategoryTheory.Functor.category PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Abelian.SpectralObject.H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃ CategoryTheory.homOfLE CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_le	—	—

CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero₁ 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder CategoryTheory.Abelian.SpectralObject.H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	—
isZero₂ 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop Preorder.toLT WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder CategoryTheory.Abelian.SpectralObject.H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	—

CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero₁ 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop Preorder.toLT WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder CategoryTheory.Abelian.SpectralObject.H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	—
isZero₂ 📖	mathematical	EInt Preorder.toLE WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithBotTop.coe	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows EInt Preorder.smallCategory WithBot.instPreorder WithTop WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt CategoryTheory.Functor.category Fin.instPartialOrder CategoryTheory.Abelian.SpectralObject.H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.homOfLE	—	—

CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore

Definitions

Name	Category	Theorems
deg 📖	CompOp	5 math math: CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_deg, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_deg, hc
i₀ 📖	CompOp	11 math math: CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₀, hc₀₂, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le, i₀_le, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₀, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₀, le₀₁, i₀_prev, antitone_i₀
i₁ 📖	CompOp	8 math math: le₁₂, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₁, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₁, hc₁₃, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₁, le₀₁, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₁, i₀_prev
i₂ 📖	CompOp	8 math math: le₂₃, i₃_next, hc₀₂, le₁₂, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₂, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₂, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₂, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₂
i₃ 📖	CompOp	11 math math: le₂₃, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₃, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₃, i₃_next, monotone_i₃, hc₁₃, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le, i₃_le, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₃, CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_i₀ 📖	mathematical	—	Preorder.toLE i₀	—	—
hc 📖	mathematical	ComplexShape.Rel	deg	—	—
hc₀₂ 📖	mathematical	ComplexShape.Rel	i₀ i₂	—	—
hc₁₃ 📖	mathematical	ComplexShape.Rel	i₁ i₃	—	—
i₀_le 📖	mathematical	—	Preorder.toLE i₀	—	antitone_i₀
i₀_le' 📖	mathematical	i₀	Preorder.toLE	—	antitone_i₀
i₀_prev 📖	mathematical	ComplexShape.Rel	i₀ i₁	—	—
i₃_le 📖	mathematical	—	Preorder.toLE i₃	—	monotone_i₃
i₃_next 📖	mathematical	ComplexShape.Rel	i₃ i₂	—	—
le₀₁ 📖	mathematical	—	Preorder.toLE i₀ i₁	—	—
le₀₁' 📖	mathematical	i₀ i₁	Preorder.toLE	—	le₀₁
le₁₂ 📖	mathematical	—	Preorder.toLE i₁ i₂	—	—
le₁₂' 📖	mathematical	i₁ i₂	Preorder.toLE	—	le₁₂
le₂₃ 📖	mathematical	—	Preorder.toLE i₂ i₃	—	—
le₂₃' 📖	mathematical	i₂ i₃	Preorder.toLE	—	le₂₃
le₃₃' 📖	mathematical	i₃	Preorder.toLE	—	monotone_i₃
monotone_i₃ 📖	mathematical	—	Preorder.toLE i₃	—	—

---

← Back to Index