feat(Algebra/Homology): spectral sequences#33842
feat(Algebra/Homology): spectral sequences#33842joelriou wants to merge 99 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
large-import
PR summary 99884c2730Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE | 1080 | 1159 | +79 (+7.31%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE |
79 |
Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (new file) |
101 |
Mathlib.Order.Fin.Clamp (new file) |
342 |
Mathlib.Algebra.Homology.SpectralObject.Basic (new file) |
781 |
Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (new file) |
786 |
Mathlib.Algebra.Homology.SpectralObject.Cycles (new file) |
833 |
Mathlib.Algebra.Homology.SpectralObject.Page (new file) |
837 |
Mathlib.Algebra.Homology.SpectralObject.Differentials (new file) |
838 |
Mathlib.Algebra.Homology.SpectralObject.EpiMono (new file) |
840 |
Mathlib.Algebra.Homology.SpectralObject.Homology (new file) |
841 |
Mathlib.Algebra.Homology.SpectralSequence.Basic (new file) |
946 |
Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (new file) |
969 |
Mathlib.Algebra.Homology.SpectralObject.FirstPage (new file) |
970 |
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (new file) |
1160 |
Mathlib.CategoryTheory.Triangulated.TStructure.Induced (new file) |
1161 |
Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (new file) |
1162 |
Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (new file) |
1166 |
Declarations diff
+ CohomologicalSpectralSequence
+ CohomologicalSpectralSequenceFin
+ CohomologicalSpectralSequenceNat
+ E
+ EIsoH
+ EIsoH_hom_naturality
+ EIsoH_hom_opcyclesIsoH_inv
+ EMap
+ EMapFourδ₁Toδ₀'
+ EMapFourδ₁Toδ₀'_EMapFourδ₃Toδ₃'
+ EMapFourδ₁Toδ₀'_comp
+ EMapFourδ₂Toδ₁'
+ EMapFourδ₄Toδ₃'
+ EMapFourδ₄Toδ₃'_comp
+ EMap_comp
+ EMap_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃
+ EMap_fourδ₁Toδ₀_d
+ EMap_id
+ EMap_ιE
+ EToCycles
+ EToCycles_i
+ E₂CohomologicalSpectralSequence
+ E₂CohomologicalSpectralSequenceFin
+ E₂CohomologicalSpectralSequenceNat
+ E₂HomologicalSpectralSequenceNat
+ E₂SpectralSequence
+ E₂SpectralSequenceNat
+ H_map_twoδ₂Toδ₁_toCycles
+ HasFirstPageComputation
+ HasInducedTStructure
+ HasInducedTStructure.mk'
+ HasSpectralSequence
+ IsFirstQuadrant
+ IsThirdQuadrant
+ SpectralObject
+ SpectralSequence
+ SpectralSequenceMkData
+ cc
+ ccSc
+ ccSc_exact
+ cc_w
+ cokernelIsoCycles
+ cokernelIsoCycles_hom_fac
+ cokernelSequenceCycles
+ cokernelSequenceCyclesE
+ cokernelSequenceCyclesEIso
+ cokernelSequenceCyclesE_exact
+ cokernelSequenceCycles_exact
+ cokernelSequenceE
+ cokernelSequenceE_exact
+ cokernelSequenceOpcycles
+ cokernelSequenceOpcyclesE
+ cokernelSequenceOpcyclesE_exact
+ cokernelSequenceOpcycles_exact
+ composableArrows₅
+ composableArrows₅_exact
+ cycles
+ cyclesIso
+ cyclesIsoH
+ cyclesIsoH_hom_EIsoH_inv
+ cyclesIsoH_hom_inv_id
+ cyclesIsoH_inv
+ cyclesIsoH_inv_hom_id
+ cyclesIso_hom_i
+ cyclesIso_inv_cyclesMap
+ cyclesIso_inv_i
+ cyclesMap
+ cyclesMap_comp
+ cyclesMap_i
+ cyclesMap_id
+ cyclesMap_Ψ
+ cyclesMap_Ψ_exact
+ d
+ dCokernelSequence
+ dCokernelSequence_exact
+ dHomologyData
+ dHomologyIso
+ dKernelSequence
+ dKernelSequence_exact
+ dShortComplex
+ d_EIsoH_hom
+ d_EMap_fourδ₄Toδ₃
+ d_d
+ d_ιE_fromOpcycles
+ descCycles
+ descE
+ descOpcycles
+ descTruncGE
+ descTruncGE_aux
+ descTruncGT
+ descTruncGT_aux
+ eTriangleLTGE
+ eTriangleLTGE_distinguished
+ eTruncGE
+ eTruncGEIsoGEGE
+ eTruncGEIsoGEGE_hom_inv_id_app
+ eTruncGEIsoGEGE_inv_hom_id_app
+ eTruncGEToGEGE
+ eTruncGE_obj_bot
+ eTruncGE_obj_coe
+ eTruncGE_obj_map_eTruncGEπ_app
+ eTruncGE_obj_top
+ eTruncGEδLT
+ eTruncGEδLT_coe
+ eTruncGEπ
+ eTruncGEπ_app_eTruncGE_map_app
+ eTruncGEπ_bot
+ eTruncGEπ_coe
+ eTruncGEπ_naturality
+ eTruncGEπ_top
+ eTruncLT
+ eTruncLTGEIsoLEGT
+ eTruncLTGEIsoLEGT_hom_app_fac
+ eTruncLTGEIsoLEGT_hom_app_fac'
+ eTruncLTGEIsoLEGT_hom_naturality
+ eTruncLTGEIsoLEGT_naturality_app
+ eTruncLTGELTSelfToGELT
+ eTruncLTGELTSelfToLTGE
+ eTruncLTLTIsoLT
+ eTruncLTLTIsoLT_hom_inv_id_app
+ eTruncLTLTIsoLT_inv_hom_id_app
+ eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj
+ eTruncLTLTToLT
+ eTruncLT_map_app_eTruncLTι_app
+ eTruncLT_map_eq_truncLTι
+ eTruncLT_obj_bot
+ eTruncLT_obj_coe
+ eTruncLT_obj_map_eTruncLTι_app
+ eTruncLT_obj_top
+ eTruncLT_ι_bot
+ eTruncLT_ι_coe
+ eTruncLT_ι_top
+ eTruncLTι
+ eTruncLTι_naturality
+ epi_EMap
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ exact₁
+ exact₂
+ exact₃
+ fac
+ fromOpcycles
+ fromOpcycles_H_map_twoδ₁Toδ₀
+ fromOpcyles_δ
+ from_truncGE_obj_ext
+ hom_ext
+ homologyData
+ homologyDataEIdId
+ homologyIso
+ homologyIso'
+ iCycles
+ iCycles_δ
+ instance (E : SpectralObject C EInt) : E.HasSpectralSequence mkDataE₂Cohomological
+ instance (P P' : ObjectProperty C) [P.IsTriangulated] [P'.IsTriangulated] (t : TStructure C)
+ instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELE a b).obj X) a := by
+ instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELT a b).obj X) a := by
+ instance (X : C) (a b : ℤ) : t.IsLE ((t.truncLTGE a b).obj X) (b - 1) := by
+ instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGT b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] :
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncGE a).obj X) b := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLE a).obj X) b := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLT a).obj X) b := by
+ instance (X : C) (n : ℤ) : IsIso ((t.truncGE n).map ((t.truncGEπ n).app X))
+ instance (X : C) (n : ℤ) : IsIso ((t.truncLE n).map ((t.truncLEι n).app X))
+ instance (X : C) (n : ℤ) : IsIso ((t.truncLT n).map ((t.truncLTι n).app X))
+ instance (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n
+ instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT (n + 1)).obj X) n
+ instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1)
+ instance (X : C) (n : ℤ) [t.IsGE X n] : IsIso ((t.truncGEπ n).app X) := by
+ instance (X : C) (n : ℤ) [t.IsLE X n] : IsIso ((t.truncLEι n).app X) := by
+ instance (a : EInt) (X : C) : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))
+ instance (a : EInt) (X : C) : IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X)) := by
+ instance (a b : ℤ) : IsIso (t.truncGELTToLTGE a b) := by
+ instance (i : EInt) : (t.eTruncGE.obj i).Additive := by
+ instance (i : EInt) : (t.eTruncLT.obj i).Additive := by
+ instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT (n - 1)).obj X) n
+ instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT n).obj X) (n + 1)
+ instance (n : ℤ) (X : C) : t.IsLE ((t.truncLE n).obj X) n
+ instance (n : ℤ) : (t.truncGT n).Additive := by
+ instance (n : ℤ) : (t.truncLE n).Additive := by
+ instance (n : ℤ) : t.IsGE (0 : C) n := t.isGE_of_isZero (isZero_zero C) n
+ instance (n : ℤ) : t.IsLE (0 : C) n := t.isLE_of_isZero (isZero_zero C) n
+ instance : Category (SpectralObject C ι)
+ instance : Category (SpectralSequence C c r₀)
+ instance : Epi (X.cokernelSequenceCycles n f g fg h).g := by
+ instance : Epi (X.cokernelSequenceCyclesE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃).g := by
+ instance : Epi (X.cokernelSequenceE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₁₂ h₁₂).g := by
+ instance : Epi (X.cokernelSequenceOpcycles n₀ n₁ hn₁ f g).g := by
+ instance : Epi (X.cokernelSequenceOpcyclesE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₁₂ h₁₂).g := by
+ instance : Epi (X.dCokernelSequence n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄).g := by
+ instance : Epi (X.opcyclesToE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₁₂ h₁₂)
+ instance : Epi (X.pOpcycles n f g) := by
+ instance : Epi (X.toCycles n f g fg h)
+ instance : Epi (ccSc X data r r' hrr' hr pq pq' n₀ n₁ n₂ hn₁ hn₂ hn₁'
+ instance : IsIso (t.eTruncGEπ ⊥) := by
+ instance : IsIso (t.eTruncLTGELTSelfToGELT a b) := by
+ instance : IsIso (t.eTruncLTGELTSelfToLTGE a b) := by
+ instance : IsIso (t.eTruncLTι ⊤) := by
+ instance : Mono (X.EToCycles n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₂₃ h₂₃)
+ instance : Mono (X.dKernelSequence n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃).f := by
+ instance : Mono (X.fromOpcycles n f g fg h)
+ instance : Mono (X.iCycles n f g) := by
+ instance : Mono (X.kernelSequenceCycles n₀ n₁ hn₁ f g).f := by
+ instance : Mono (X.kernelSequenceCyclesE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₂₃ h₂₃).f := by
+ instance : Mono (X.kernelSequenceE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₂₃ h₂₃).f := by
+ instance : Mono (X.kernelSequenceOpcycles n f g fg h).f := by
+ instance : Mono (X.kernelSequenceOpcyclesE n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃).f := by
+ instance : Mono (kfSc X data r r' hrr' hr pq' pq'' n₀ n₁ n₂ hn₁ hn₂ hn₁'
+ instance : Y.HasSpectralSequence mkDataE₂CohomologicalNat
+ instance : Y.HasSpectralSequence mkDataE₂HomologicalNat
+ instance : mkDataE₂Cohomological.HasFirstPageComputation
+ instance : mkDataE₂CohomologicalNat.HasFirstPageComputation
+ instance : mkDataE₂HomologicalNat.HasFirstPageComputation
+ instance : t.bounded.HasInducedTStructure t := by
+ instance : t.bounded.IsTriangulated := by
+ instance : t.minus.HasInducedTStructure t
+ instance : t.minus.IsTriangulated
+ instance : t.plus.HasInducedTStructure t
+ instance : t.plus.IsTriangulated
+ instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
+ isColimitCc
+ isGE_eTruncGE_obj_obj
+ isGE_iff_isIso_truncGEπ_app
+ isGE_iff_isIso_truncGTπ_app
+ isGE_iff_isZero_truncLE_obj
+ isGE_iff_isZero_truncLT_obj
+ isGE_iff_orthogonal
+ isGE_of_isZero
+ isGE_truncGE_obj
+ isGE_truncGT_obj
+ isGE₂
+ isIso_EMap
+ isIso_EMapFourδ₂Toδ₁'
+ isIso_EMap_fourδ₁Toδ₀
+ isIso_EMap_fourδ₁Toδ₀_of_isZero
+ isIso_EMap_fourδ₄Toδ₃
+ isIso_EMap_fourδ₄Toδ₃_of_isZero
+ isIso_H_map_twoδ₁Toδ₀
+ isIso_H_map_twoδ₁Toδ₀'
+ isIso_eTruncGEIsoGEGE
+ isIso_eTruncGE_obj_map_truncGEπ_app
+ isIso_eTruncLTLTIsoLT
+ isIso_eTruncLT_obj_map_truncLTπ_app
+ isIso_fromOpcycles
+ isIso_toCycles
+ isIso_truncGE_map_iff
+ isIso_truncGE_map_truncGEπ_app
+ isIso_truncGT_map_iff
+ isIso_truncGT_map_truncGTπ_app
+ isIso_truncLE_map_iff
+ isIso_truncLE_map_truncLEι_app
+ isIso_truncLT_map_iff
+ isIso_truncLT_map_truncLTι_app
+ isIso₁_truncLE_map_of_isGE
+ isIso₁_truncLT_map_of_isGE
+ isIso₂_truncGE_map_of_isLE
+ isIso₂_truncGT_map_of_isLE
+ isLE_eTruncLT_obj_obj
+ isLE_iff_isIso_truncLEι_app
+ isLE_iff_isIso_truncLTι_app
+ isLE_iff_isZero_truncGE_obj
+ isLE_iff_isZero_truncGT_obj
+ isLE_iff_orthogonal
+ isLE_of_isZero
+ isLE_truncLE_obj
+ isLE_truncLT_obj
+ isLE₂
+ isLimitKf
+ isZero_E_of_isZero_H
+ isZero_H_map_mk₁_of_isIso
+ 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_H_obj_of_isIso
+ isZero_cycles
+ isZero_eTruncGE_obj_obj
+ isZero_eTruncLT_obj_obj
+ isZero_opcycles
+ isZero_spectralSequence_page_X_iff
+ isZero_spectralSequence_page_X_of_isZero_H
+ isZero_spectralSequence_page_X_of_isZero_H'
+ isZero_truncGE_obj_of_isLE
+ isZero_truncLE_obj_of_isGE
+ isZero_truncLT_obj_of_isGE
+ isZero₁_of_isFirstQuadrant
+ isZero₁_of_isThirdQuadrant
+ isZero₂_of_isFirstQuadrant
+ isZero₂_of_isThirdQuadrant
+ isoEMapFourδ₁Toδ₀'
+ isoEMapFourδ₁Toδ₀'_hom_inv_id
+ isoEMapFourδ₁Toδ₀'_inv_hom_id
+ isoEMapFourδ₄Toδ₃'
+ isoEMapFourδ₄Toδ₄'_hom_inv_id
+ isoEMapFourδ₄Toδ₄'_inv_hom_id
+ i₀_le
+ i₃_le
+ kernelSequenceCycles
+ kernelSequenceCyclesE
+ kernelSequenceCyclesE_exact
+ kernelSequenceCycles_exact
+ kernelSequenceE
+ kernelSequenceE_exact
+ kernelSequenceOpcycles
+ kernelSequenceOpcyclesE
+ kernelSequenceOpcyclesEIso
+ kernelSequenceOpcyclesE_exact
+ kernelSequenceOpcycles_exact
+ kf
+ kfSc
+ kfSc_exact
+ kf_w
+ leftHomologyDataShortComplexE
+ leftHomologyDataShortComplexE_f'
+ le₀'₀
+ le₀₁'
+ le₁₂'
+ le₂₃'
+ le₃₃'
+ liftCycles
+ liftCycles_i
+ liftE
+ liftE_ιE_fromOpcycles
+ liftOpcycles
+ liftOpcycles_fromOpcycles
+ liftTruncLE
+ liftTruncLE_aux
+ liftTruncLE_ι
+ liftTruncLT
+ liftTruncLT_aux
+ liftTruncLT_ι
+ mem_of_hasInductedTStructure
+ mkDataE₂Cohomological
+ mkDataE₂CohomologicalFin
+ mkDataE₂CohomologicalNat
+ mkDataE₂HomologicalNat
+ mk₃fac
+ mono_EMap
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ natTransTriangleLTGEOfLE
+ natTransTriangleLTGEOfLE_refl
+ natTransTriangleLTGEOfLE_trans
+ natTransTruncGEOfLE
+ natTransTruncGEOfLE_refl
+ natTransTruncGEOfLE_refl_app
+ natTransTruncGEOfLE_trans
+ natTransTruncGEOfLE_trans_app
+ natTransTruncLEOfLE
+ natTransTruncLEOfLE_refl
+ natTransTruncLEOfLE_refl_app
+ natTransTruncLEOfLE_trans
+ natTransTruncLEOfLE_trans_app
+ natTransTruncLEOfLE_ι
+ natTransTruncLEOfLE_ι_app
+ natTransTruncLTOfLE
+ natTransTruncLTOfLE_refl
+ natTransTruncLTOfLE_refl_app
+ natTransTruncLTOfLE_trans
+ natTransTruncLTOfLE_trans_app
+ natTransTruncLTOfLE_ι
+ natTransTruncLTOfLE_ι_app
+ onBounded
+ onMinus
+ onPlus
+ opcycles
+ opcyclesIso
+ opcyclesIsoH
+ opcyclesIsoH_hom
+ opcyclesIsoH_hom_inv_id
+ opcyclesIsoH_inv_hom_id
+ opcyclesIsoKernel
+ opcyclesIsoKernel_hom_fac
+ opcyclesIso_hom_δFromOpcycles
+ opcyclesMap
+ opcyclesMap_comp
+ opcyclesMap_fromOpcycles
+ opcyclesMap_id
+ opcyclesMap_opcyclesIso_hom
+ opcyclesMap_threeδ₂Toδ₁_opcyclesToE
+ opcyclesToE
+ opcyclesToE_EMap
+ opcyclesToE_ιE
+ pOpcycles
+ pOpcycles_δFromOpcycles
+ p_descOpcycles
+ p_fromOpcycles
+ p_opcyclesIso_hom
+ p_opcyclesIso_inv
+ p_opcyclesMap
+ p_opcyclesToE
+ page
+ pageD
+ pageD_eq
+ pageD_pageD
+ pageFunctor
+ pageHomologyNatIso
+ pageX
+ pageXIso
+ pageXIsoOfEq
+ rightHomologyDataShortComplexE
+ rightHomologyDataShortComplexE_g'
+ sc₁
+ sc₂
+ sc₃
+ sequenceΨ
+ sequenceΨ_exact
+ shortComplexE
+ shortComplexEMap
+ shortComplexEMap_comp
+ shortComplexEMap_id
+ shortComplexIso
+ shortComplexOpcyclesThreeδ₂Toδ₁
+ shortComplexOpcyclesThreeδ₂Toδ₁_exact
+ shortComplexOpcyclesThreeδ₂Toδ₁_shortExact
+ spectralObject
+ spectralObjectFunctor
+ spectralObject_δ
+ spectralSequence
+ spectralSequenceFin
+ spectralSequenceFin_rel_iff
+ spectralSequenceFirstPageXIso
+ spectralSequenceFirstPageXIso_hom
+ spectralSequenceFirstPageXIso_inv
+ spectralSequenceHomologyData
+ spectralSequenceHomologyData_left_i
+ spectralSequenceHomologyData_right_homologyIso_eq_left_homologyIso
+ spectralSequenceHomologyData_right_p
+ spectralSequenceNat
+ spectralSequenceNat_rel_iff
+ spectralSequencePageSc'Iso
+ spectralSequencePageXIso
+ spectralSequence_first_page_d_eq
+ spectralSequence_iso
+ spectralSequence_page_d_eq
+ tStructure
+ tStructure_isGE_iff
+ tStructure_isLE_iff
+ toCycles
+ toCycles_cyclesMap
+ toCycles_descCycles
+ toCycles_i
+ toCycles_Ψ
+ toCycles_πE_d
+ toCycles_πE_descE
+ to_truncLE_obj_ext
+ to_truncLT_obj_ext
+ triangleFunctorNatTransOfLE
+ triangleFunctorNatTransOfLE_app_hom₂
+ triangleFunctorNatTransOfLE_refl
+ triangleFunctorNatTransOfLE_trans
+ triangleLEGE
+ triangleLEGEIsoTriangleLTGE
+ triangleLEGE_distinguished
+ triangleLEGT
+ triangleLEGTIsoTriangleLEGE
+ triangleLEGT_distinguished
+ triangleLTLTGELT
+ triangleLTLTGELT_distinguished
+ triangleMapOfLE
+ triangleω₁δ
+ triangleω₁δObjIso
+ triangleω₁δ_distinguished
+ truncGELE
+ truncGELEIsoLEGE
+ truncGELEIsoTruncGELT
+ truncGELT
+ truncGELTIsoLTGE
+ truncGELTToLTGE
+ truncGELTToLTGE_app_pentagon
+ truncGELTToLTGE_app_pentagon_uniqueness
+ truncGELTδLT
+ truncGE_map_truncGEπ_app
+ truncGEδLE
+ truncGEδLT_comp_natTransTruncLTOfLE_app
+ truncGEδLT_comp_truncLTι
+ truncGEδLT_comp_truncLTι_app
+ truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE
+ truncGEπ_comp_truncGEδLT
+ truncGEπ_comp_truncGEδLT_app
+ truncGEπ_naturality
+ truncGT
+ truncGTIsoTruncGE
+ truncGTδLE
+ truncGTπ
+ truncLE
+ truncLEGE
+ truncLEIsoTruncLT
+ truncLEIsoTruncLT_hom_ι
+ truncLEIsoTruncLT_hom_ι_app
+ truncLEIsoTruncLT_inv_ι
+ truncLEIsoTruncLT_inv_ι_app
+ truncLEι
+ truncLTGE
+ truncLT_map_truncGE_map_truncLTι_app_fac
+ truncLT_map_truncLTι_app
+ truncLTι_comp_truncGEπ
+ truncLTι_comp_truncGEπ_app
+ zero₁
+ zero₂
+ zero₃
+ Ψ
+ Ψ_fromOpcycles
+ Ψ_opcyclesMap
+ Ψ_opcyclesMap_exact
+ δ
+ δFromOpcycles
+ δToCycles
+ δToCycles_cyclesIso_inv
+ δToCycles_iCycles
+ δToCycles_πE
+ δ_eq_zero_of_isIso₁
+ δ_eq_zero_of_isIso₂
+ δ_naturality
+ δ_pOpcycles
+ δ_toCycles
+ δ_δ
+ ιE
+ ιE_δFromOpcycles
+ πE
+ πE_EIsoH_hom
+ πE_EMap
+ πE_EToCycles
+ πE_d_ιE
+ πE_ιE
+ π_descTruncGE
+ π_descTruncGT
+ π_natTransTruncGEOfLE
+ π_natTransTruncGEOfLE_app
+ π_truncGTIsoTruncGE_hom
+ π_truncGTIsoTruncGE_hom_ι_app
+ π_truncGTIsoTruncGE_inv
+ π_truncGTIsoTruncGE_inv_ι_app
+ ω₁
+ ω₁δ
+ ω₁δ_naturality
++ Hom
++ instance (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) :
++ instance (X : C) (n : ℤ) [t.IsLE X n] (i : EInt) :
++ instance (a b : ℤ) (X : C) :
++ isIso_EMapFourδ₁Toδ₀'
++ isIso_EMapFourδ₄Toδ₃'
+++ instance (X : C) (a b : ℤ) :
+++ instance (X : C) (a b : ℤ) [t.IsGE X a] :
++++ instance :
- instance (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n := by
- instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1) := by
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for scripts/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
merge-conflict
…mit kernel fork (leanprover-community#33874) We make a few additions to the homology API, as it shall be necessary to formalize spectral sequences leanprover-community#33842. Let `S` be a short complex. The data of a kernel fork of `S.g` allows to compute `S.cycles`. Similarly, the data of a cokernel cofork of `S.f` allows to compute `S.opcycles`.
…ommunity#33437) The main definition in this file is `ComposableArrows.Exact.cokerIsoKer`: given an exact sequence `S` (involving at least four objects), this is the isomorphism from the cokernel of `S.map' k (k + 1)` to the kernel of `S.map' (k + 2) (k + 3)`. This will be used in the formalization of spectral sequences leanprover-community#33842.
…r arrows (leanprover-community#33881) This shall be used in the formalization of spectral sequences leanprover-community#33842.
…rs (leanprover-community#33887) A fully faithful triangulated functor preserves and reflects distinguished triangles. If the target category satisfies the octahedron axiom (i.e. the category is triangulated), then the source category also does. This is part of the formalization of spectral sequences leanprover-community#33842.
leanprover-community#33875) Let `S` be a short complex in an abelian category. If `K` is a kernel of `S.g` and `Q` a cokernel of `S.f`, and `K ⟶ H ⟶ Q` is an epi-mono factorization of `K ⟶ S.X₂ ⟶ Q`, then `H` identifies to the homology of `S`. (That shall be used when computing the homology of the differentials on pages of spectral sequences leanprover-community#33842.) In this PR, we also show that `ShortComplex C` is an abelian category if `C` is abelian.
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
leanprover-community#33875) Let `S` be a short complex in an abelian category. If `K` is a kernel of `S.g` and `Q` a cokernel of `S.f`, and `K ⟶ H ⟶ Q` is an epi-mono factorization of `K ⟶ S.X₂ ⟶ Q`, then `H` identifies to the homology of `S`. (That shall be used when computing the homology of the differentials on pages of spectral sequences leanprover-community#33842.) In this PR, we also show that `ShortComplex C` is an abelian category if `C` is abelian.
3 participants
This PR introduces spectral sequences. It contains two mostly independent developments:
Cequipped with a t-structure;After these additions, we have two ways to construct a spectral object in triangulated categories (the spectral object attached to a filtered complex, and the spectral object attached to a t-structure 1.). After applying a homological functor to these spectral objects, we obtain a spectral object in an abelian category, and the construction 2. allows to define spectral sequences.
In this PR, we do not study the stabilization and convergence of spectral sequences, which require more developments.
The mathematical material is discussed in https://hal.science/hal-04546712v5 (§5.4.1 and §5.4.4).
Cequipped with a t-structure;EIntthat use the octahedron axiom #35369truncLEandtruncGT#35364truncLTandtruncGEwhich use the octahedron axiom #35363truncLTandtruncGE#35362HasSpectralSequence#35374SpectralSequenceMkData#35372WithBotTopand the extended integers #33876Triangle#33886