feat/refactor: redefinition of homology + derived categories#25848
feat/refactor: redefinition of homology + derived categories#25848joelriou wants to merge 2224 commits intoleanprover-community:masterfrom
Conversation
joelriou
added
WIP
PR summary c70a3c4816Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.ObjectProperty.Retract | 421 | 733 | +312 (+74.11%) |
| Mathlib.CategoryTheory.Shift.SingleFunctors | 466 | 694 | +228 (+48.93%) |
| Mathlib.CategoryTheory.GradedObject | 467 | 645 | +178 (+38.12%) |
| Mathlib.CategoryTheory.GradedObject.Bifunctor | 468 | 646 | +178 (+38.03%) |
| Mathlib.Algebra.Homology.DerivedCategory.TStructure | 1330 | 1824 | +494 (+37.14%) |
| Mathlib.Algebra.Homology.LeftResolution.Basic | 937 | 1274 | +337 (+35.97%) |
| Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape | 628 | 837 | +209 (+33.28%) |
| Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition | 792 | 964 | +172 (+21.72%) |
| Mathlib.CategoryTheory.SmallObject.TransfiniteIteration | 797 | 969 | +172 (+21.58%) |
| Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim | 896 | 1066 | +170 (+18.97%) |
| Mathlib.Algebra.Homology.Factorizations.Basic | 827 | 978 | +151 (+18.26%) |
Import changes for all files
| Files | Import difference |
|---|---|
69 filesMathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.ExactSequenceFour Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.Basic Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence Mathlib.Algebra.Homology.ShortComplex.Homology Mathlib.Algebra.Homology.ShortComplex.LeftHomology Mathlib.Algebra.Homology.ShortComplex.Limits Mathlib.Algebra.Homology.ShortComplex.PreservesHomology Mathlib.Algebra.Homology.ShortComplex.QuasiIso Mathlib.Algebra.Homology.ShortComplex.Retract Mathlib.Algebra.Homology.ShortComplex.RightHomology Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.Square Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.EffectiveEpi Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.EffectiveEpi Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Small Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Tannaka |
1 |
58 filesMathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Module.PID Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicTopology.MooreComplex Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.Condensed.AB Mathlib.Condensed.Light.AB Mathlib.FieldTheory.Galois.NormalBasis Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Induced Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Regular.Category Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Sheaves.MayerVietoris |
2 |
25 filesMathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.Refinements Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives Mathlib.CategoryTheory.Shift.CommShiftTwo Mathlib.RepresentationTheory.Homological.Resolution |
3 |
56 filesMathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Homology.CochainComplexOpposite Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.ExtendHomotopy Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.TotalComplexShift Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Functor.Derived.Adjunction Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.Condensed.Light.InternallyProjective Mathlib.Condensed.Light.Monoidal Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro |
4 |
3 filesMathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.HomologySequenceLemmas |
5 |
9 filesMathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Localization Mathlib.CategoryTheory.FinCategory.AsType Mathlib.CategoryTheory.FinCategory.Basic |
6 |
3 filesMathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Sites.Etale |
8 |
Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.AlgebraicTopology.SimplexCategory.Defs |
10 |
8 filesMathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Preadditive.Indization |
11 |
71 filesMathlib.Algebra.Homology.ConcreteCategory Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.CategoryTheory.Category.Cat.Adjunction Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing |
13 |
8 filesMathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Equivalence Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison |
14 |
Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor |
15 |
26 filesMathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Instances Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Topology.Sheaves.CommRingCat |
16 |
3 filesMathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt |
17 |
3 filesMathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.Finite Mathlib.Algebra.Category.ModuleCat.Presheaf.Free |
18 |
Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.Subobject |
19 |
10 filesMathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Extend Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Extend Mathlib.CategoryTheory.ConnectedComponents Mathlib.CategoryTheory.IsConnected Mathlib.CategoryTheory.Sites.SheafCohomology.Basic |
20 |
13 filesMathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Linear Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.HomotopyCategory.Acyclic Mathlib.Algebra.Homology.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Presentable |
21 |
13 filesMathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear Mathlib.Algebra.Homology.DerivedCategory.Ext.Map Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.HomotopyCategory.KInjective Mathlib.Algebra.Homology.HomotopyCategory.KProjective Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Topology.Category.LightProfinite.Cartesian |
22 |
Mathlib.Algebra.Homology.DerivedCategory.Fractions |
23 |
4 filesMathlib.Algebra.Category.Ring.FinitePresentation Mathlib.CategoryTheory.Category.Preorder Mathlib.CategoryTheory.Functor.OfSequence Mathlib.CategoryTheory.Generator.Preadditive |
25 |
3 filesMathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Linear |
26 |
Mathlib.Algebra.Homology.Factorizations.CM5b Mathlib.Algebra.Homology.HomologySequence |
27 |
5 filesMathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison |
28 |
Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.Topology.CWComplex.Abstract.Basic |
29 |
14 filesMathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks |
30 |
27 filesMathlib.CategoryTheory.RegularCategory.Basic Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.Descent.IsStack Mathlib.CategoryTheory.Sites.Descent.Precoverage Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.Sites |
31 |
4 filesMathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.ObjectProperty.Equivalence Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Opposite.OpOp |
32 |
Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.CategoryTheory.Preadditive.CommGrp_ |
33 |
5 filesMathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated |
34 |
9 filesMathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.EssentiallyLarge Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.Presheaf Mathlib.CategoryTheory.Presentable.StrongGenerator |
35 |
Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject |
36 |
Mathlib.CategoryTheory.Triangulated.HomologicalFunctor |
37 |
Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory |
38 |
Mathlib.CategoryTheory.Triangulated.Orthogonal |
39 |
16 filesMathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism Mathlib.CategoryTheory.Category.Cat.Colimit |
40 |
Mathlib.CategoryTheory.Generator.Sheaf |
43 |
4 filesMathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.PreservesSheafification |
47 |
Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.Sites.Localization |
48 |
Mathlib.CategoryTheory.Category.ULift |
50 |
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems |
52 |
4 filesMathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Functor.KanExtension.Dense Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument |
53 |
8 filesMathlib.Algebra.Homology.ImageToKernel Mathlib.CategoryTheory.ExtremalEpi Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.StrongGenerator Mathlib.CategoryTheory.Generator.Type Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits |
54 |
7 filesMathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.Single |
55 |
Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ |
56 |
8 filesMathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.ColimitPresentation Mathlib.CategoryTheory.Presentable.Directed Mathlib.CategoryTheory.Presentable.Finite Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.Limits Mathlib.CategoryTheory.Presentable.Retracts Mathlib.CategoryTheory.Presentable.Type |
57 |
38 filesMathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HasFibers Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Join.Basic Mathlib.CategoryTheory.Join.Opposites Mathlib.CategoryTheory.Join.Sum Mathlib.CategoryTheory.Monoidal.Action.Basic Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Subobject.HasCardinalLT Mathlib.CategoryTheory.Sums.Products Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.Widget.StringDiagram |
58 |
Mathlib.Algebra.Homology.Double Mathlib.CategoryTheory.Generator.HomologicalComplex |
59 |
Mathlib.Algebra.Homology.HomologicalBicomplex |
60 |
18 filesMathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.CategoryTheory.Bicategory.EqToHom Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.Opposites Mathlib.CategoryTheory.Bicategory.Strict.Basic Mathlib.CategoryTheory.Bicategory.Strict Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.DinatTrans Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform Mathlib.CategoryTheory.ObjectProperty.Opposite Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic |
61 |
Mathlib.CategoryTheory.EssentialImage |
62 |
Mathlib.CategoryTheory.Subobject.FactorThru |
63 |
Mathlib.CategoryTheory.GradedObject.Braiding Mathlib.CategoryTheory.GradedObject.Monoidal |
65 |
Mathlib.CategoryTheory.Triangulated.Subcategory |
66 |
3 filesMathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure |
67 |
3 filesMathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite |
69 |
Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ |
76 |
Mathlib.Topology.Category.CompHausLike.Cartesian |
91 |
Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE |
92 |
Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms |
94 |
Mathlib.AlgebraicTopology.ModelCategory.Over Mathlib.CategoryTheory.Limits.MorphismProperty |
99 |
Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous |
102 |
Mathlib.CategoryTheory.Limits.Constructions.Over.Basic |
104 |
4 filesMathlib.Algebra.Homology.SpectralSequence.ComplexShape (new file) Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape |
105 |
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator |
106 |
Mathlib.CategoryTheory.Triangulated.SpectralObject |
109 |
3 filesMathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject |
117 |
Mathlib.CategoryTheory.Monoidal.Cartesian.Over |
121 |
Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Grp_ |
125 |
3 filesMathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ Mathlib.CategoryTheory.ObjectProperty.FiniteProducts |
128 |
11 filesMathlib.CategoryTheory.Filtered.FinallySmall Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Monoidal.Closed.Ideal Mathlib.CategoryTheory.Subfunctor.Subobject Mathlib.CategoryTheory.Topos.Classifier |
129 |
Mathlib.CategoryTheory.Subobject.Comma |
130 |
7 filesMathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.Sifted Mathlib.CategoryTheory.Monoidal.Closed.Types Mathlib.Order.Interval.Set.Final |
131 |
8 filesMathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism Mathlib.CategoryTheory.LocallyCartesianClosed.Over Mathlib.CategoryTheory.LocallyCartesianClosed.Sections Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Subobject.Presheaf Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Subobject.WellPowered |
132 |
Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic |
133 |
Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.CategoryTheory.Subterminal |
134 |
Mathlib.CategoryTheory.Monoidal.Closed.Zero |
135 |
29 filesMathlib.CategoryTheory.Bicategory.CatEnriched Mathlib.CategoryTheory.Category.Cat.CartesianClosed Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian Mathlib.CategoryTheory.Enriched.Basic Mathlib.CategoryTheory.Enriched.EnrichedCat Mathlib.CategoryTheory.Enriched.FunctorCategory Mathlib.CategoryTheory.Enriched.HomCongr Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal Mathlib.CategoryTheory.Enriched.Opposite Mathlib.CategoryTheory.Enriched.Ordinary.Basic Mathlib.CategoryTheory.Functor.FunctorHom Mathlib.CategoryTheory.Monoidal.Cartesian.Basic Mathlib.CategoryTheory.Monoidal.Cartesian.Cat Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_ Mathlib.CategoryTheory.Monoidal.Closed.Cartesian Mathlib.CategoryTheory.Monoidal.Closed.Enrichment Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes Mathlib.CategoryTheory.Monoidal.Closed.Functor Mathlib.CategoryTheory.Monoidal.Functor.Types Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Monoidal.Types.Coyoneda |
136 |
Mathlib.CategoryTheory.Localization.Bousfield |
140 |
3 filesMathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape Mathlib.CategoryTheory.ObjectProperty.Local |
141 |
Mathlib.Algebra.Homology.Factorizations.Basic |
151 |
Mathlib.Algebra.Category.ModuleCat.LeftResolution |
168 |
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim |
170 |
6 filesMathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration |
172 |
6 filesMathlib.CategoryTheory.GradedObject.Associator Mathlib.CategoryTheory.GradedObject.Bifunctor Mathlib.CategoryTheory.GradedObject.Single Mathlib.CategoryTheory.GradedObject.Trifunctor Mathlib.CategoryTheory.GradedObject.Unitor Mathlib.CategoryTheory.GradedObject |
178 |
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms |
204 |
5 filesMathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape Mathlib.CategoryTheory.SmallObject.Iteration.Basic Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty |
209 |
Mathlib.CategoryTheory.Shift.SingleFunctors |
228 |
Mathlib.CategoryTheory.Preadditive.Projective.Internal |
301 |
Mathlib.CategoryTheory.ObjectProperty.Retract |
312 |
3 filesMathlib.Algebra.Homology.LeftResolution.Reduced Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Ext |
335 |
Mathlib.Algebra.Homology.LeftResolution.Basic Mathlib.Algebra.Homology.LeftResolution.Transport |
337 |
Mathlib.CategoryTheory.Functor.Quadrifunctor (new file) |
363 |
Mathlib.CategoryTheory.Monoidal.Pentagon (new file) |
365 |
Mathlib.AlgebraicTopology.ModelCategory.Smith.SolutionSetCondition (new file) |
392 |
Mathlib.CategoryTheory.QuotientTwo (new file) |
398 |
Mathlib.CategoryTheory.QuotientThree (new file) |
403 |
Mathlib.CategoryTheory.Localization.OfQuotient (new file) |
416 |
Mathlib.CategoryTheory.Quotient.LocallySmall (new file) |
417 |
Mathlib.CategoryTheory.Comma.Extra (new file) |
418 |
Mathlib.CategoryTheory.Functor.KanExtension.Opposite (new file) |
437 |
Mathlib.CategoryTheory.ArrowTwo (new file) |
448 |
Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition (new file) |
450 |
Mathlib.CategoryTheory.Functor.Derived.LeftDerivedTwo (new file) |
451 |
3 filesMathlib.CategoryTheory.Functor.Derived.LeftDerivedFour (new file) Mathlib.CategoryTheory.Functor.Derived.LeftDerivedThree (new file) Mathlib.CategoryTheory.Functor.Derived.Opposite (new file) |
452 |
Mathlib.CategoryTheory.Functor.Derived.LeftDerivedBifunctorComp (new file) |
453 |
Mathlib.CategoryTheory.Functor.Derived.LeftDerivedTrifunctorComp (new file) |
454 |
Mathlib.CategoryTheory.Monoidal.Derived (new file) |
461 |
Mathlib.CategoryTheory.Shift.Prod (new file) |
479 |
Mathlib.CategoryTheory.Shift.CommShiftProd (new file) |
480 |
Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift (new file) |
486 |
Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure |
491 |
Mathlib.CategoryTheory.ConcreteCategory.Operation (new file) |
493 |
Mathlib.Algebra.Homology.DerivedCategory.TStructure |
494 |
Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrowsTwo (new file) |
505 |
Mathlib.CategoryTheory.JointlyReflect.Isomorphisms (new file) |
597 |
Mathlib.CategoryTheory.GuitartExact.HorizontalComposition (new file) Mathlib.CategoryTheory.GuitartExact.Quotient (new file) |
603 |
3 filesMathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences (new file) Mathlib.CategoryTheory.Localization.DerivabilityStructure.Product (new file) Mathlib.CategoryTheory.Localization.DerivabilityStructure.Quotient (new file) |
617 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Existence (new file) |
629 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Bifunctor (new file) |
632 |
Mathlib.AlgebraicTopology.ModelCategory.Transport (new file) |
635 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.DerivesTwo (new file) |
639 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.DerivesThree (new file) |
641 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.DerivesFour (new file) |
644 |
Mathlib.CategoryTheory.GradedObject.Colimits (new file) |
647 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Monoidal (new file) |
652 |
Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (new file) |
670 |
Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma (new file) |
671 |
Mathlib.CategoryTheory.ArrowThree (new file) |
684 |
Mathlib.CategoryTheory.ArrowFour (new file) |
685 |
Mathlib.CategoryTheory.ArrowFive (new file) |
686 |
Mathlib.CategoryTheory.ArrowSix (new file) |
687 |
Mathlib.CategoryTheory.ArrowSeven (new file) |
688 |
Mathlib.CategoryTheory.Shift.SingleFunctorsLift (new file) |
695 |
Mathlib.CategoryTheory.Localization.CalculusOfFractions.Lemmas (new file) |
700 |
Mathlib.CategoryTheory.Abelian.Constructor (new file) |
728 |
Mathlib.Algebra.Homology.ShortComplex.ShortComplexFour (new file) Mathlib.CategoryTheory.Functor.ReflectsExactSequences (new file) |
770 |
3 filesMathlib.Algebra.Homology.CategoryWithHomology (new file) Mathlib.Algebra.Homology.ShortComplex.Refinements (new file) Mathlib.Algebra.Homology.ShortComplex.ShortComplexFive (new file) |
771 |
Mathlib.Algebra.Homology.ShortComplex.FourLemma (new file) Mathlib.Algebra.Homology.ShortComplex.Images (new file) |
773 |
Mathlib.Algebra.Homology.ConnectShortExact (new file) |
774 |
Mathlib.Algebra.Homology.ShortComplex.FiveLemma (new file) |
775 |
Mathlib.Algebra.Homology.SpectralObject.Basic (new file) |
776 |
Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (new file) |
780 |
Mathlib.CategoryTheory.ObjectProperty.HomologicalComplex (new file) |
789 |
Mathlib.Algebra.Homology.Homology (new file) |
790 |
Mathlib.Algebra.Homology.HomologicalComplexFunctorEquiv (new file) |
794 |
Mathlib.CategoryTheory.ExactCategory.Basic (new file) |
796 |
Mathlib.CategoryTheory.ExactCategory.Abelian (new file) |
797 |
Mathlib.CategoryTheory.ExactCategory.Split (new file) |
798 |
Mathlib.CategoryTheory.ExactCategory.Q (new file) |
820 |
Mathlib.Algebra.Homology.SpectralObject.Cycles (new file) |
827 |
Mathlib.Algebra.Homology.SpectralObject.Page (new file) |
831 |
Mathlib.Algebra.Homology.SpectralObject.Differentials (new file) |
832 |
Mathlib.Algebra.Homology.SpectralObject.EpiMono (new file) |
834 |
Mathlib.Algebra.Homology.SpectralObject.Homology (new file) |
835 |
Mathlib.CategoryTheory.ExactCategory.GrothendieckGroup (new file) Mathlib.CategoryTheory.Monoidal.KFlat (new file) |
843 |
Mathlib.Algebra.Homology.SpectralSequence.Basic (new file) |
942 |
Mathlib.Algebra.Homology.SpectralSequence.EdgeStep (new file) |
943 |
Mathlib.Algebra.Homology.SpectralSequence.PageInfinity (new file) |
944 |
Mathlib.Algebra.Homology.SpectralSequence.Convergence (new file) |
949 |
Mathlib.Algebra.Homology.SpectralSequence.LowDegreesExactSequence (new file) |
955 |
Mathlib.Algebra.Homology.SpectralObject.SpectralSequence (new file) |
963 |
Mathlib.Algebra.Homology.SpectralObject.FirstPage (new file) |
964 |
Mathlib.CategoryTheory.MorphismProperty.TransfiniteCompositionCoproducts (new file) |
965 |
Mathlib.Algebra.Homology.DoubleHomology (new file) Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant (new file) |
967 |
Mathlib.Algebra.Homology.Embedding.ExtendMap (new file) |
968 |
Mathlib.Algebra.Homology.HomotopyFiber (new file) |
971 |
Mathlib.Algebra.Homology.Embedding.StupidFiltration (new file) Mathlib.Algebra.Homology.SpectralObject.PageInfinity (new file) |
972 |
Mathlib.Algebra.Homology.SpectralObject.Convergence (new file) |
973 |
Mathlib.Algebra.Homology.Embedding.ComplementaryTrunc (new file) |
990 |
Mathlib.Algebra.Homology.PreservesQuasiIso (new file) |
995 |
Mathlib.CategoryTheory.Sites.Balanced (new file) |
1020 |
Mathlib.CategoryTheory.Presentable.SmallObject (new file) |
1050 |
Mathlib.AlgebraicTopology.ModelCategory.Smith.Lemma18 (new file) |
1051 |
Mathlib.AlgebraicTopology.ModelCategory.Smith.Lemma19 (new file) |
1054 |
Mathlib.AlgebraicTopology.ModelCategory.Smith.Basic (new file) |
1062 |
Mathlib.CategoryTheory.Abelian.RefinementsExtra (new file) |
1073 |
Mathlib.CategoryTheory.Functor.Derived.RightDerivedTriangulated (new file) |
1095 |
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Triangulated (new file) |
1131 |
Mathlib.Algebra.Homology.BifunctorSingle (new file) |
1145 |
Mathlib.Algebra.Homology.BifunctorColimits (new file) |
1146 |
Mathlib.Algebra.Homology.TotalComplexMap (new file) |
1154 |
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (new file) |
1167 |
Mathlib.CategoryTheory.Triangulated.TStructure.Induced (new file) |
1168 |
Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (new file) Mathlib.CategoryTheory.Triangulated.TStructure.Heart (new file) |
1169 |
Mathlib.CategoryTheory.Triangulated.TStructure.Shift (new file) Mathlib.CategoryTheory.Triangulated.TStructure.TExact (new file) |
1170 |
Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (new file) |
1172 |
Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory (new file) |
1189 |
Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (new file) |
1192 |
Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (new file) |
1194 |
Mathlib.Algebra.Homology.HomotopyCategory.Monoidal (new file) |
1232 |
Mathlib.Algebra.Homology.BifunctorMappingCone (new file) |
1248 |
Mathlib.Algebra.Homology.BifunctorCommShift (new file) |
1256 |
Mathlib.Algebra.Homology.CochainComplexMinus (new file) Mathlib.Algebra.Homology.CochainComplexPlus (new file) |
1272 |
Mathlib.Algebra.Homology.ObjectProperty (new file) |
1273 |
Mathlib.Algebra.Homology.Embedding.CochainComplexTrunc (new file) |
1274 |
Mathlib.Algebra.Homology.BifunctorTriangulated (new file) Mathlib.CategoryTheory.Abelian.Flat.Basic (new file) |
1293 |
Mathlib.Algebra.Homology.BicomplexColumns (new file) |
1304 |
Mathlib.Algebra.Homology.BicomplexRows (new file) |
1305 |
Mathlib.Algebra.Homology.HomotopyCategory.MonoidalTriangulated (new file) |
1308 |
Mathlib.Algebra.Homology.LeftResolution.CochainComplexMinus (new file) |
1310 |
Mathlib.Algebra.Homology.HomotopyCategory.PreservesQuasiIso (new file) |
1327 |
Mathlib.Algebra.Homology.DerivedCategory.SpectralObject (new file) |
1332 |
Mathlib.Algebra.Homology.HomotopyCategory.Minus (new file) |
1347 |
Mathlib.Algebra.Homology.HomotopyCategory.Plus (new file) |
1348 |
Mathlib.Algebra.Homology.HomotopyCategory.Devissage (new file) |
1349 |
Mathlib.CategoryTheory.Abelian.YonedaExt (new file) |
1353 |
Mathlib.Algebra.Homology.LeftResolution.CochainComplex (new file) |
1374 |
Mathlib.Algebra.Homology.DerivedCategory.Monoidal (new file) |
1399 |
Mathlib.CategoryTheory.Abelian.Flat.KFlat (new file) |
1502 |
Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureKInjectives (new file) |
1520 |
Mathlib.Algebra.Homology.ShortComplex.ULift (new file) |
1627 |
Mathlib.CategoryTheory.Triangulated.TStructure.Homology (new file) |
1733 |
Mathlib.CategoryTheory.Triangulated.TStructure.RightTExact (new file) |
1734 |
Mathlib.Algebra.Homology.SpectralSequence.Examples.OfTStructure (new file) |
1780 |
Mathlib.Algebra.Homology.DerivedCategory.Minus (new file) Mathlib.Algebra.Homology.Factorizations.CM5a (new file) |
1835 |
Mathlib.Algebra.Homology.ModelCategory.Lifting (new file) |
1846 |
Mathlib.Algebra.Homology.DerivedCategory.Plus (new file) |
1847 |
Mathlib.Algebra.Homology.ModelCategory.Injective (new file) |
1853 |
Mathlib.Algebra.Homology.ModelCategory.Projective (new file) |
1857 |
Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureProjectives (new file) |
1894 |
Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives (new file) |
1902 |
Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus (new file) |
1909 |
Mathlib.Algebra.Homology.SpectralSequence.Examples.Grothendieck (new file) |
1931 |
Mathlib.CategoryTheory.Abelian.Flat.ModuleCat (new file) |
2177 |
Declarations diff
+ Acyclic.of_iso
+ AdmissibleEpi
+ AdmissibleEpi.mem
+ AdmissibleMono
+ AdmissibleMono.mem
+ Antitone.functor
+ Arrow₂
+ Arrow₃
+ Arrow₄
+ Arrow₅
+ Arrow₆
+ Arrow₇
+ B
+ Bifunctor
+ BinaryBicone.IsBilimit.op
+ BinaryBicone.op
+ BinaryBiproductData.op
+ Bounded
+ Bounded.ι
+ Category
+ CategoryTheory.Functor.map_quasiIsoAt_of_preservesHomology
+ CategoryTheory.Functor.map_quasiIso_of_preservesHomology
+ CategoryTheory.Functor.quasiIso_of_map_quasiIso_of_preservesHomology
+ CategoryTheory.asIso'
+ CategoryWithSmithStructure
+ ChainComplex.homology'SuccIso
+ ChainComplex.homology'ZeroIso
+ CochainComplex.homology'SuccIso
+ CochainComplex.homology'ZeroIso
+ CochainComplex.minus_cylinder
+ CochainComplex.plus_cylinder
+ CochainComplex.plus_pathObject
+ CofFibFactorization
+ CofFibFactorizationQuasiIsoLE
+ CohomologicalSpectralSequence
+ CohomologicalSpectralSequenceFin
+ CohomologicalSpectralSequenceNat
+ CollapsesAsSESAt
+ CollapsesAt
+ CompatiblePreserving.of_iso
+ CompatibleWithConvergenceStripes
+ ComplexShape.decidableRelSymm
+ ContainsHeart
+ ConvergenceStripes
+ ConvergesInDegree
+ CoreHasTotal
+ CoverPreserving.comp'
+ CoverPreserving.of_iso
+ DerivedMonoidal
+ DerivesMonoidalStructure
+ Derives₂
+ Derives₃
+ Derives₄
+ E
+ EIsoH
+ EIsoH_hom_naturality
+ EIsoH_hom_opcyclesIsoH_inv
+ EIsoPageInfinity
+ EMap
+ EMapFourδ₁Toδ₀'
+ EMapFourδ₁Toδ₀'_EMapFourδ₃Toδ₃'
+ EMapFourδ₁Toδ₀'_EObjIsoPageInfinity_hom
+ EMapFourδ₁Toδ₀'_comp
+ EMapFourδ₂Toδ₁'
+ EMapFourδ₄Toδ₃'
+ EMapFourδ₄Toδ₃'_EObjIsoPageInfinity_inv'
+ EMapFourδ₄Toδ₃'_comp
+ EMap_comp
+ EMap_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃
+ EMap_fourδ₁Toδ₀_d
+ EMap_id
+ EMap_ιE
+ EToCycles
+ EToCycles_i
+ Exact.cokerIsoKer
+ Exact.cokerIsoKer'
+ Exact.comp_desc
+ Exact.desc
+ Exact.isIso_cokerToKer
+ Exact.isIso_cokerToKer'
+ Exact.isIso_opcyclesToCycles
+ Exact.opcyclesIsoCycles
+ ExactCategory
+ E₂CohomologicalSpectralSequence
+ E₂CohomologicalSpectralSequenceFin
+ E₂CohomologicalSpectralSequenceNat
+ E₂HomologicalSpectralSequenceNat
+ E₂SpectralSequence
+ E₂SpectralSequenceNat
+ Factorization
+ Fan.congr_proj
+ Functor.HasDerivedMonoidalCategory
+ Functor.faithful_of_precomp_cancel_zero_essSurj
+ Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions
+ Functor.faithful_of_precomp_essSurj
+ Functor.faithful_of_precomp_of_hasLeftCalculusOfFractions
+ Functor.full_of_precomp_essSurj
+ Functor.isCocontinuous_comp
+ Functor.isCocontinuous_comp'
+ Functor.isCocontinuous_id
+ Functor.isCocontinuous_of_iso
+ Functor.isConnected_of_isConnected_costructuredArrow
+ Functor.isConnected_of_isConnected_of_essSurj
+ Functor.mapHomologicalComplexCompIso
+ Functor.mapHomotopyCategoryCompIso
+ Functor.postcompose₄
+ Functor.preimageHomotopy
+ GrothendieckGroup
+ GrothendieckTopology.CoversTop.jointlyReflectIsomorphisms
+ GuitartExact.prod
+ H_map_twoδ₂Toδ₁_toCycles
+ HasDesc
+ HasEdgeEpiAt
+ HasEdgeEpiAtFrom
+ HasEdgeEpiAtFrom.mk'
+ HasEdgeMonoAt
+ HasEdgeMonoAtFrom
+ HasEdgeMonoAtFrom.mk'
+ HasFirstPageComputation
+ HasFunctorialFactorization.of_le
+ HasFunctorialFlatResolution
+ HasFunctorialFlatResolution.mk
+ HasHeart
+ HasHomology₀
+ HasHomotopyFiber
+ HasInducedTStructure
+ HasInducedTStructure.mk'
+ HasKInjectiveResolutions
+ HasLeftDerivedFunctor₂
+ HasLeftDerivedFunctor₃
+ HasLeftDerivedFunctor₄
+ HasPageInfinityAt
+ HasPathObject
+ HasRightDerivedBifunctor
+ HasShift.prod
+ HasSpectralSequence
+ Heart
+ HoCat
+ HoCat.adj
+ HoCat.adjCounit'
+ HoCat.adjCounit'_app
+ HoCat.adjCounitIso
+ HoCat.adjCounitIso_inv_app
+ HoCat.adjUnit
+ HoCat.adjUnit_app
+ HoCat.bifibrantResolution
+ HoCat.bifibrantResolution'
+ HoCat.bifibrantResolution_map
+ HoCat.bifibrantResolution_obj
+ HoCat.homEquivLeft
+ HoCat.homEquivLeft_apply
+ HoCat.homEquivLeft_symm_apply
+ HoCat.homEquivRight
+ HoCat.homEquivRight_apply
+ HoCat.homEquivRight_symm_apply
+ HoCat.ιCofibrantObject
+ HoCat.ιCofibrantObject_map_toHoCat_map
+ HoCat.ιCofibrantObject_obj
+ HoCat.ιFibrantObject
+ HoCat.ιFibrantObject_map_toHoCat_map
+ HoCat.ιFibrantObject_obj
+ Hom.comp_eq
+ Hom.ext
+ Hom.ext'
+ Hom.isIso_τ_of_isIso_mapPageInfinity
+ Hom.isIso_τ_of_sub
+ Hom.isIso_τ_succ
+ Hom.isIso_φ_of_isIso_mapPageInfinity
+ Hom.isIso_φ_of_isIso_τ
+ Hom.mapShortComplex
+ Hom.mk'
+ Hom.mk'_surjective
+ HomFactorization
+ HomologicalComplex.preservesQuasiIso
+ HomologicalComplex.preservesQuasiIso.comp
+ HomotopyCategory.Plus.mk
+ HomotopyCategory.preservesQuasiIso
+ HomotopyEquiv.toQuasiIso
+ HomotopyEquiv.toQuasiIsoAt
+ ImagesLemmaInput
+ InjectiveObject
+ Int.antitone_neg
+ Int.opEquivalence
+ IsCofFibFactorization
+ IsColimit.ofIsZero
+ IsFirstQuadrant
+ IsInduced
+ IsInvertedBy.of_iso
+ IsIsoLE
+ IsKInjective.bijective_precomp
+ IsKInjective.eq_δ_of_cocycle
+ IsKInjective.eq_δ_of_cocycle'
+ IsKInjective.isIso_quotient_map_iff_quasiIso
+ IsKProjective.isIso_quotient_map_iff_quasiIso
+ IsLeftDerivabilityStructure.quotient
+ IsLeftDerivedFunctor₂
+ IsLeftDerivedFunctor₃
+ IsLeftDerivedFunctor₄
+ IsLeftLocalizing
+ IsLeftLocalizing.mk'
+ IsLimit.ofIsZero
+ IsLocalizedEquivalence.comp
+ IsLocalizedEquivalence.id
+ IsPointwiseRightKanExtension.compTwoSquare
+ IsPresentable.exists_cardinal
+ IsRightDerivedBifunctor
+ IsRightLocalizing
+ IsRightLocalizing.mk'
+ IsStableUnderColimitsOfShape.of_equivalence
+ IsStableUnderFiniteCoproducts.mk'
+ IsThirdQuadrant
+ IsZero.of_full_of_faithful_of_isZero
+ Iso.op_hom_inv_id_app
+ Iso.op_inv_hom_id_app
+ IteratedExtCategory
+ J
+ J_le
+ J_le_inter
+ J_le_llp_rlp
+ JointlyReflectEpimorphisms
+ JointlyReflectIsomorphisms
+ JointlyReflectMonomorphisms
+ L'
+ LE_of_hasEdgeEpiAtFrom
+ LE_of_hasEdgeMonoAtFrom
+ LE_rFromMin
+ LE_rMin
+ LE_rToMin
+ LeftExtension.isUniversalEquivOfIso₃
+ LeftExtension.isUniversalPostcompEquiv
+ LeftExtension.op
+ LeftExtension.postcomp₂
+ LeftExtension.unop
+ LeftHomotopyRel.iff_map_eq
+ LeftHomotopyRel.leftHomotopy
+ LeftResolution.prod
+ LeftTExact
+ LeftTExact.mk'
+ Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements
+ Minus.ι
+ ModelCategory.transport
+ ObjectProperty.essImage_ι
+ ObjectProperty.localizerMorphism
+ ObjectProperty.localizerMorphism.comp
+ Operation₀
+ Operation₁
+ Operation₂
+ Operation₃
+ Option.by_cases
+ Pentagon
+ Pi.congr_π
+ Plus.ι
+ PrecompLocalizerMorphismsInverts
+ Prod.eqToHom_fst
+ Prod.eqToHom_snd
+ ProjectiveObject
+ Q_map_triangle_distinguished
+ Qh_map_bijective_of_isKInjective
+ QuasiIsoLE
+ Quotient.functor_obj_shift
+ ReflectsExactSequences
+ ReflectsExactSequences.reflects
+ ReflectsExactSequences.reflectsShortComplexExact
+ Retract.injective
+ RightExtension.isUniversalEquivOfIso₃
+ RightExtension.op
+ RightExtension.unop
+ RightHomotopyRel.iff_map_eq
+ RightHomotopyRel.rightHomotopy
+ RightResolution.prod
+ RightTExact
+ RightTExact.mk'
+ Set.has_min_of_ℤ
+ ShortComplex.comp_homologyπ_eq_iff_up_to_refinements
+ ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements
+ ShortComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements
+ ShortComplex.epi_homologyMap_iff_up_to_refinements
+ ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements
+ ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements
+ ShortComplex.mono_homologyMap_iff_up_to_refinements
+ ShortComplexIso
+ ShortComplex₄
+ ShortComplex₅
+ SpectralObject
+ SpectralSequence
+ SpectralSequenceMkData
+ StationaryAt
+ StronglyConvergesTo
+ StronglyConvergesToInDegree
+ StructuredArrowRightwardsProdEquivalence
+ Subset
+ T
+ TExact
+ Triangle
+ VanishesOnGEOne
+ VanishesOnLESubOne
+ WKFlat
+ WL
+ XIsoOfEq_hom_comp_v
+ XIsoOfEq_inv_comp_v
+ YonedaExt'
+ Z
+ Z.X
+ Z.XIso
+ Z.d
+ ZToX₁
+ ZToX₁_f_0
+ ZToX₂
+ ZToX₂_f_self
+ ZXIso
+ ZXIso₂
+ Z_d_eq
+ Zero
+ _root_.AddEquiv.toIsoULift
+ _root_.CategoryTheory.Arrow₂.zero_of_arrow₂Iso
+ _root_.CategoryTheory.Functor.PreservesTotalComplex
+ _root_.CategoryTheory.Functor.mapArrow₃
+ _root_.CategoryTheory.Functor.mapArrow₅
+ _root_.CategoryTheory.Functor.mapArrow₆
+ _root_.CategoryTheory.Functor.mapArrow₇
+ _root_.CategoryTheory.Functor.quasiIsoAt_of_map_quasiIsoAt_of_preservesHomology
+ _root_.CategoryTheory.ObjectProperty.hom_zero
+ _root_.CategoryTheory.Retract.isZero
+ _root_.CategoryTheory.ShortComplex.ab_exact_iff_ulift
+ _root_.CategoryTheory.SpectralSequence.StronglyConvergesToInDegree.exists_isIso_aux
+ _root_.CategoryTheory.SpectralSequence.StronglyConvergesToInDegree.exists_isZero_aux
+ _root_.Fin.clamp_eq_last
+ _root_.Fin.clamp_le_clamp
+ _root_.ShortComplex.ab_exact_iff_of_addEquiv
+ _root_.ShortComplex.exact_and_epi_g_iff_of_addEquiv
+ _root_.ShortComplex.exact_and_mono_f_iff_of_addEquiv
+ abelian
+ abelianOfCategoryWithHomologyOfBalanced
+ abutment
+ abutmentFiltration
+ abutmentFiltrationFunctor
+ abutmentFiltrationMap
+ abutmentFiltrationMap_abutmentFiltrationToPageInfinity
+ abutmentFiltrationMap_ι
+ abutmentFiltrationShortComplex
+ abutmentFiltrationShortComplex_shortExact
+ abutmentFiltrationToPageInfinity
+ abutmentFiltrationToPageInfinity_EMapFourδ₂Toδ₁'
+ abutmentFiltrationι
+ abutmentFiltrationι_π
+ abutmentπ
+ abutmentπ_map
+ acyclic_X₁
+ acyclic_X₃
+ acyclic_truncGE_iff
+ acyclic_truncLE_iff
+ acyclic_ιTruncLE_iff_isSupportedOutside
+ addCommGroupCat_add
+ addCommGroupCat_add_assoc
+ addCommGroupCat_add_comm
+ addCommGroupCat_add_left_neg
+ addCommGroupCat_add_zero
+ addCommGroupCat_neg
+ addCommGroupCat_zero
+ addCommGroupCat_zero_add
+ addEquivFromHomology₀OfIsLE
+ addEquivFromHomology₀OfIsLE_naturality
+ addEquivToHomology₀OfIsGE
+ addEquivToHomology₀OfIsGE_naturality
+ addEquivULiftFunctorObj
+ add_apply
+ add_left_neg
+ add_liftCycles
+ add_zero
+ additive_iff_of_iso
+ additive_of_preserves_finite_products
+ additivity
+ admissibleMorphism
+ admissibleMorphism_heart
+ admissibleSplitEpi
+ admissibleSplitEpi_op
+ admissibleSplitEpi_quarrable
+ admissibleSplitEpi_stableUnderBaseChange
+ admissibleSplitEpi_stableUnderComposition
+ admissibleSplitEpi_unop
+ admissibleSplitMono
+ admissibleSplitMono_coquarrable
+ admissibleSplitMono_op
+ admissibleSplitMono_stableUnderCobaseChange
+ admissibleSplitMono_stableUnderComposition
+ admissibleSplitMono_unop
+ antitone_i₀'
+ arrowHomToG
+ arrowIsoDoubleD
+ arrowIsoMk
+ arrow₂
+ arrow₂IsoMk
+ assoc
+ associator_eq
+ associator_hom_app_app_app
+ associator_hom_fac_app_app_app
+ attachCells
+ attachCells'
+ attachCellsOfProp
+ bicomplexFunctor
+ bicomplexπ
+ biconeOfColimitCocone
+ biconeOfLimitCone
+ bifibrantResolutionMap
+ bifibrantResolutionMap_fac
+ bifibrantResolutionMap_fac'
+ bifibrantResolutionObj
+ bifibrantResolutionObj_hom_ext
+ bifunctorComp₁₂Counit
+ bifunctorComp₁₂Iso_hom_app_app_app
+ bifunctorComp₁₂Iso_inv_app_app_app
+ bifunctorComp₂₃Counit
+ bifunctorComp₂₃Iso_hom_app_app_app
+ bifunctorComp₂₃Iso_inv_app_app_app
+ bifunctorCounit₁
+ bifunctorCounit₁_app
+ bifunctorCounit₂
+ bifunctorCounit₂_app
+ bifunctorIso
+ bifunctorIso_hom_app_app
+ bifunctorIso_inv_app_app
+ bifunctorMapCochainComplex
+ bifunctorMapCochainComplexObjMapMappingConeTriangleIso
+ bifunctorMapHomologicalComplex
+ bifunctorMapHomotopyCategory
+ bijective_leftHomotopyClassToHom
+ bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom
+ bijective_rightHomotopyClassToHom
+ binaryBiproduct_shortExact
+ binaryCofanOfIsColimitCofanOption
+ boundaries
+ boundariesFunctor
+ boundariesIsoImage
+ boundariesMap
+ boundariesToCycles'
+ boundariesToCycles'NatTrans
+ boundariesToCycles'_naturality
+ boundaries_eq_bot
+ boundaries_eq_imageSubobject
+ boundaries_le_cycles'
+ c
+ case₁
+ case₁'
+ case₂
+ case₂'
+ category
+ cc
+ ccSc
+ ccSc_exact
+ cc_w
+ chgObj
+ chgObjEquivalence
+ closedUnderColimitsOfShape_flat
+ closedUnderColimitsOfShape_kFlat
+ closedUnderLimitsOfShape_discrete_flat
+ closedUnderLimitsOfShape_discrete_kFlat
+ cm5a
+ cm5a_cof
+ cochainComplexFunctor
+ cochainComplexMinus
+ cochainComplexMinus_flat_le_kFlat
+ cochainComplexNatTransπ
+ cochainComplexXNegOneIso
+ cochainComplexXZeroIso
+ cochainComplex_d_neg_one_zero
+ cochainComplex_kFlat_isLeftDerivabilityStructure
+ cochainComplexπ
+ cochainComplexπ_f_0
+ cochain₀
+ cochain₁
+ cocone
+ coconeAtIso
+ coconeStupidFiltrationGE
+ cocone_heart_isGE_neg_one
+ cocone_heart_isLE_zero
+ cocycle₁
+ cocycle₁'
+ coe_cocycle₁'_v_comp_eq_zero
+ cofFibFactorization
+ cofan
+ cofanOfIsZero
+ cofanOfIsZeroButOne
+ cofanOfIsZeroButOne_ι_self
+ cofanOfIsZero_inj
+ cofanSingleColumnObjTotal
+ cofanSingleRowObjTotal
+ cofibrantObjectEquivalence
+ cofibrantObjectLocalizerMorphism
+ cofibrations_eq
+ cohomologicalStripes
+ cohomomologicalStripesFin
+ cokerToKer
+ cokerToKer'
+ cokerToKer'_fac
+ cokerToKer_fac
+ cokernelIsoCycles
+ cokernelIsoCycles_hom_fac
+ cokernelSequenceCycles
+ cokernelSequenceCyclesE
+ cokernelSequenceCyclesEIso
+ cokernelSequenceCyclesE_exact
+ cokernelSequenceCycles_exact
+ cokernelSequenceE
+ cokernelSequenceE_exact
+ cokernelSequenceOpcycles
+ cokernelSequenceOpcyclesE
+ cokernelSequenceOpcyclesE_exact
+ cokernelSequenceOpcycles_exact
+ colimitCocone
+ colimitOfShapeFlatResolutionFunctorObj
+ colimitOfShapeResolutionFunctorObj
+ collapsesAsSESAt_of_succ
+ columnFunctor
+ commShift
+ commShiftIso_id_hom_app
+ commShiftIso_id_inv_app
+ commShiftOfFac
+ commShiftOfFac_aux
+ commShiftUncurry
+ commShift_curry_flip_obj_hom_app
+ commShift_curry_obj_hom_app
+ commShift_op_hom_app
+ commShift₂Curry
+ comp
+ compK
+ compKX
+ compKXIso
+ compKXIso'
+ compKd
+ compKd_comp_d'
+ compKd_eq_d
+ compKd_eq_d'
+ compKd_eq_d'_comp_d
+ compKd_shape
+ compShortComplex₄
+ compShortComplex₄Iso
+ compShortComplex₄_exact
+ compTwoSquare
+ compZToShiftZ
+ compZToShiftZ_comp_ZToZ₂
+ compZToShiftZf
+ compZToShiftZf_eq
+ compZToZ
+ compZToZ_comp_ZToX₁
+ compZToZf
+ compZToZf_eq
+ compZToZf_eq'
+ compZToZf_eq_zero_of_le
+ compZ_comm
+ compZ_comm'
+ comp_K_d_eq_d
+ comp_K_d_eq_d'
+ comp_K_d_eq_d'_comp_d
+ comp_assoc_of_third_degree_eq_neg_second_degree
+ comp_coe_cocycle₁_comp
+ comp_coe_cocyle₁'_v_eq_zero
+ comp_commShiftIso_hom
+ comp_homologyδ
+ comp_homologyδOfDistinguished
+ comp_homologyπ_eq_zero_iff_up_to_refinements
+ comp_natTransOfIsRightDerivedFunctorComp_app
+ comp_pOpcycles_eq_zero_iff_up_to_refinements
+ comp_rightDerivedδ
+ comp_π
+ comp_π''
+ comp_τ₇
+ compatibility
+ composableArrows
+ composableArrows_exact
+ composableArrows₀Equivalence
+ composableArrows₁Equivalence
+ composableArrows₅
+ composableArrows₅_exact
+ condition
+ cone
+ congr_map_conjugate
+ connect
+ connectShortComplex
+ connectShortComplex_exact
+ connectShortComplex_exact'
+ connectShortComplexι
+ connectShortComplexπ
+ connect_exact
+ convergesAt
+ coproductTriangle
+ coproductTriangle_distinguished
+ coquarrable
+ coquarrable.hasPushout
+ coquarrable.hasPushout'
+ coquarrable.op
+ coquarrable.unop
+ coreHasTotalOfIsStrictlyLE
+ costructuredArrowCostructuredArrowPreEquivalence
+ costructuredArrowRightWards_final_iff_of_iso
+ costructuredArrowRightwardsComp
+ counit
+ counit₁₂
+ counit₁₂_app
+ counit₂₃
+ counit₂₃_app
+ curry
+ curryObjUncurryObjIso
+ currying₄
+ currying₄_unitIso_hom_app_app_app_app_app
+ currying₄_unitIso_inv_app_app_app_app_app
+ curry₄
+ curry₄_map_app_app_app_app
+ curry₄_obj_map_app_app_app
+ curry₄_obj_obj_map_app_app
+ curry₄_obj_obj_obj_map_app
+ curry₄_obj_obj_obj_obj_map
+ cycles
+ cycles'
+ cycles'Functor
+ cycles'IsoKernel
+ cycles'Map
+ cycles'Map_arrow
+ cycles'Map_comp
+ cycles'Map_id
+ cycles'_eq_kernelSubobject
+ cyclesIso
+ cyclesIsoH
+ cyclesIsoH_hom_EIsoH_inv
+ cyclesIsoH_hom_inv_id
+ cyclesIsoH_inv
+ cyclesIsoH_inv_hom_id
+ cyclesIsoSc'_eq_rfl
+ cyclesIso_hom_i
+ cyclesIso_inv_cyclesMap
+ cyclesIso_inv_i
+ cyclesMap
+ cyclesMap_comp
+ cyclesMap_i
+ cyclesMap_id
+ cyclesMap_Ψ
+ cyclesMap_Ψ_exact
+ cycles_eq_top
+ d
+ dCokernelSequence
+ dCokernelSequence_exact
+ dHomologyData
+ dHomologyIso
+ dKernelSequence
+ dKernelSequence_exact
+ dNatTrans
+ dShortComplex
+ d_EIsoH_hom
+ d_EMap_fourδ₄Toδ₃
+ d_comp_edgeEpiStep
+ d_d
+ d_eq_zero_of_hasEdgeEpiAt
+ d_eq_zero_of_hasEdgeMonoAt
+ d_from_eq_zero
+ d_to_eq_zero
+ d_ιE_fromOpcycles
+ deg_position
+ degreewiseEpiWithInjectiveKernel.epi
+ degreewiseEpiWithInjectiveKernel_iff_of_isZero
+ degreewiseEpiWithInjectiveKernel_p
+ degreewiseMonoWithProjectiveCokernel
+ degreewiseMonoWithProjectiveCokernel_eq_unop
+ degreewiseMonoWithProjectiveCokernel_iff_of_isZero
+ degreewiseMonoWithProjectiveKernel.mono
+ derives₂_iff
+ descCycles
+ descE
+ descExtend
+ descExtend_f
+ descExtend_homRestrict'
+ descExtendfArrowIso
+ descOpcycles
+ descTruncGE
+ descTruncGE_aux
+ descTruncGT
+ descTruncGT_aux
+ diagramFunctor
+ direct_factor
+ distinguished_iff_op
+ doubleFunctor
+ doubleFunctorCompMapHomologicalComplex
+ d₂
+ d₂Sequence
+ d₂Sequence_exact
+ d₂_fromE₂TwoZero
+ 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
+ edgeEpi
+ edgeEpiStep
+ edgeEpiStepShortComplex
+ edgeEpiStepShortComplex_exact
+ edgeEpiStep_comp_iso_inv
+ edgeEpiStep_edgeMonoStep
+ edgeEpiStep_pageInfinityIso_inv
+ edgeEpiStep_pageInfinityIso_inv'
+ edgeEpiStep_ιE₃TwoZero
+ edgeEpiSteps
+ edgeEpiSteps'
+ edgeEpiSteps'_succ
+ edgeEpiSteps'_zero
+ edgeEpiSteps_comp
+ edgeEpiSteps_edgeEpi
+ edgeEpiSteps_edgeMonoSteps
+ edgeEpiSteps_eq
+ edgeEpiSteps_eq_edgeEpiStep
+ edgeEpiSteps_eq_edgeEpiSteps'
+ edgeEpiSteps_eq_edgeEpiSteps_comp_edgeEpiStep
+ edgeEpiSteps_eq_edgeEpiSteps_comp_pageXIsoOfEq_hom
+ edgeEpiSteps_eq_id
+ edgeEpiSteps_eq_of_eq
+ edgeEpiSteps_pageInfinityIso_inv
+ edgeEpiSteps_pageInfinityIso_inv'
+ edgeEpi_eq_pageInfinityIso_inv
+ edgeIsoSteps
+ edgeMono
+ edgeMonoStep
+ edgeMonoStepShortComplex
+ edgeMonoStepShortComplex_exact
+ edgeMonoStep_comp_d
+ edgeMonoStep_edgeEpiStep
+ edgeMonoStep_naturality
+ edgeMonoStep_pageInfinityIso_inv
+ edgeMonoSteps
+ edgeMonoSteps'
+ edgeMonoSteps'_succ
+ edgeMonoSteps'_zero
+ edgeMonoSteps_comp
+ edgeMonoSteps_edgeEpiSteps
+ edgeMonoSteps_eq
+ edgeMonoSteps_eq_edgeMonoStep
+ edgeMonoSteps_eq_edgeMonoStep_comp_edgeMonoSteps
+ edgeMonoSteps_eq_edgeMonoSteps'
+ edgeMonoSteps_eq_id
+ edgeMonoSteps_eq_of_eq
+ edgeMonoSteps_eq_pageXIsoOfEq_inv_comp_edgeMonoSteps
+ edgeMonoSteps_naturality
+ edgeMonoSteps_pageInfinityIso_inv
+ edgeMono_edgeMonoSteps
+ edgeMono_eq_pageInfinityIso_hom
+ effectiveEpiStructOfEpiOfIsPushout
+ effective_epi_of_epi
+ embeddingUpIntGE_monotone
+ epi
+ epiWithInjectiveKernel.hasLiftingProperty
+ epiWithInjectiveKernel_iff_of_isZero
+ epi_EMap
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ epi_cokerToKer'
+ epi_d
+ epi_descExtend_f_iff
+ epi_homologyFunctor_map_mor₂
+ epi_homologyMap_iff'
+ epi_homologyMap_iff_up_to_refinements
+ epi_homologyMap_p
+ epi_homologyMap_τ₁
+ epi_homologyMap_τ₂
+ epi_homologyMap₀_doubleFunctor_map_arrowHomToG_iff
+ epi_iff
+ epi_iff_epi_yoneda_map
+ epi_iff_isLocallySurjective
+ epi_iff_isLocallySurjective_yoneda_map
+ epi_iff_of_addEquiv
+ epi_iff_ulift
+ epi_of_isZero_cokernel
+ epi_of_isZero_cokernel'
+ epi_πQ
+ epimorphisms_stableUnderBaseChange
+ eq_add_ofNat_of_le
+ eq_zero_of_map_eq_zero
+ essImage_singleFunctor_eq_heart
+ essImage_ι_comp
+ essSurj_mapComposableArrows_two
+ evalJointlyReflectsColimits
+ evaluationIso
+ exactFunctor.preservesFiniteColimits
+ exactFunctor.preservesFiniteLimits
+ exactFunctor_iff_preservesQuasiIso
+ exact_and_epi_g_iff
+ exact_and_epi_g_iff_preadditiveYoneda
+ exact_and_mono_f_iff
+ exact_and_mono_f_iff_preadditiveCoyoneda
+ exact_iff
+ exact_iff_of_iso
+ exact_of_arrow₂Iso
+ exact_shortComplex_of_isLimit
+ exact₁
+ exact₁₂₃₄
+ exact₂
+ exact₂₃₄₅
+ exact₃
+ exists_bifibrant
+ exists_bifibrant_map
+ exists_distTriang_of_shortExact
+ exists_distinguished_triangle_of_epi
+ exists_distinguished_triangle_of_isLE_zero_of_isGE_neg_one
+ exists_fac
+ exists_hom
+ exists_index
+ exists_injective_resolution'
+ exists_isIso
+ exists_isZero
+ exists_iso_single
+ exists_lift
+ exists_of_essSurj
+ exists_sub_eq
+ exists_sub_le
+ extend_comp_homRestrict'
+ fAdmissible
+ fAdmissible_eq_monomorphisms
+ fAdmissible_iff_mono
+ fAdmissible_respectsIso
+ fMor
+ f_index
+ f_α
+ f_α_f
+ fac_left
+ fac_of_isLeftLocalizing
+ fac_of_isLeftLocalizing'
+ fac_of_isRightLocalizing
+ fac_of_isRightLocalizing'
+ fac_right
+ factorization
+ factorizationM_ι_inr
+ faithful_of_isRightLocalizing
+ fanOfEquiv
+ fanOfEquiv_proj
+ fibrantObjectEquivalence
+ fibrantObjectLocalizerMorphism
+ fibrations_eq
+ filtration
+ filtrationLE
+ filtrationLECocone
+ filtrationLEFunctor
+ filtrationLEFunctorCompColimIso
+ filtrationLEMinus
+ filtrationLEMinusCompιIso
+ filtrationLEMinusFunctor
+ filtrationLEMinusFunctorCompWhiskeringRightObjιIso
+ filtration_map_ι
+ filtrationι
+ filtrationι_pageInfinityπ
+ five_lemma
+ flat
+ four_lemma_epi
+ four_lemma_mono
+ free_shortExact_finrank_add'
+ fromE₂TwoZero
+ fromHomology₀
+ fromHomology₀_naturality
+ fromNext
+ fromOfShortComplex
+ fromOpcycles
+ fromOpcycles_H_map_twoδ₁Toδ₀
+ fromOpcyles_δ
+ fromSingleEquiv
+ from_truncGE_obj_ext
+ fst
+ full_of_isRightLocalizing
+ fullyFaithfulUncurry₄
+ functorArrow
+ functorConcat
+ functorConcat₃
+ functorEmptyLimitCone
+ functorEquivalence
+ functorEquivalenceInverseCompMapHomologicalComplexColim
+ functorObj
+ functorOperation_add_zero'
+ functorOperation_assoc'
+ functorOperation_zero_add'
+ functorOperation₀
+ functorOperation₀.equiv_of_iso
+ functorOperation₀.of_iso
+ functorOperation₁
+ functorOperation₁.equiv_of_iso
+ functorOperation₁.of_iso
+ functorOperation₂
+ functorOperation₂.add_left_neg
+ functorOperation₂.add_left_neg.of_iso
+ functorOperation₂.add_zero
+ functorOperation₂.add_zero.of_iso
+ functorOperation₂.assoc
+ functorOperation₂.assoc.of_iso
+ functorOperation₂.comm
+ functorOperation₂.comm.of_iso
+ functorOperation₂.equiv_of_iso
+ functorOperation₂.of_iso
+ functorOperation₂.swap
+ functorOperation₂.zero_add
+ functorOperation₂.zero_add.of_iso
+ functorOperation₃
+ functorOperation₃.equiv_of_iso
+ functorOperation₃.of_iso
+ functorPr₀
+ functorPr₁
+ functorPr₂
+ functorPr₃₁
+ functorPr₃₂
+ functorPr₃₃
+ functorPullback_eq_of_iso
+ functorPushforward_eq_of_iso
+ functor_additive_iff'
+ functor_from_isTriangulated_iff
+ functor_obj_surjective
+ functor₁
+ functor₂
+ functor₃
+ functor₄
+ functor₅
+ gAdmissible
+ gAdmissible_eq_epimorphisms
+ gAdmissible_iff_epi
+ gAdmissible_respectsIso
+ gMor
+ gradedHomology'Functor
+ grothendieckSpectralSequence
+ hComp
+ hComp'
+ hK'
+ hMor
+ hasCokernel
+ hasCokernel_of_admissibleMorphism
+ hasCokernels
+ hasCoproduct
+ hasCoproduct_of_direct_factor
+ hasCoproduct_of_isZero
+ hasCoproduct_of_isZero_but_one
+ hasCoproductsOfShape_index
+ hasDerivedMonoidalCategory
+ hasEdgeEpiAt
+ hasEdgeEpiAtFrom
+ hasEdgeEpiAtFrom_of_GE
+ hasEdgeEpiAt_of_rFromMin_LE
+ hasEdgeEpiSet
+ hasEdgeMonoAt
+ hasEdgeMonoAtFrom
+ hasEdgeMonoAtFrom_of_GE
+ hasEdgeMonoAt_of_rToMin_LE
+ hasEdgeMonoSet
+ hasHeartFullSubcategory
+ hasHomology₀
+ hasKernel
+ hasKernel_of_admissibleMorphism
+ hasKernels
+ hasLeftDerivedFunctor
+ hasLeftDerivedFunctor_iff_op
+ hasLeftDerivedFunctor_of_inverts
+ hasLeftDerivedFunctor₂
+ hasLeftDerivedFunctor₃
+ hasLeftDerivedFunctor₄
+ hasLeftResolutions_arrow
+ hasLeftResolutions_arrow_of_functorial_resolutions
+ hasLift
+ hasLiftingProperty_iff_of_isEquivalence
+ hasPageInfinityAt
+ hasPageInfinityAt_of_convergesInDegree
+ hasPointwiseRightDerivedFunctor
+ hasPointwiseRightKanExtension
+ hasPointwiseRightKanExtensionAt_iff
+ hasPointwiseRightKanExtension_iff
+ hasProductOfEquiv
+ hasRightDerivedBifunctor_of_precompLocalizerMorphismsInverts
+ hasRightDerivedFunctor
+ hasRightDerivedFunctor_iff_op
+ hasRightDerivedFunctor_of_inverts
+ hasRightDerivedFunctor₁_of_precompLocalizerMorphismsInverts
+ hasRightDerivedFunctor₂_of_precompLocalizerMorphismsInverts
+ hasRightKanExtension
+ hasRightResolutions_of_arrow
+ hasShift
+ hasTotalOfPreserves
+ hasTotal_of_isStrictlyGE_of_isStrictlyLE
+ hasTotal_of_isStrictlyLE
+ hasTotal_of_retract
+ hasZeroObject
+ heart
+ heartEquivalenceFullsubcategory
+ heartMk
+ heartShortExactTriangle
+ heartShortExactTriangle_distinguished
+ heartShortExactδ
+ heartShortExactδ_unique
+ hom'
+ homEquiv'
+ homOfLE'
+ homRel
+ homRel_iff_leftHomotopyRel
+ homRel_iff_rightHomotopyRel
+ homRestrict'
+ homRestrict'_descExtend
+ homRestrict'_f
+ homRestrict'_hasDesc
+ homRestrict'_postcomp
+ hom_ι
+ homologicalComplex
+ homologicalComplex_iff
+ homologicalStripesNat
+ homology
+ homology'
+ homology'Functor
+ homology'Iso
+ homologyCompιHeartIso
+ homologyData
+ homologyDataEIdId
+ homologyFunctorIsotruncLE₀GE₀ToHeart
+ homologyIsoSc'_eq_rfl
+ homologyMapArrowIso
+ homologyMap_comp₁₂_eq_zero_of_distinguished
+ homologyMap_eq_zero_of_Q_map_eq_zero
+ homologyMap_fst_comp
+ homologyMap_shift
+ homologyRightTExact
+ homologyRightTExact_comp_δ
+ homologyRightTExact_exact₁
+ homologyRightTExact_exact₂
+ homologyRightTExact_exact₃
+ homologyRightTExactδ
+ homologyRightTExactδ_comp
+ homologyRightTExact₀_map_exact
+ homologySequence_isIso_shift_map_mor₁_iff
+ homologySequence_isIso_shift_map_mor₂_iff
+ homologyShortComplex
+ homologyShortComplex'
+ homologyShortComplex''
+ homologyShortComplex''_exact
+ homologyShortComplex'_exact
+ homologyShortComplex_exact
+ homology_comp_δ
+ homology_exact₁_of_distinguished
+ homology_exact₂_of_distinguished
+ homology_exact₃_of_distinguished
+ homology_δ
+ homology_δ_comp
+ homologyδ
+ homologyδOfDistinguished
+ homologyδOfDistinguished_comp
+ homologyδ_comp
+ homology₀
+ homology₀ιHeart
+ homotopyCategory_kFlat_isLeftDerivabilityStructure
+ homotopyEquiv
+ homotopyFiber
+ homotopy₀₁
+ iBifibrantResolutionObj
+ iCycles
+ iCycles_δ
+ i_π
+ id
+ id_prod_kFlat_derives_curriedTensor
+ id_τ₇
+ image.lift
+ image.lift_ι
+ imageToKernel_as_boundariesToCycles'
+ image_preimageNatTrans
+ index
+ induced
+ induced_compatibility
+ induction_Q_obj
+ injectiveResolution
+ injective_of_isZero
+ injective_φ
+ inl
+ inlX_XIsoBiprod_hom
+ inlX_mapHomologicalComplexObjXIso_inv
+ inl_XIsoBiprod_inv
+ inl_fst
+ inl_snd
+ inrCompHomotopy
+ inrX_XIsoBiprod_hom
+ inrX_mapHomologicalComplexObjXIso_inv
+ inr_XIsoBiprod_inv
+ inr_fst
+ inr_mapHomologicalComplexObjIso_hom
+ inr_snd
+ instMonoidalCategory
+ instance (E : SpectralObject C EInt) : E.HasSpectralSequence mkDataE₂Cohomological
+ instance (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated] [F.Full] :
+ instance (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) [F.Faithful] :
+ instance (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) [F.Faithful] [F.Full] :
+ instance (F : V ⥤ W) [F.Additive] [F.Full] [F.Faithful] : (F.mapHomotopyCategory c).Full
+ instance (G : D ⥤ H) : (L ⋙ G).HasLeftDerivedFunctor W
+ instance (G : D ⥤ H) : (L ⋙ G).HasRightDerivedFunctor W
+ instance (K : CochainComplex A ℤ) (i : ℤ) [K.IsStrictlyLE i]
+ instance (K : CochainComplex A ℤ) : QuasiIso ((Λ.kFlatResolutionNatTrans hι).app K) := by
+ instance (K : CochainComplex C ℤ) (i : ℤ) :
+ instance (K : CochainComplex C ℤ) (i : ℤ) [K.IsStrictlyLE i] :
+ instance (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyGE n] :
+ instance (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] :
+ instance (K : CochainComplex C ℤ) (y : ℤ) :
+ instance (K : CochainComplex C ℤ) [K.IsKInjective] :
+ instance (K : CochainComplex.Minus (ProjectiveObject C)) :
+ instance (K : CofibrantObject (Minus C)) (n : ℤ) :
+ instance (K : DerivedCategory.Plus C) (n : ℤ) [t.IsGE K n] :
+ instance (K : FibrantObject (Plus C)) (n : ℤ) :
+ instance (K : HomologicalComplex₂ C (up ℤ) c) (n : ℤ) :
+ instance (K : HomologicalComplex₂ C (up ℤ) c) (n x : ℤ) [CochainComplex.IsStrictlyLE K x] :
+ instance (K : HomotopyCategory.Plus C) [(∀ (n : ℤ), Injective (K.obj.as.X n))] :
+ instance (K : Minus (ProjectiveObject C)) (n : ℤ) :
+ instance (K : Minus A) :
+ instance (K : Plus (InjectiveObject C)) (n : ℤ) :
+ instance (K L : CochainComplex C ℤ) [hK : K.IsKInjective] [hL : L.IsKInjective] :
+ instance (K₁ : CochainComplex C₁ ℤ) :
+ instance (K₁ : HomologicalComplex C₁ c₁) :
+ instance (K₁ : HomologicalComplex C₁ c₁) [HasColimitsOfShape B C₂]
+ instance (K₁ : HomotopyCategory C₁ (.up ℤ)) :
+ instance (K₁ : HomotopyCategory C₁ (.up ℤ)) [HasZeroObject C₂] [HasBinaryBiproducts C₂] :
+ instance (K₂ : CochainComplex C₂ ℤ) :
+ instance (K₂ : HomologicalComplex C₂ c₂) :
+ instance (K₂ : HomologicalComplex C₂ c₂) [HasColimitsOfShape B C₁]
+ instance (K₂ : HomotopyCategory C₂ (.up ℤ)) :
+ instance (K₂ : HomotopyCategory C₂ (.up ℤ)) [HasZeroObject C₁] [HasBinaryBiproducts C₁] :
+ instance (L : CochainComplex C ℤ) (i₂ : ℤ) :
+ instance (M : ModuleCat.{u} R) : ((curriedTensor _).flip.obj M).IsLeftAdjoint
+ instance (M : ModuleCat.{u} R) : ((curriedTensor _).obj M).IsLeftAdjoint
+ instance (M : ModuleCat.{u} R) : (tensorRight M).IsLeftAdjoint
+ instance (P : ObjectProperty C) [P.IsTriangulated] : P.op.IsTriangulated
+ instance (P : ObjectProperty Cᵒᵖ) [P.IsTriangulated] : P.unop.IsTriangulated
+ instance (P P' : ObjectProperty C) [P.IsTriangulated] [P'.IsTriangulated] (t : TStructure C)
+ instance (P' : ObjectProperty C) [P.IsTriangulatedClosed₂] [P.IsClosedUnderIsomorphisms]
+ instance (P' : ObjectProperty C) [P.IsTriangulated] [P.IsClosedUnderIsomorphisms]
+ instance (W : MorphismProperty C) [MorphismProperty.IsSmall.{w} W] :
+ instance (X : BifibrantObject C) :
+ instance (X : BifibrantObject C) : IsCofibrant (ιFibrantObject.obj X).obj := X.property.1
+ instance (X : BifibrantObject C) : IsFibrant (ιCofibrantObject.obj X).obj := X.property.2
+ instance (X : BifibrantObject.HoCat C) : IsIso (HoCat.adjCounit'.app X) := by
+ 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) (i : ℤ) : IsIso (singleShiftIso_hom_app n a a' ha' X i) := 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 0] : t.IsGE (X⟦-n⟧) n
+ instance (X : C) (n : ℤ) [t.IsGE X 0] : t.IsGE (X⟦n⟧) (-n)
+ instance (X : C) (n : ℤ) [t.IsGE X n] : IsIso ((t.truncGEπ n).app X) := by
+ instance (X : C) (n : ℤ) [t.IsGE X n] : t.IsGE (X⟦n⟧) 0
+ instance (X : C) (n : ℤ) [t.IsLE X 0] : t.IsLE (X⟦-n⟧) n
+ instance (X : C) (n : ℤ) [t.IsLE X 0] : t.IsLE (X⟦n⟧) (-n)
+ instance (X : C) (n : ℤ) [t.IsLE X n] : IsIso ((t.truncLEι n).app X) := by
+ instance (X : C) (n : ℤ) [t.IsLE X n] : t.IsLE (X⟦(1 : ℤ)⟧) n
+ instance (X : C) (n : ℤ) [t.IsLE X n] : t.IsLE (X⟦n⟧) 0
+ instance (X : C) : ((curriedTensor C).obj X).Additive
+ instance (X : C) : AdmissibleEpi (0 : X ⟶ 0) := by
+ instance (X : C) : AdmissibleMono (0 : 0 ⟶ X) := by
+ instance (X : C) : IsIso (t.homology₀.map ((truncGEπ t 0).app X)) := by
+ instance (X : C) : IsIso (t.homology₀.map ((truncLEι t 0).app X)) := by
+ instance (X : C) : t.IsLE ((t.truncLT 0).obj X) (-1)
+ instance (X : C) [IsCofibrant X] : IsCofibrant (HoCat.resolutionObj X)
+ instance (X : C) [IsFibrant X] : IsFibrant (HoCat.resolutionObj X)
+ instance (X : C) [t.IsGE X 0] : t.IsGE X (-1)
+ instance (X : C) [t.IsGE X n] : t.IsGE (X⟦(-1 : ℤ)⟧) n := by
+ instance (X : C) [t.IsLE X 0] : t.IsLE X 1
+ instance (X : CofibrantObject.HoCat C) : WeakEquivalence (HoCat.adj.unit.app X) := by
+ instance (X : CofibrantObject.HoCat C) : WeakEquivalence (HoCat.adjUnit.app X) := by
+ instance (X : HomotopyCategory.Plus (InjectiveObject C)) (n : ℤ) :
+ instance (X : HomotopyCategory.Plus (InjectiveObject C)) :
+ instance (X : HomotopyCategory.Plus (ProjectiveObject C)) (n : ℤ) :
+ instance (X : InjectiveObject C) : Injective ((ι C).obj X) := X.2
+ instance (X : InjectiveObject C) : Injective X.obj := X.2
+ instance (X : Minus C) (n : ℤ) [X.IsGE n] : (ι.obj X).IsGE n := by
+ instance (X : Minus C) (n : ℤ) [X.IsLE n] : (ι.obj X).IsLE n := by
+ instance (X : Plus C) (n : ℤ) [X.IsGE n] : (ι.obj X).IsGE n := by
+ instance (X : Plus C) (n : ℤ) [X.IsLE n] : (ι.obj X).IsLE n := by
+ instance (X : ProjectiveObject C) : Projective ((ι C).obj X) := X.2
+ instance (X : ProjectiveObject C) : Projective X.obj := X.2
+ instance (X : SpectralObject C EInt) [X.IsFirstQuadrant] (n : ℕ) :
+ instance (X : SpectralObject C EInt) [X.IsFirstQuadrant] (n : ℤ) :
+ instance (X : SpectralObject C EInt) [X.IsThirdQuadrant] (n : ℕ) :
+ instance (X : t.Heart) : t.IsGE (t.ιHeart.obj X) 0
+ instance (X : t.Heart) : t.IsLE (t.ιHeart.obj X) 0
+ instance (X : t₁.Heart) :
+ instance (X₁ : C₁) :
+ instance (X₁ X₂ : C) : AdmissibleEpi (biprod.fst : X₁ ⊞ X₂ ⟶ X₁) := by
+ instance (X₁ X₂ : C) : AdmissibleEpi (biprod.snd : X₁ ⊞ X₂ ⟶ X₂)
+ instance (X₁ X₂ : C) : AdmissibleMono (biprod.inl : _ ⟶ X₁ ⊞ X₂)
+ instance (X₁ X₂ : C) : AdmissibleMono (biprod.inr : _ ⟶ X₁ ⊞ X₂) := by
+ instance (X₂ : C₂) : ((h.curry G).flip.obj X₂).CommShift M
+ instance (Y : C) : HasIterationOfShape J (Over Y)
+ 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 (i : I) : PreservesColimitsOfShape K (eval i : _ ⥤ C)
+ instance (i : WithBot (α n)) : Mono (h.filtrationι i) := by
+ instance (i : α n) (pq : ι) (hpq : s.position n i = pq) :
+ instance (i : α) : HasBinaryBiproduct (K.op.X i) (K.op.X i) := by
+ instance (i : ι) : (eval V c i).PreservesZeroMorphisms
+ instance (i : ι) : IsIso ((K.ιStupidTrunc e).f (e.f i))
+ instance (i : ι) : IsIso ((K.πStupidTrunc e).f (e.f i))
+ instance (i' : ι') : Epi ((K.πStupidTrunc e).f i') := by
+ instance (i' : ι') : Mono ((K.ιStupidTrunc e).f i') := by
+ instance (j : J) [OrderBot J] [SuccOrder J] :
+ instance (k : ℕ) : E.HasEdgeEpiAtFrom pq (r + k)
+ instance (k : ℕ) : E.HasEdgeMonoAtFrom pq (r + k)
+ instance (k : ℕ) : Epi (E.edgeEpiSteps' pq r k) := by
+ instance (k : ℕ) : Mono (E.edgeMonoSteps' pq r k) := by
+ instance (n : σ) (i : α n) (j : WithBot (α n)) :
+ instance (n : σ) (i : α n) : Subsingleton (s.segment' n i ⊥)
+ instance (n : σ) (i j : α n) : Fintype (s.segment n i j) := by
+ instance (n : ℕ) : (F.homologyRightTExact t₁ t₂ n).Additive := by
+ instance (n : ℕ) : (F.rightDerived' n).Additive := by
+ instance (n : ℤ) (F : CofFibFactorizationQuasiIsoLE f n) : F.1.QuasiIsoLE n := F.2
+ instance (n : ℤ) (X : C) : IsIso ((truncGEComparison F t₁ t₂ n).app X) := by
+ instance (n : ℤ) (X : C) : IsIso ((truncLEComparison F t₁ t₂ n).app X) := 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 : ℤ) (j : ι) : Epi (X.πAbutmentFiltration n j) := by
+ instance (n : ℤ) (j : ι) : Mono (X.abutmentFiltrationι n j) := by
+ instance (n : ℤ) (j₁ j₂ : ι) (h : j₁ ≤ j₂) :
+ instance (n : ℤ) :
+ instance (n : ℤ) : (CochainComplex.singleFunctor C n ⋙ Q).Faithful
+ instance (n : ℤ) : (CochainComplex.singleFunctor C n ⋙ Q).Full
+ instance (n : ℤ) : (t.homology n).Additive := by
+ instance (n : ℤ) : (t.truncGT n).Additive := by
+ instance (n : ℤ) : (t.truncLE n).Additive := by
+ instance (n : ℤ) : Category (CofFibFactorizationQuasiIsoLE f n) := by
+ instance (n : ℤ) : Epi (K.πTruncGE n) := by
+ instance (n : ℤ) : IsIso (truncGEComparison F t₁ t₂ n)
+ instance (n : ℤ) : IsIso (truncLEComparison F t₁ t₂ n)
+ 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 (n : ℤᵒᵖ) : (K.rowFiltrationGE.obj n).HasTotal (up ℤ) := by
+ instance (n : ℤᵒᵖ) {ι' : Type*} {c' : ComplexShape ι'}
+ instance (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (i j : ι) (hij : i ≤ j) :
+ instance (p : ℤ) : Injective ((I f n).X p) := by
+ instance (pq : ι) (r r' : ℤ) (hrr' : r + 1 = r') [E.HasEdgeEpiAt pq r] :
+ instance (pq : ι) (r r' : ℤ) (hrr' : r + 1 = r') [E.HasEdgeMonoAt pq r] :
+ instance (pq : ℕ × ℕ) : E.HasPageInfinityAt pq
+ instance (pq : ℕ × ℕ) : Y.StationaryAt mkDataE₂CohomologicalNat pq
+ instance (pq : ℕ × ℕ) : Y.StationaryAt mkDataE₂HomologicalNat pq
+ instance (pq : ℤ × ℤ) : Y.StationaryAt mkDataE₂Cohomological pq
+ instance (priority := 100) guitartExact_of_isEquivalence_of_isIso'
+ instance (q : ℕ) : E.HasEdgeMonoAtFrom ⟨0, q⟩ 1
+ instance (q : ℤ) :
+ instance (q : ℤ) : Injective ((K.injectiveResolution n).X q)
+ instance (r : ℤ) [E.HasEdgeEpiAtFrom pq r] :
+ instance (r : ℤ) [E.HasEdgeMonoAtFrom pq r] :
+ instance (Ψ : LocalizerMorphism W₂ W₃) [Φ.IsLocalizedEquivalence]
+ instance (α : F ⟶ G) [IsIso α] : IsIso (NatTrans.op α) := (NatIso.op (asIso α)).isIso_hom
+ instance (α : F ⟶ L ⋙ F') [F'.IsLeftKanExtension α] :
+ instance (α : L ⋙ F' ⟶ F) [F'.IsRightKanExtension α] :
+ instance (α : TwoSquare T L R B) [IsIso α.natTrans] : IsIso α.op.natTrans := by
+ instance (α : h.Hom h' f) : IsIso (α.τ.app ⊥)
+ instance : ((curriedTensor _).flip.obj K).CommShift ℤ
+ instance : ((curriedTensor _).flip.obj K).IsTriangulated
+ instance : ((curriedTensor _).obj K).CommShift ℤ
+ instance : ((curriedTensor _).obj K).IsTriangulated
+ instance : (BifibrantObject.HoCat.ιCofibrantObject (C := C)).Faithful
+ instance : (BifibrantObject.HoCat.ιCofibrantObject (C := C)).Full
+ instance : (DerivedCategory.Minus.homologyFunctor C 0).ShiftSequence ℤ := by
+ instance : (DerivedCategory.Plus.homologyFunctor C 0).ShiftSequence ℤ := by
+ instance : (F.mapHomotopyCategory c).Faithful
+ instance : (F.mapHomotopyCategoryMinus).CommShift ℤ := by
+ instance : (F.mapHomotopyCategoryMinus).IsTriangulated := by
+ instance : (F.mapHomotopyCategoryPlus).CommShift ℤ := by
+ instance : (F.mapHomotopyCategoryPlus).IsTriangulated := by
+ instance : (G.rightDerivedFunctorPlus ⋙ homologyFunctor C 0).VanishesOnGEOne t
+ instance : (HomotopyCategory.Minus.quotient (ProjectiveObject C)).IsLocalization
+ instance : (HomotopyCategory.Plus.localizerMorphism C).arrow.HasRightResolutions := by
+ instance : (HomotopyCategory.Plus.localizerMorphism C).functor.CommShift ℤ := by
+ instance : (HomotopyCategory.Plus.localizerMorphism C).functor.IsTriangulated := by
+ instance : (HomotopyCategory.Plus.quotient (InjectiveObject C)).IsLocalization
+ instance : (HomotopyCategory.quasiIso A (.up ℤ)).kFlat.IsTriangulated
+ instance : (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasLeftCalculusOfFractions := by
+ instance : (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasRightCalculusOfFractions := by
+ instance : (HomotopyCategory.subcategoryAcyclic C).IsLeftLocalizing (HomotopyCategory.Minus.ι C)
+ instance : (HomotopyCategory.subcategoryAcyclic C).IsRightLocalizing (HomotopyCategory.Plus.ι C)
+ instance : (K.injectiveResolution n).IsStrictlyGE n
+ instance : (L A).IsLocalizedEquivalence
+ instance : (L A).functor.EssSurj
+ instance : (L A).functor.Full
+ instance : (L A).functor.IsLocalization (WL A)
+ instance : (ObjectProperty.flat (A := A)).ContainsZero
+ instance : (ObjectProperty.flat (A := A)).IsStableUnderRetracts
+ instance : (Q (C := C)).LaxMonoidal
+ instance : (Q : _ ⥤ DerivedCategory C).mapArrow.EssSurj
+ instance : (Qh (C := C)).EssSurj
+ instance : (Qh (C := C)).Faithful
+ instance : (Qh (C := C)).Full
+ instance : (Qh (C := C)).IsEquivalence
+ instance : (Qh (C := C)).LaxMonoidal
+ instance : (Qh : _ ⥤ Minus C).CommShift ℤ := by
+ instance : (Qh : _ ⥤ Minus C).IsTriangulated := by
+ instance : (Qh : _ ⥤ Plus C).CommShift ℤ := by
+ instance : (Qh : _ ⥤ Plus C).IsTriangulated := by
+ instance : (R A).IsLocalizedEquivalence := by
+ instance : (R A).functor.EssSurj := by
+ instance : (S.tStructure t).HasHeart
+ instance : (S.tStructure t).HasHomology₀
+ instance : (ShortComplex.fAdmissible (shortExact C)).IsStableUnderCobaseChange
+ instance : (ShortComplex.fAdmissible (shortExact C)).IsStableUnderComposition
+ instance : (ShortComplex.gAdmissible (shortExact C)).IsStableUnderBaseChange
+ instance : (ShortComplex.gAdmissible (shortExact C)).IsStableUnderComposition
+ instance : (W.localizerMorphismOfIsCompatibleWithShift a).IsLocalizedEquivalence := by
+ instance : (bifunctor L W).IsLeftDerivedFunctor₂ (counit L W) W W
+ instance : (cofibrantObjectLocalizerMorphism C).IsInduced
+ instance : (cofibrantObjectLocalizerMorphism C).functor.IsEquivalence := by
+ instance : (cofibrations (CategoryWithSmithStructure hIW₁ hIW₃)).HasFunctorialFactorization
+ instance : (cofibrations (Plus C)).HasFactorization (trivialFibrations (Plus C))
+ instance : (cofibrations (Plus C)).IsStableUnderRetracts
+ instance : (curriedTensor (DerivedCategory C)).IsLeftDerivedFunctor₂
+ instance : (curriedTensor (DerivedMonoidal L W)).IsLeftDerivedFunctor₂
+ instance : (curriedTensor C).Additive
+ instance : (degreewiseEpiWithInjectiveKernel (C := C)).IsStableUnderRetracts
+ instance : (degreewiseMonoWithProjectiveCokernel (C := C)).IsMultiplicative := by
+ instance : (degreewiseMonoWithProjectiveCokernel (C := C)).IsStableUnderRetracts := by
+ instance : (epiWithInjectiveKernel (C := C)).IsStableUnderRetracts
+ instance : (exactFunctor (C := C) (D := D)).IsClosedUnderIsomorphisms := by
+ instance : (fibrantObjectLocalizerMorphism C).IsInduced
+ instance : (fibrantObjectLocalizerMorphism C).functor.IsEquivalence := by
+ instance : (fibrations (Plus C)).IsStableUnderRetracts
+ instance : (flat (A := A)).IsClosedUnderIsomorphisms
+ instance : (flat (A := A)).IsMonoidal
+ instance : (hE 0).CollapsesAt 0
+ instance : (hE 1).CollapsesAsSESAt 0 1
+ instance : (id W₁).IsInduced
+ instance : (id W₁).functor.IsEquivalence := by dsimp; infer_instance
+ instance : (leftDerived₂ F L₁ L₂ W₁ W₂).IsLeftDerivedFunctor₂
+ instance : (leftDerived₃ F L₁ L₂ L₃ W₁ W₂ W₃).IsLeftDerivedFunctor₃
+ instance : (leftDerived₄ F L₁ L₂ L₃ L₄ W₁ W₂ W₃ W₄).IsLeftDerivedFunctor₄
+ instance : (leftExactFunctor C D).IsClosedUnderIsomorphisms
+ instance : (localizerMorphism C).IsLeftDerivabilityStructure := by
+ instance : (localizerMorphism C).IsLocalizedEquivalence
+ instance : (localizerMorphism C).IsLocalizedEquivalence := by
+ instance : (localizerMorphism C).IsRightDerivabilityStructure
+ instance : (localizerMorphism C).IsRightDerivabilityStructure := by
+ instance : (localizerMorphism C).arrow.HasRightResolutions := by
+ instance : (map₂HomologicalComplex F c₁ c₂ c).Additive
+ instance : (map₂HomologicalComplex F c₁ c₂ c).flip.Additive
+ instance : (minus C).IsTriangulated
+ instance : (monoWithProjectiveCokernel : MorphismProperty C).IsMultiplicative := by
+ instance : (monoWithProjectiveCokernel : MorphismProperty C).IsStableUnderRetracts := by
+ instance : (ofNatTrans τ).IsClosedUnderIsomorphisms
+ instance : (ofNatTrans τ).IsTriangulated
+ instance : (opFunctor V c).IsEquivalence := (opEquivalence V c).isEquivalence_functor
+ instance : (opInverse V c).IsEquivalence := (opEquivalence V c).isEquivalence_inverse
+ instance : (plus C).IsTriangulated
+ instance : (quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ := by
+ instance : (quasiIso C c).IsMultiplicative
+ instance : (quasiIso C).HasTwoOutOfThreeProperty := by
+ instance : (quasiIso C).IsStableUnderRetracts := by
+ instance : (quotient C c).Monoidal
+ instance : (rightExactFunctor C D).IsClosedUnderIsomorphisms
+ instance : (spectralSequence X data).HasEdgeEpiAtFrom pq (X.stationaryPage data pq)
+ instance : (spectralSequence X data).HasEdgeMonoAtFrom pq (X.stationaryPage data pq)
+ instance : (spectralSequence X data).HasPageInfinityAt pq
+ instance : (subcategoryAcyclic C).IsStableUnderRetracts := by
+ instance : (t : TStructure (DerivedCategory C)).HasHeart
+ instance : (t : TStructure (DerivedCategory C)).HasHomology₀
+ instance : (t : TStructure (DerivedCategory C)).homology₀.ShiftSequence ℤ
+ instance : (toDerivedMonoidal L W).IsLocalization W := by assumption
+ instance : (toDerivedMonoidal L W).LaxMonoidal
+ instance : (toGradedObjectFunctor C c₁ c₂).Additive
+ instance : (toHomotopyCategory (C := C)).EssSurj
+ instance : (toHomotopyCategory (C := C)).Full
+ instance : (trivialCofibrations (CategoryWithSmithStructure hIW₁ hIW₃)).HasFactorization
+ instance : (trivialCofibrations (Plus C)).HasFactorization (fibrations (Plus C))
+ instance : (weakEquivalences (Plus C)).HasTwoOutOfThreeProperty
+ instance : (weakEquivalences (Plus C)).IsStableUnderRetracts
+ instance : (Λ.cochainComplex X).IsStrictlyLE 0
+ instance : (ιCofibrantObjectLocalizerMorphism C).IsLocalizedEquivalence := by
+ instance : (ιFibrantObjectLocalizerMorphism C).IsLocalizedEquivalence := by
+ instance : (𝟭 C).IsLocalization (MorphismProperty.isomorphisms C)
+ instance : AB5OfSize.{0, 0} (ModuleCat.{u} R) := AB5OfSize_shrink.{0, 0, u, u, u} _
+ instance : Abelian t.Heart := by
+ instance : Add (X ⟶ Y)
+ instance : AddCommGroup (GrothendieckGroup C) := by
+ instance : AddCommGroup (X ⟶ Y)
+ instance : Category (Arrow₂ C)
+ instance : Category (Arrow₃ C)
+ instance : Category (Arrow₄ C)
+ instance : Category (Arrow₅ C)
+ instance : Category (Arrow₆ C)
+ instance : Category (Arrow₇ C)
+ instance : Category (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : Category (CofFibFactorization f) := by
+ instance : Category (DerivedMonoidal L W) := inferInstanceAs (Category D)
+ instance : Category (HomFactorization f)
+ instance : Category (Q C)
+ instance : Category (ShortComplex₄ C)
+ instance : Category (ShortComplex₅ C)
+ instance : Category (SpectralObject C ι)
+ instance : Category (SpectralSequence C c r₀)
+ instance : Category t.Heart := ht.cat
+ instance : CategoryWithCofibrations (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : CategoryWithFibrations (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : CategoryWithWeakEquivalences (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : CochainComplex.IsGE
+ instance : Congruence (homRel C)
+ instance : E.HasEdgeEpiAt pq r
+ instance : E.HasEdgeEpiAtFrom pq (E.rFromMin pq)
+ instance : E.HasEdgeEpiAtFrom pq (E.rMin pq)
+ instance : E.HasEdgeMonoAt pq r
+ instance : E.HasEdgeMonoAtFrom pq (E.rMin pq)
+ instance : E.HasEdgeMonoAtFrom pq (E.rToMin pq)
+ instance : E.Z.IsStrictlyGE (-n-1) := by
+ instance : E.Z.IsStrictlyLE 0 := by
+ instance : Epi (I.shortComplex.g) := epi_of_epi_fac I.shortComplex_g_fac
+ instance : Epi (K.πStupidTrunc e) := epi_of_epi_f _ inferInstance
+ instance : Epi (X.abutmentFiltrationShortComplex n₀ n₁ n₂ hn₁ hn₂ i j hij).g := by
+ 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 : Epi (h.pageInfinityπ i pq hpq hi) := by
+ instance : Epi (h.shortComplex i j hij pq hpq).g := by dsimp; infer_instance
+ instance : Epi (h.shortComplexOfCollapses i j pqi pqj hpqi hpqj).g := by
+ instance : Epi (toImageOfFac f p i fac)
+ instance : Epi (π X hdata n i pq hpq) := epi_comp _ _
+ instance : Epi E.shortComplex.g := by
+ instance : Epi I.shortComplex.g := epi_of_epi_fac I.shortComplex_g_fac
+ instance : F.HasPointwiseRightDerivedFunctor (HomotopyCategory.Plus.quasiIso C)
+ instance : F.homologicalKernel.IsStableUnderRetracts
+ instance : F.rightDerivedFunctorPlus.CommShift ℤ
+ instance : F.rightDerivedFunctorPlus.IsTriangulated
+ instance : F.rightDerivedFunctorPlus.RightTExact t t
+ instance : Fintype (K.coreHasTotalOfIsStrictlyLE x₀ y₀ n).J := by
+ instance : Functor.Full (toHoCat (C := C)) := by dsimp [toHoCat]; infer_instance
+ instance : HasBinaryBiproducts (InjectiveObject C) := hasBinaryBiproducts_of_finite_biproducts _
+ instance : HasBinaryBiproducts (ProjectiveObject C) := hasBinaryBiproducts_of_finite_biproducts _
+ instance : HasBinaryProducts C := inferInstance
+ instance : HasColimitsOfSize.{w, w} C := by
+ instance : HasCoproduct (K.toGradedObject.mapObjFun (π c₁ c₂ c) n ∘ κ.φ) := κ.hasCoproduct'
+ instance : HasFiniteBiproducts (InjectiveObject C)
+ instance : HasFiniteBiproducts (ObjectProperty.flat (A := A)).FullSubcategory
+ instance : HasFiniteBiproducts (ProjectiveObject C)
+ instance : HasFiniteColimits (CategoryWithSmithStructure hIW₁ hIW₃) := by
+ instance : HasFiniteColimits (Plus C)
+ instance : HasFiniteCoproducts (ProjectiveObject C)
+ instance : HasFiniteLimits (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : HasFiniteLimits (Plus C)
+ instance : HasFiniteProducts (InjectiveObject C)
+ instance : HasFiniteProducts (ObjectProperty.flat (A := A)).FullSubcategory
+ instance : HasFiniteProducts t.Heart
+ instance : HasFiniteProducts t.heart.FullSubcategory
+ instance : HasFunctorialFlatResolution (ModuleCat.{u} R)
+ instance : HasHomotopyCofiber ((opFunctor C c).map φ.op)
+ instance : HasShift (Minus C) ℤ
+ instance : HasShift (Plus C) ℤ
+ instance : HasTerminal t.heart.FullSubcategory := by
+ instance : HasZeroObject (InjectiveObject C)
+ instance : HasZeroObject (ProjectiveObject C)
+ instance : HoCat.bifibrantResolution.IsLocalization (weakEquivalences (HoCat C))
+ instance : HomRel.IsStableUnderPostcomp (homRel C)
+ instance : HomRel.IsStableUnderPrecomp (homRel C)
+ instance : IsEquivalence (LeftExtension.postcomp₂ L F G) := by
+ instance : IsIso ((hE 1).filtrationι (WithBot.some 1))
+ instance : IsIso ((hE 1).filtrationι 1) := by
+ instance : IsIso ((hE 1).π 0 (1, 0) rfl) := by
+ instance : IsIso ((hE 2).π 0 (2, 0) rfl) := by
+ instance : IsIso (Functor.LaxMonoidal.ε (toDerivedMonoidal L W))
+ instance : IsIso (HoCat.adj (C := C)).counit := by
+ instance : IsIso (HoCat.adjCounit' (C := C)) := NatIso.isIso_of_isIso_app _
+ instance : IsIso (connectShortComplexι S T e φ hφ).τ₁ := by dsimp; infer_instance
+ instance : IsIso (connectShortComplexι S T e φ hφ).τ₂ := by dsimp; infer_instance
+ instance : IsIso (connectShortComplexπ S T e φ hφ).τ₂ := by dsimp; infer_instance
+ instance : IsIso (connectShortComplexπ S T e φ hφ).τ₃ := by dsimp; infer_instance
+ instance : IsIso (h.filtrationι i)
+ instance : IsIso (h.π i pq hpq)
+ instance : IsIso (hom X hdata n i j hij pq hpq h)
+ instance : IsIso (hom' X hdata n i j hij pq hpq h)
+ 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 : IsLocallyPresentable.{w} (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : IsSmall.{w} hm.morphismProperty := hm.choose_spec.choose
+ instance : LocallySmall.{w} C := by
+ instance : ModelCategory (CategoryWithSmithStructure hIW₁ hIW₃)
+ instance : Mono ((π' f n).f n) := by
+ instance : Mono (F.1.i) := F.2.hi
+ instance : Mono (I.shortComplex.f) := mono_of_mono_fac I.shortComplex_f_fac
+ instance : Mono (K.ιStupidTrunc e) := mono_of_mono_f _ inferInstance
+ instance : Mono (X.EToCycles n₀ n₁ n₂ hn₁ hn₂ f₁ f₂ f₃ f₂₃ h₂₃)
+ instance : Mono (X.abutmentFiltrationShortComplex n₀ n₁ n₂ hn₁ hn₂ i j hij).f := by
+ 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 (h.pageInfinityι i pq hpq hi) := by
+ instance : Mono (h.shortComplex i j hij pq hpq).f := by dsimp; infer_instance
+ instance : Mono (h.shortComplexOfCollapses i j pqi pqj hpqi hpqj).f := by
+ instance : Mono (homologyShortComplex'' f n).f
+ instance : Mono (i f n) := mono_of_mono_fac (fac f n)
+ instance : Mono (i f n₀) := mono_of_mono_fac (fac f n₀)
+ instance : Mono (kfSc X data r r' hrr' hr pq' pq'' n₀ n₁ n₂ hn₁ hn₂ hn₁'
+ instance : MonoidalCategory (DerivedCategory C)
+ instance : MonoidalCategory (DerivedMonoidal L W)
+ instance : MonoidalPreadditive (HomologicalComplex C c)
+ instance : NatTrans.CommShift (h.uncurryCurryIso G).hom (M × M)
+ instance : NatTrans.CommShift F.rightDerivedFunctorPlusUnit ℤ := by
+ instance : Neg (X ⟶ Y)
+ instance : P.ι.IsTriangulated
+ instance : P.ι.ReflectsEpimorphisms
+ instance : P.ι.ReflectsMonomorphisms
+ instance : Preadditive (GradedObject I C)
+ instance : Preadditive (HomotopyCategory V c) := Quotient.preadditive _ (by
+ instance : Preadditive t.Heart := ht.preadditive
+ instance : Preregular C
+ instance : Pretriangulated P.FullSubcategory
+ instance : Qh.IsLocalization (.isomorphisms (KInjectives C)) := by
+ instance : Qh.IsLocalization (HomotopyCategory.Minus.quasiIso C) := by
+ instance : Qh.IsLocalization (HomotopyCategory.Minus.subcategoryAcyclic C).trW
+ instance : Qh.IsLocalization (HomotopyCategory.Plus.quasiIso C) := by
+ instance : Qh.IsLocalization (HomotopyCategory.Plus.subcategoryAcyclic C).trW
+ instance : QuasiIso (K.ιInjectiveResolution n)
+ instance : QuasiIso (compZToZ E E' hn'') := by
+ instance : QuasiIso (i f n₀)
+ instance : QuasiIso (Λ.cochainComplexNatTransπ.app X) := by
+ instance : QuasiIso (Λ.cochainComplexπ X)
+ instance : QuasiIso (Λ.totalπ K) := by
+ instance : QuasiIso (Λ.totalπ' K) := by
+ instance : QuasiIso E.ZToX₁
+ instance : QuasiIsoAt (K.ιTruncLE n) n
+ instance : QuasiIsoAt (K.πTruncGE n) n
+ instance : QuasiIsoAt (Λ.cochainComplexπ X) 0 := by
+ instance : S.ι.TExact (S.tStructure t) t
+ instance : TwoSquare.GuitartExact (iso A).inv
+ instance : TwoSquare.GuitartExact (iso C).hom
+ instance : TwoSquare.GuitartExact (iso C).inv
+ instance : W.localizerMorphismKFlat.IsInduced
+ instance : W.localizerMorphismKFlat.functor.Faithful := by dsimp; infer_instance
+ instance : W.localizerMorphismKFlat.functor.Full := by dsimp; infer_instance
+ instance : Y.HasSpectralSequence mkDataE₂CohomologicalNat
+ instance : Y.HasSpectralSequence mkDataE₂HomologicalNat
+ instance : Zero (S₁ ⟶ S₂) := ⟨{ τ₁ := 0, τ₂ := 0, τ₃ := 0, τ₄ := 0 }⟩
+ instance : Zero (S₁ ⟶ S₂) := ⟨{ τ₁ := 0, τ₂ := 0, τ₃ := 0, τ₄ := 0, τ₅ := 0 }⟩
+ instance : mkDataE₂Cohomological.HasFirstPageComputation
+ instance : mkDataE₂CohomologicalNat.HasFirstPageComputation
+ instance : mkDataE₂HomologicalNat.HasFirstPageComputation
+ instance : t.IsGE (t.truncGETriangle T n).obj₁ n := by dsimp; infer_instance
+ instance : t.IsGE (t.truncGETriangle T n).obj₂ n := by dsimp; infer_instance
+ instance : t.IsGE (t.truncGETriangle T n).obj₃ n := by dsimp; infer_instance
+ instance : t.IsLE (t.truncLETriangle T n).obj₁ n := by dsimp; infer_instance
+ instance : t.IsLE (t.truncLETriangle T n).obj₂ n := by dsimp; infer_instance
+ instance : t.IsLE (t.truncLETriangle T n).obj₃ n := by dsimp; infer_instance
+ instance : t.bounded.ContainsHeart t
+ instance : t.bounded.HasInducedTStructure t := by
+ instance : t.bounded.IsTriangulated := by
+ instance : t.heart.IsClosedUnderIsomorphisms
+ instance : t.heart.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
+ instance : t.homology₀.Additive := by
+ instance : t.homology₀.IsHomological
+ instance : t.minus.ContainsHeart t
+ instance : t.minus.HasInducedTStructure t
+ instance : t.minus.IsTriangulated
+ instance : t.plus.ContainsHeart t
+ instance : t.plus.HasInducedTStructure t
+ instance : t.plus.IsTriangulated
+ instance : t.ιHeart.Additive := ht.additive_ι
+ instance : t.ιHeart.Faithful := ht.faithful_ι
+ instance : t.ιHeart.Full := ht.fullι
+ instance : toHoCat.IsLocalization (weakEquivalences (BifibrantObject C))
+ instance : toHomotopyCategory.IsLocalization (KInjectives.quasiIso C) := by
+ instance : Λ.chainComplexFunctor.PreservesZeroMorphisms
+ instance : Λ.cochainComplexFunctor.PreservesZeroMorphisms
+ instance : Φ.inv.IsInduced
+ instance : Φ.inv.functor.IsEquivalence := by
+ instance : ι.PreservesTotalComplex ((bicomplexFunctor Λ).obj K.obj)
+ instance [(weakEquivalences C).RespectsIso] :
+ instance [AdmissibleEpi f] [AdmissibleEpi g] : AdmissibleEpi (f ≫ g)
+ instance [AdmissibleEpi g] (f : Z' ⟶ Z) : AdmissibleEpi (pullback.fst f g)
+ instance [AdmissibleEpi g] (f : Z' ⟶ Z) : AdmissibleEpi (pullback.snd g f)
+ instance [AdmissibleEpi g] (f : Z' ⟶ Z) : HasPullback f g
+ instance [AdmissibleEpi g] (f : Z' ⟶ Z) : HasPullback g f
+ instance [AdmissibleEpi g] : Epi g := by
+ instance [AdmissibleMono f] (g : X ⟶ X') : AdmissibleMono (pushout.inl g f)
+ instance [AdmissibleMono f] (g : X ⟶ X') : AdmissibleMono (pushout.inr f g)
+ instance [AdmissibleMono f] (g : X ⟶ X') : HasPushout f g
+ instance [AdmissibleMono f] (g : X ⟶ X') : HasPushout g f
+ instance [AdmissibleMono f] : Mono f := by
+ instance [AdmissibleMono f] [AdmissibleMono g] : AdmissibleMono (f ≫ g)
+ instance [B.IsLeftLocalizing F] : B.op.IsRightLocalizing F.op
+ instance [CategoryWithHomology C] : (quasiIso C).RespectsIso := by
+ instance [E.HasEdgeEpiAtFrom pq 2] : E.HasEdgeEpiAtFrom pq 3 := by
+ instance [E.HasEdgeMonoAtFrom (0, 1) 3] [E.HasEdgeEpiAtFrom (0, 1) 3] :
+ instance [E.HasEdgeMonoAtFrom (1, 0) 2] [E.HasEdgeEpiAtFrom (1, 0) 2]
+ instance [E.HasEdgeMonoAtFrom (1, 0) 2] [E.HasEdgeEpiAtFrom (1, 0) 2] : Mono (ιE₂OneZero hE) := by
+ instance [E.HasEdgeMonoAtFrom (2, 0) 3] [E.HasEdgeEpiAtFrom (2, 0) 3] : Mono (ιE₃TwoZero hE) := by
+ instance [E.HasEdgeMonoAtFrom pq 2] : E.HasEdgeMonoAtFrom pq 3 := by
+ instance [Epi S.g] : Epi (connectShortComplexπ S T e φ hφ).τ₁ := epi_comp _ _
+ instance [F'.IsLeftDerivedFunctor α W] :
+ instance [F'.IsRightDerivedFunctor β W] :
+ instance [F.Faithful] : (sheafCompose J F).Faithful
+ instance [F.IsTriangulated] : F.op.IsTriangulated
+ instance [Full F] [Faithful F] : Faithful F.mapHomotopyCategoryMinus
+ instance [Full F] [Faithful F] : Faithful F.mapHomotopyCategoryPlus
+ instance [Full F] [Faithful F] : Full F.mapHomotopyCategoryMinus
+ instance [Full F] [Faithful F] : Full F.mapHomotopyCategoryPlus
+ instance [HasBinaryBiproduct P Q] :
+ instance [HasBinaryBiproducts C] : HasBinaryBiproducts Cᵒᵖ
+ instance [HasBinaryBiproducts C] : HasHomotopyFiber φ
+ instance [HasColimitsOfShape B C₁]
+ instance [HasColimitsOfShape B C₂]
+ instance [HasColimitsOfShape J C] (i : ι) :
+ instance [HasColimitsOfShape K C] : HasColimitsOfShape K (GradedObject I C)
+ instance [HasFiniteColimits C] (i : ι) :
+ instance [HasFiniteLimits C] (i : ι) :
+ instance [HasIterationOfShape J C] (Y : C) :
+ instance [HasLimitsOfShape J C] (i : ι) :
+ instance [HasSheafify J (Type w)] : Balanced (Sheaf J (Type w))
+ instance [HasZeroMorphisms C] : (CochainComplex.minus C).IsClosedUnderIsomorphisms
+ instance [HasZeroMorphisms C] : (CochainComplex.plus C).IsClosedUnderIsomorphisms
+ instance [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [HasZeroObject C₂]
+ instance [HasZeroObject C₁] (X₁ : C₁) (K₂ : CochainComplex C₂ ℤ) (x₁ : ℤ) :
+ instance [HasZeroObject C₂] (X₂ : C₂) (K₁ : CochainComplex C₁ ℤ) (x₂ : ℤ) :
+ instance [IsConnected C] [IsConnected D] : IsConnected (C × D) := by
+ instance [IsIdempotentComplete C] [P.IsStableUnderRetracts] :
+ instance [IsIso α] : LF.IsLeftDerivedFunctor α W
+ instance [IsIso α] : RF.IsRightDerivedFunctor α W
+ instance [IsTriangulated C] : IsTriangulated P.FullSubcategory
+ instance [K.HasTotal c] : HomologicalComplex₂.HasTotal (K.stupidTrunc e) c
+ instance [K.IsStrictlySupported e] : IsIso (K.ιStupidTrunc e) := by
+ instance [K.IsStrictlySupported e] : IsIso (K.πStupidTrunc e) := by
+ instance [L.IsEquivalence] [R.IsEquivalence] [IsIso w.natTrans] : GuitartExact w := by
+ instance [LocallySmall.{w} C] : LocallySmall.{w} (Arrow C)
+ instance [LocallySmall.{w} C] : LocallySmall.{w} (HoCat C) := by
+ instance [Mono T.f] : Mono (connectShortComplexι S T e φ hφ).τ₃ := mono_comp _ _
+ instance [Mono i] : IsIso (toImageOfFac f p i fac) := by
+ instance [Mono i] : Mono (toImageOfFac f p i fac)
+ instance [OrderBot J] : (diagramFunctor f ⋙ colim).IsWellOrderContinuous
+ instance [OrderBot J] : (diagramFunctor f).IsWellOrderContinuous
+ instance [P.IsClosedUnderIsomorphisms] :
+ instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+ instance [P.IsStableUnderRetracts] :
+ instance [P.IsTriangulated] : (P.inverseImage F).IsTriangulated
+ instance [P.IsTriangulated] : P.trW.IsStableUnderFiniteProducts := by
+ instance [Preadditive C] [Preadditive D] [Preadditive E] [G.Additive] (a : A)
+ instance [W.ContainsIdentities] : W.WKFlat.ContainsIdentities := by
+ instance [W.ContainsIdentities] [W.RespectsIso] :
+ instance [W.IsStableUnderFiniteCoproducts] (J : Type w) [Finite J] :
+ instance [W.IsStableUnderTransfiniteCompositionOfShape J]
+ instance [W.RespectsIso] :
+ instance [W.RespectsIso] : W.kFlat.IsClosedUnderIsomorphisms
+ instance [W.RespectsIso] : W.kFlat.IsMonoidal
+ instance [W.RespectsIso] [W.localizerMorphismKFlat.IsLeftDerivabilityStructure]
+ instance [W₂.RespectsIso] :
+ instance [Wₕ.IsMultiplicative] [Wₕ.RespectsIso] [L.functor.EssSurj] [R.functor.Full]
+ instance [e₁.IsTruncGE] [e₂.IsTruncGE] : Mono (K.mapStupidTruncGE h)
+ instance [e₁.IsTruncLE] [e₂.IsTruncLE] : Epi (K.mapStupidTruncLE h)
+ instance [hg : IsIso f] : AdmissibleMono f
+ instance [hg : IsIso g] : AdmissibleEpi g
+ instance [t.IsGE X 0] [H.VanishesOnGEOne t] :
+ instance [t.homology₀.ShiftSequence ℤ] :
+ instance [w.GuitartExact] (α : T' ⟶ T) (β : B ⟶ B')
+ instance [Φ.IsInduced] : Φ.op.IsInduced
+ instance [Φ.IsLeftDerivabilityStructure] : Φ.op.IsRightDerivabilityStructure := by
+ instance [Φ.IsLocalizedEquivalence] : Φ.op.IsLocalizedEquivalence := by
+ instance [Φ.IsRightDerivabilityStructure] : Φ.op.IsLeftDerivabilityStructure := by
+ instance [Φ₁.HasLeftResolutions] [Φ₂.HasLeftResolutions] :
+ instance [Φ₁.HasRightResolutions] [Φ₂.HasRightResolutions] :
+ instance [Φ₁.IsLeftDerivabilityStructure] [Φ₂.IsLeftDerivabilityStructure] :
+ instance [Φ₁.IsRightDerivabilityStructure] [Φ₂.IsRightDerivabilityStructure] :
+ instance [π.CommShift M] [H.ShiftSequence M] : (π ⋙ H).ShiftSequence M
+ instance [∀ (F : C₁ ⥤ D), T.HasRightKanExtension F]
+ instance {A B : CochainComplex.Plus C} (i : A ⟶ B) [Cofibration i] :
+ instance {A B : t.Heart} (f : A ⟶ B) [Mono f] (n : ℤ) :
+ instance {A B X Y : CategoryWithSmithStructure hIW₁ hIW₃}
+ instance {C : Type u} [Category.{v} C] (r : HomRel C) [LocallySmall.{w} C] :
+ instance {C D E : Type*} [Category C] [Category D] [Category E] (G : D ⥤ E)
+ instance {C ι : Type*} [Category C] [HasZeroMorphisms C]
+ instance {D : Type*} [Category D] (F : D ⥤ C) [F.IsEquivalence]
+ instance {D : Type*} [Category D] (L : CofibrantObject C ⥤ D)
+ instance {D : Type*} [Category D] (L : C₁ᵒᵖ × C₂ᵒᵖ ⥤ D)
+ instance {D : Type*} [Category D] (L : FibrantObject C ⥤ D)
+ instance {D : Type*} [Category D] [HasZeroObject D] [Preadditive D]
+ instance {D : Type*} [Category* D] (L : C ⥤ D)
+ instance {E : Type*} [Category E] (F : D ⥤ E) [IsEquivalence F]
+ instance {F : C ⥤ D} [EssSurj F] : EssSurj F.op
+ instance {F : Cᵒᵖ ⥤ Dᵒᵖ} [EssSurj F] : EssSurj F.unop
+ instance {F : Cᵒᵖ ⥤ Dᵒᵖ} [Faithful F] : Faithful F.unop
+ instance {F : Cᵒᵖ ⥤ Dᵒᵖ} [Full F] : Full F.unop
+ instance {F : Cᵒᵖ ⥤ Dᵒᵖ} [IsEquivalence F] : IsEquivalence F.unop
+ instance {I : Type*} (i : I) [HasZeroMorphisms C] :
+ instance {I : Type*} (i : I) [Preadditive C] :
+ instance {I : Type*} {F G : Discrete I ⥤ C} (f : ∀ i, F.obj i ⟶ G.obj i)
+ instance {I J : Type*} (p : I → J)
+ instance {K₁ K₂ L₁ : CochainComplex C ℤ} (f : K₁ ⟶ K₂) (i : K₁ ⟶ L₁) [Mono i] [QuasiIso i] :
+ instance {R : Type _} [Ring R] [CategoryTheory.Linear R C] (n : ℤ) :
+ instance {X Y : BifibrantObject C} (f : X ⟶ Y) [hf : WeakEquivalence f] :
+ instance {X Y : CochainComplex.Minus C} (p : X ⟶ Y) [Fibration p] :
+ instance {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) [WeakEquivalence f] :
+ instance {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) :
+ instance {X₂ Y₂ : C₂} (f : X₂ ⟶ Y₂) :
+ instance {Y' : C} (f : X ⟶ Y) (g : Y' ⟶ Y) [hf : AdmissibleMono f] [AdmissibleEpi g] :
+ instance {i j : WithBot (α n)} (f : i ⟶ j) :
+ instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
+ instance {β : Type*} (g : β → C) [HasCoproduct g] [∀ b, Projective (g b)] : Projective (∐ g)
+ instance {ι : Type*} (c : ComplexShape ι) [P.IsClosedUnderIsomorphisms] :
+ inv'_ι
+ inv_ι
+ inverseImage_eq
+ inverseImage_quasiIso_mapCochainComplexMinus_projectivesι
+ inverseImage_quasiIso_mapCochainComplexPlus_injectivesι
+ inverseImage_trW_iff
+ inverseImage_trW_isInverted
+ inverseObj
+ inverseSystem
+ inverseSystemI
+ inverts_iff_factors
+ isBilimitBiconeOfColimitCocone
+ isBilimitBiconeOfLimitCone
+ isCofibrant_iff
+ isColimit
+ isColimitBinaryCofanOfIsColimitCofanOption
+ isColimitCc
+ isColimitCocone
+ isColimitCoconeStupidFiltrationGE
+ isColimitCofanOfIsZero
+ isColimitCofanOfIsZeroButOne
+ isColimitCofanSingleColumnObjTotal
+ isColimitCofanSingleRowObjTotal
+ isColimitCokernelCofork
+ isColimitCokernelCoforkOfDistTriang
+ isColimitColimitCocone
+ isColimitFiltrationLECocone
+ isColimitMapCoconeOfCokernelCoforkOfπKernelConditionOfEpi
+ isColimitOfExactShortComplex
+ isColimitOfIsEventuallyConstant
+ isColimitSplitShortExactPushoutCocone
+ isColimit_cokernelCofork_of_shortExact
+ isConnected_leftResolution
+ isConnected_leftResolution_of_functorial_resolutions
+ isEmpty_index
+ isEquivalenceFullSubcategoryLift
+ isEventuallyConstantTo_inverseSystemI_comp_eval
+ isFibrant_iff
+ isGE_cokernel
+ 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_of_iso
+ isGE_iff_orthogonal
+ isGE_obj
+ isGE_of_isZero
+ isGE_succ_iff_isGE_and_isZero_homology
+ isGE_truncGE_obj
+ isGE_truncGT_obj
+ isGE₁_iff_isGE₀_and_isZero_homology₀
+ isGE₂
+ isInvertedBy₁
+ isInvertedBy₂
+ isInverted₁_of_precompLocalizerMorphismsInverts
+ isInverted₂_of_precompLocalizerMorphismsInverts
+ 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_app_app_iff_of_iso
+ isIso_app_app_of_isRightDerivedBifunctor
+ isIso_app_of_isRightDerivedFunctor
+ isIso_counit_app_app_of_kFlat_left
+ isIso_counit_app_app_of_kFlat_right
+ isIso_descExtend_f_iff
+ isIso_descOpcycles
+ isIso_eTruncGEIsoGEGE
+ isIso_eTruncGE_obj_map_truncGEπ_app
+ isIso_eTruncLTLTIsoLT
+ isIso_eTruncLT_obj_map_truncLTπ_app
+ isIso_filtation_map_of_isIso_filtrationι
+ isIso_filtration_map
+ isIso_filtration_map'_iff
+ isIso_filtration_map_comp_iff
+ isIso_filtration_map_from_pred'_iff
+ isIso_filtration_map_from_pred_iff
+ isIso_filtration_map_iff
+ isIso_filtrationι_iff
+ isIso_filtrationι_of_GE
+ isIso_filtrationι_of_collapsesAsSESAt
+ isIso_filtrationι_of_isZero
+ isIso_fromNext_φ_f
+ isIso_fromOpcycles
+ isIso_hom_of_GE
+ isIso_hom_succ
+ isIso_homologyFunctor_map_mor₂_of_isGE
+ isIso_homologyFunctor_map_truncGEπ_app
+ isIso_homologyFunctor_map_truncLEι_app
+ isIso_homologyFunctor_map_truncLTι_app
+ isIso_homologyMap_fromOfShortComplex
+ isIso_homologyMap_i
+ isIso_homologyMap_i'
+ isIso_homologyMap_iff'
+ isIso_homologyMap_mor₁_iff
+ isIso_homologyMap_mor₂_iff
+ isIso_homologyMap_of_isIso_cyclesMap_of_epi
+ isIso_homologyMap_of_isIso_opcyclesMap_of_mono
+ isIso_homologyMap_p
+ isIso_homologyMap_τ₁
+ isIso_homologyMap_τ₂
+ isIso_homology₀_iff_isIso_truncGE₀LE₀_map
+ isIso_homology₀_iff_isIso_truncLE₀GE₀_map
+ isIso_iff_bijective
+ isIso_iff_of_arrow_iso
+ isIso_iff_of_arrow_mk_iso
+ isIso_inverseSystemI_map
+ isIso_inverseSystemI_map'
+ isIso_inverseSystemI_map_succ
+ isIso_leftDerivedFunctor_counit_iff_inverts
+ isIso_liftCycles
+ isIso_limit_π_of_isEventuallyConstantTo
+ isIso_mapMap_apply
+ isIso_mapPageInfinity_of_isIso_hom
+ isIso_mapStupidTruncGE_f
+ isIso_natTransOfIsRightDerivedFunctorComp_app
+ isIso_of_isLeftDerivedFunctor
+ isIso_of_isRightDerivedFunctor
+ isIso_quotient_map_iff_homotopyEquivalences
+ isIso_ranBaseChange_app
+ isIso_ranBaseChange_app_iff
+ isIso_rightDerivedFunctorPlusCompNatTrans
+ isIso_rightDerivedFunctorPlusCompNatTrans'
+ isIso_rightDerivedFunctorPlusCompNatTrans_app
+ isIso_rightDerivedFunctorPlusUnit_app
+ isIso_rightDerivedFunctorPlusUnit_app_of_bounded
+ isIso_rightDerivedFunctor_unit_iff_inverts
+ isIso_rightDerivedNatTrans₁
+ isIso_rightDerivedNatTrans₂
+ isIso_stupidFiltrationGE_map_f
+ isIso_toCycles
+ isIso_toHomotopyCategory_map_iff
+ 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_whiskerLeft_ιHeart_truncGEπ
+ isIso_whiskerLeft_ιHeart_truncLEι
+ isIso_whiskerRight_truncGEπ_homologyFunctor
+ isIso_whiskerRight_truncLEι_homologyFunctor
+ isIso_ιStupidTrunc_iff
+ isIso_πStupidTrunc_iff
+ isIso_π_f
+ isIso_π_f_of_isLimit_of_isEventuallyConstantTo
+ isIso_π_iff
+ isIso_π_iff'
+ isIso_π_of_collapsesAsSESAt
+ isIso_π_of_isZero
+ isIso₁_of_convergesInDegree
+ isIso₁_truncLE_map_of_isGE
+ isIso₁_truncLT_map_of_isGE
+ isIso₂_of_convergesInDegree
+ 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_of_iso
+ isLE_iff_orthogonal
+ isLE_obj
+ isLE_of_isZero
+ isLE_truncLE_obj
+ isLE_truncLT_obj
+ isLE₂
+ isLeftDerivabilityStructure
+ isLeftDerivabilityStructure_iff_of_equivalences
+ isLeftDerivabilityStructure_of_equivalences
+ isLeftDerivabilityStructure_of_functorial_resolutions
+ isLeftDerivabilityStructure_of_isLocalizedEquivalence
+ isLeftDerivedFunctor_bifunctorCounit₁_kFlat
+ isLeftDerivedFunctor_bifunctorCounit₂_kFlat
+ isLeftDerivedFunctor_iff_isIso
+ isLeftDerivedFunctor_iff_op
+ isLeftDerivedFunctor_of_isIso
+ isLeftDerivedFunctor_of_isLeftDerivabilityStructure
+ isLeftDerivedFunctor₂_of_isLeftDerivabilityStructure
+ isLeftDerivedFunctor₃_of_isLeftDerivabilityStructure
+ isLeftDerivedFunctor₄_of_isLeftDerivabilityStructure
+ isLeftKanExtension_iff_of_iso₃
+ isLeftKanExtension_iff_op
+ isLeftKanExtension_iff_postcomp₂
+ isLeftLocalizing_of_op
+ isLimitFanOfEquiv
+ isLimitKernelFork
+ isLimitKernelForkOfDistTriang
+ isLimitKf
+ isLimitMapConeOfKernelForkOfιCokernelConditionOfMono
+ isLimit_kernelFork_of_shortExact
+ isLimit_of_isPushout_of_injective
+ isLocalization_functor
+ isLocalization_of_essSurj_of_full_of_exists_cylinders
+ isLocalization_of_isLeftLocalizing
+ isLocalization_of_isRightLocalizing
+ isLocalizedEquivalence_of_functorial_left_resolutions
+ isLocalizedEquivalence_of_isInduced
+ isLocalizedEquivalence_of_isLocalization
+ isLocalizedEquivalence_of_iso
+ isLocalizedEquivalence_of_precomp
+ isLocalizedEquivalence_op_iff
+ isLocalizerEquivalence
+ isPointwiseRightKanExtensionAtCompTwoSquareEquiv
+ isPointwiseRightKanExtensionEquivOfGuitartExact
+ isPointwiseRightKanExtensionOfCompTwoSquare
+ isPushout
+ isPushout_of_isPullback_of_epi
+ isRightDerivabilityStructure
+ isRightDerivabilityStructure_iff_of_equivalences
+ isRightDerivabilityStructure_iff_op
+ isRightDerivabilityStructure_of_isLocalizedEquivalence
+ isRightDerivedFunctor_iff_of_isLocalization
+ isRightDerivedFunctor_iff_op
+ isRightDerivedFunctor_iff_postcomp
+ isRightDerivedFunctor_iff_precomp
+ isRightDerivedFunctor_of_isLocalization
+ isRightDerivedFunctor_of_isRightDerivabilityStructure
+ isRightDerivedFunctor_of_iso₂
+ isRightDerivedFunctor_postcomp
+ isRightDerivedFunctor₁_of_isRightDerivedBifunctor
+ isRightDerivedFunctor₂_of_isRightDerivedBifunctor
+ isRightKanExtension_iff_of_iso₃
+ isRightKanExtension_iff_op
+ isStableUnderColimitsOfShape_preservesQuasiIso
+ isStableUnderColimitsOfShape_quasiIso
+ isTriangulated_lift
+ isUniversalOfPointwise
+ isZero'
+ 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_X
+ isZero_Z_X_of_ge
+ isZero_Z_X_of_le
+ isZero_cycles
+ isZero_eTruncGE_obj_obj
+ isZero_eTruncLT_obj_obj
+ isZero_filtration_obj_iff
+ isZero_filtration_obj_none
+ isZero_filtration_obj_of_LE
+ isZero_homology_I
+ isZero_homology_ZToX₁
+ isZero_homology_of_isZero
+ isZero_homology₀_of_isGE_one
+ isZero_homology₀_of_isLE_neg_one
+ isZero_of_collapsesAt
+ isZero_of_isIso_filtration_map
+ isZero_opcycles
+ isZero_shift_obj_of_vanishesOnGEOne
+ isZero_shift_obj_of_vanishesOnLESubOne
+ isZero_singleColumn_X
+ isZero_singleColumn_X_X
+ isZero_singleRow_X_X
+ isZero_spectralSequence_page_X_iff
+ isZero_spectralSequence_page_X_of_isZero_H
+ isZero_spectralSequence_page_X_of_isZero_H'
+ isZero_stupidTrunc
+ isZero_stupidTrunc_iff
+ isZero_truncGE_obj_of_isLE
+ isZero_truncLE_obj_of_isGE
+ isZero_truncLT_obj_of_isGE
+ isZero₁_of_convergesInDegree
+ isZero₁_of_isFirstQuadrant
+ isZero₁_of_isThirdQuadrant
+ isZero₂_of_convergesInDegree
+ isZero₂_of_isFirstQuadrant
+ isZero₂_of_isThirdQuadrant
+ iso'
+ isoAdd'_iso₁_iso₂
+ isoBiprod
+ isoBiprod_hom_fst
+ isoBiprod_hom_snd
+ isoBiprod_inv_fst
+ isoBiprod_inv_snd
+ isoBot
+ isoEMapFourδ₁Toδ₀'
+ isoEMapFourδ₁Toδ₀'_hom_inv_id
+ isoEMapFourδ₁Toδ₀'_inv_hom_id
+ isoEMapFourδ₄Toδ₃'
+ isoEMapFourδ₄Toδ₄'_hom_inv_id
+ isoEMapFourδ₄Toδ₄'_inv_hom_id
+ isoFiltrationMap
+ isoFiltrationMap_hom_inv_id
+ isoFiltrationMap_inv_hom_id
+ isoFiltrationι
+ isoFiltrationι_hom_inv_id
+ isoFiltrationι_inv_hom_id
+ isoImageOfFac
+ isoOfArrow₂Iso
+ isoOfCollapsesAt
+ isoSingle
+ iso_hom_app
+ iso_hom_comp_edgeMonoStep
+ isomorphisms_isInvertedBy
+ isoπ
+ isoπ_hom_inv_id
+ isoπ_inv_hom_id
+ iso₀
+ iso₁_add
+ iso₁_hom_app
+ iso₁_hom_app_app
+ iso₁_zero
+ iso₂_add
+ iso₂_hom_app
+ iso₂_hom_app_app
+ iso₂_zero
+ iso₃
+ i₀_le
+ i₃_le
+ jointlyReflectEpimorphisms
+ jointlyReflectMonomorphisms
+ kFlat
+ kFlat.whiskerLeft
+ kFlat.whiskerRight
+ kFlatResolutionFunctor
+ kFlatResolutionNatTrans
+ kFlat_biprod
+ kFlat_cylinder
+ kFlat_derivesMonoidal
+ kFlat_iff_preserves_acyclic
+ kFlat_of_bounded_of_flat
+ kFlat_of_isStrictlyLE_of_flat
+ kFlat_prod
+ kFlat_prod_id_derives_curriedTensor
+ kFlat_quotient_obj_iff
+ kFlat_resolutionFunctor_obj
+ kFlat_shift_iff
+ kFlat_single_obj_iff_flat
+ kernelSequenceCycles
+ kernelSequenceCyclesE
+ kernelSequenceCyclesE_exact
+ kernelSequenceCycles_exact
+ kernelSequenceE
+ kernelSequenceE_exact
+ kernelSequenceOpcycles
+ kernelSequenceOpcyclesE
+ kernelSequenceOpcyclesEIso
+ kernelSequenceOpcyclesE_exact
+ kernelSequenceOpcycles_exact
+ kf
+ kfSc
+ kfSc_exact
+ kf_w
+ largeExtClass
+ le_pred'_of_lt
+ leftDerivedCounit₂
+ leftDerivedCounit₃
+ leftDerivedCounit₄
+ leftDerivedFunctor₃Unique
+ leftDerived₂
+ leftDerived₂Lift
+ leftDerived₂_ext
+ leftDerived₂_fac
+ leftDerived₂_fac_app_app
+ leftDerived₃
+ leftDerived₃Lift
+ leftDerived₃NatIso
+ leftDerived₃NatTrans
+ leftDerived₃NatTrans_comp
+ leftDerived₃NatTrans_fac
+ leftDerived₃NatTrans_fac_app_app_app
+ leftDerived₃NatTrans_id
+ leftDerived₃_ext
+ leftDerived₃_fac
+ leftDerived₃_fac_app_app
+ leftDerived₄
+ leftDerived₄Lift
+ leftDerived₄_ext
+ leftDerived₄_fac
+ leftDerived₄_fac_app_app
+ leftExtensionOpEquivalence
+ leftHomologyData
+ leftHomologyDataShortComplexE
+ leftHomologyDataShortComplexE_f'
+ leftHomologyData_f'
+ leftHomologyData_i_edgeEpiStep_compatibility
+ leftHomologyData_π_edgeMonoStep_compatibility
+ leftHomologyIso
+ leftHomologyIso'
+ leftHomologyMapData
+ leftHomotopyClassToHom
+ leftHomotopyClassToHom_mk
+ leftResolution
+ leftResolutionComparison
+ leftResolutionπ
+ leftUnitor_eq
+ leftcomp
+ lemma_1_8
+ lemma_1_8'
+ le₀'₀
+ le₀_of_hasEdgeEpiAt
+ le₀_of_hasEdgeEpiAtFrom
+ le₀_of_hasEdgeMonoAt
+ le₀_of_hasEdgeMonoAtFrom
+ le₀_stationaryPage
+ le₀₁'
+ le₁₂'
+ le₂₃'
+ le₃₃'
+ liftCycles
+ liftCycles_comp_homologyπ_eq_iff_up_to_refinements
+ liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements
+ liftCycles_i
+ liftE
+ liftE_ιE_fromOpcycles
+ liftFunctorCompIso
+ liftFunctorObjectProperty
+ liftHeart
+ liftHeartιHeart
+ liftObjectProperty
+ liftOpcycles
+ liftOpcycles_fromOpcycles
+ liftTruncLE
+ liftTruncLE_aux
+ liftTruncLE_ι
+ liftTruncLT
+ liftTruncLT_aux
+ liftTruncLT_ι
+ lift_π₀
+ lift_π₁
+ lifting
+ lift₂
+ llp_ofHoms_iff_hasLiftingProperty
+ llp_rlp_J
+ localizerMorphismKFlat
+ localizerMorphismOfIsCompatibleWithShift
+ localizerMorphism_derives
+ locallySmall_of_isLocalization
+ lowDegreesComposableArrows
+ lowDegreesComposableArrows_exact
+ lt_iff_le_pred'
+ lt_of_collapsesAsSESAt
+ mapArrowHom
+ mapArrowHom_comp
+ mapArrowHom_id
+ mapArrowIso
+ mapBifunctorMapIso
+ mapBifunctorMap_inr_mapBifunctorMappingCone₁Iso_hom
+ mapBifunctorMap_inr_mapBifunctorMappingCone₂Iso_hom
+ mapBifunctorMap_map_add₁
+ mapBifunctorMap_map_add₂
+ mapBifunctorMappingCone₁Iso
+ mapBifunctorMappingCone₂Iso
+ mapBifunctorShift₁Iso_hom_naturality₂
+ mapBifunctorShift₂Iso_hom_naturality₁
+ mapBifunctorSingle₁Iso
+ mapBifunctorSingle₁Iso_hom_naturality
+ mapBifunctorSingle₁Iso_inv_naturality
+ mapBifunctorSingle₁XIso
+ mapBifunctorSingle₂Iso
+ mapBifunctorSingle₂Iso_hom_naturality
+ mapBifunctorSingle₂Iso_inv_naturality
+ mapCochainComplexMinus
+ mapCochainComplexMinusCompι
+ mapCochainComplexPlus
+ mapCochainComplexPlusCompι
+ mapExtendFunctorNatIso
+ mapExtendIso
+ mapExtendX
+ mapExtendX_hom_eq
+ mapExtensIso_hom_f_naturality
+ mapFiltrationLEMinus
+ mapFiltrationLEMinus_app_hom
+ mapHeartShortExactTriangle
+ mapHomologicalComplexCompShortComplexFunctorIso
+ mapHomologicalComplexHomologyIso
+ mapHomologicalComplexObjDoubleIso
+ mapHomologicalComplexObjDoubleXIso
+ mapHomologicalComplexObjIso_hom_map_π₀
+ mapHomologicalComplexObjIso_hom_map_π₁
+ mapHomologicalComplexObjXIso
+ mapHomologicalComplex₂
+ mapHomologicalComplex₂_d₁
+ mapHomologicalComplex₂_d₂
+ mapHomologicalFunctor
+ mapHomologicalFunctor_δ
+ mapHomotopyCategoryMinus
+ mapHomotopyCategoryMinusCompIso
+ mapHomotopyCategoryPlus
+ mapHomotopyCategoryPlusCompIso
+ mapMap_add
+ mapMap_zero
+ mapPageInfinity
+ mapPageInfinity_eq
+ mapShortComplex
+ mapShortComplexSplitting
+ mapShortComplexStupidFiltrationGE
+ mapStupidTruncGE_fac
+ mapStupidTruncGE_naturality
+ mapStupidTruncGE_refl
+ mapStupidTruncGE_trans
+ mapStupidTruncLE_fac
+ mapStupidTruncLE_naturality
+ mapStupidTruncLE_refl
+ mapStupidTruncLE_trans
+ mapTotalIso
+ mapTotalIso_hom_naturality
+ mapTotalIso_inv_naturality
+ mapTotalXIso
+ mapTotalXIso_hom_naturality
+ mapTriangle
+ mapWithBot
+ mapWithBotFunctor
+ mapWithBot_bot
+ mapWithBot_monotone
+ mapWithBot_none
+ mapWithBot_pred_le_i₂
+ mapWithBot_some
+ mapWithBot_some'
+ map_distinguished_op_exact
+ map_eq_of_le₂
+ map_inrX_mapHomologicalComplexObjXIso_hom
+ map_objι
+ map_of_hom
+ map_refl
+ map_shiftIso_inv_app
+ map_surjective_of_isLocalization
+ map_trans
+ map_ι_mapTotalXIso_inv
+ map_ι₀_mapHomologicalComplexObjIso_hom
+ map_ι₁_mapHomologicalComplexObjIso_hom
+ mappingCocone
+ map₂CochainComplexFlipObjMapMappingConeTriangleIso
+ map₂CochainComplexFlipObjShiftIso
+ map₂CochainComplexObjShiftIso
+ map₂CochainComplex_flip_obj_commShiftIso_hom_app
+ map₂CochainComplex_flip_obj_commShiftIso_inv_app
+ map₂CochainComplex_obj_commShiftIso_hom_app
+ map₂CochainComplex_obj_commShiftIso_inv_app
+ map₂HomologicalComplexFlipObjSingleIso
+ map₂HomologicalComplexObjSingleIso
+ mem_essImage_ιHeart_iff
+ mem_hasEdgeEpiSet
+ mem_hasEdgeMonoSet
+ mem_heart_iff
+ mem_of_hasInductedTStructure
+ mem_quasiIso_iff
+ mem_spectralSequence_hasEdgeEpiSet
+ mem_spectralSequence_hasEdgeMonoSet
+ mem_subcategory_of_strictly_bounded
+ mem_tStructure_heart_iff
+ minusResolutionFunctor
+ minusResolutionNatTrans
+ mk''
+ mkDataE₂Cohomological
+ mkDataE₂CohomologicalCompatibility
+ mkDataE₂CohomologicalFin
+ mkDataE₂CohomologicalNat
+ mkDataE₂CohomologicalNatCompatibility
+ mkDataE₂Cohomological_i₁_eq_i₂
+ mkDataE₂HomologicalNat
+ mkDataE₂HomologicalNatCompatibility
+ mkOfArrow₂Iso
+ mkProd
+ mk_prod
+ mk₃fac
+ mono
+ monoUpTo
+ monoWithProjectiveCokernel
+ monoWithProjectiveCokernel_eq_unop
+ monoWithProjectiveCokernel_iff_of_isZero
+ mono_EMap
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ mono_cokerToKer'
+ mono_cyclesMap_π'
+ mono_d
+ mono_descExtend_f_iff
+ mono_homologyFunctor_map_mor₂
+ mono_homologyMap_iff'
+ mono_homologyMap_iff_up_to_refinements
+ mono_homologyMap_p
+ mono_homologyMap_π'
+ mono_homologyMap_τ₁
+ mono_homologyMap_τ₂
+ mono_homologyMap₀_doubleFunctor_map_arrowHomToG_iff
+ mono_homologyShortComplex'_f
+ mono_homologyShortComplex_f
+ mono_iff_injective
+ mono_iff_of_addEquiv
+ mono_iff_ulift
+ mono_of_isZero_kernel
+ mono_of_isZero_kernel'
+ mono_ιK
+ monomorphisms_stableUnderCobaseChange
+ monotone_cochainComplexMinus
+ monotone_homologicalComplex
+ monotone_i₃'
+ morphismProperty
+ morphismProperty_le
+ mor₁_πQ
+ natIsoLift₃
+ natTransCommshift_of_fac
+ natTransConcat
+ natTransConcat₃
+ natTransLift₃
+ natTransLift₃_app_app_app
+ natTransOfIsRightDerivedFunctorComp
+ 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
+ natTrans_app_op_shift
+ natTrans_commShift
+ natTrans₁₂
+ natTrans₁₅
+ natTrans₂₃
+ natTrans₃₄
+ natTrans₅₄
+ neg_apply
+ next
+ nonempty_factorization
+ nonempty_hasEdgeEpiSet
+ nonempty_hasEdgeMonoSet
+ nonempty_hom_of_connected_groupoid
+ nonempty_isColimit_iff_preadditiveYoneda
+ nonempty_isLimit_iff_preadditiveCoyoneda
+ nonempty_isPointwiseRightKanExtensionAt_compTwoSquare_iff
+ nonempty_stationarySet
+ obj
+ objIso₁
+ objIso₁_inv_objι
+ objIso₂
+ objIso₂_inv_map
+ objectPropertyColimitOfShapeLeftResolutionObj
+ objectPropertyColimitOfShape_leftResolution_obj
+ objectPropertyFlat_iff_moduleFlat
+ objectPropertyFlat_iff_preservesFiniteLimits_tensorLeft
+ objι
+ obj₀
+ obj₁
+ obj₂
+ ofAbelian
+ ofBifunctor
+ ofComplexSc'Iso
+ ofComplexXIso
+ ofNatTrans
+ of_biprod
+ of_coprod_inr_with_id
+ of_eq_of_iso
+ of_eq_zero_of_isZero
+ of_hComp
+ of_hComp'
+ of_hasBinaryBiproduct_fst_snd
+ of_isIso_app_functor_obj
+ of_isIso_app_functor_obj'
+ of_localization_comparison
+ of_zero
+ onBounded
+ onMinus
+ onPlus
+ opCoproductTriangleIsoProductTriangle
+ opEquiv
+ opEquivalence
+ opFunctor
+ opMap
+ opMap_id
+ opShiftFunctorEquivalence_inv_app_shift
+ opShiftFunctorEquivalence_symm_homEquiv
+ opShiftFunctorEquivalence_symm_homEquiv_apply
+ opShiftFunctorEquivalence_symm_homEquiv_left_inv
+ opUnop
+ opcycles
+ opcyclesIso
+ opcyclesIsoH
+ opcyclesIsoH_hom
+ opcyclesIsoH_hom_inv_id
+ opcyclesIsoH_inv_hom_id
+ opcyclesIsoKernel
+ opcyclesIsoKernel_hom_fac
+ opcyclesIsoSc'_eq_rfl
+ opcyclesIso_hom_δFromOpcycles
+ opcyclesMap
+ opcyclesMap_comp
+ opcyclesMap_fromOpcycles
+ opcyclesMap_id
+ opcyclesMap_opcyclesIso_hom
+ opcyclesMap_threeδ₂Toδ₁_opcyclesToE
+ opcyclesToCycles
+ opcyclesToCycles_fac
+ opcyclesToE
+ opcyclesToE_EMap
+ opcyclesToE_ιE
+ overMapPullback_map_overPullback_map
+ overPullback_map_sheafHomSectionsEquiv_apply
+ over_forget_coverLifting
+ p'
+ p'_zero
+ 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
+ pageInfinityIso'
+ pageInfinityIso_hom_edgeEpiStep
+ pageInfinityIso_hom_edgeEpiSteps
+ pageInfinityIso_hom_edgeMonoStep
+ pageInfinityIso_hom_edgeMonoStep'
+ pageInfinityIso_hom_edgeMonoSteps
+ pageInfinityIso_hom_edgeMonoSteps'
+ pageInfinityι
+ pageInfinityι_π
+ pageInfinityι_π_eq_zero
+ pageInfinityπ
+ pageInfinityπ_ι
+ pageX
+ pageXIso
+ pageXIsoOfEq
+ page₂Iso
+ pathObject
+ pentagon_curriedAssociatorNatIso_hom
+ postcomp_shiftIso_hom_app'
+ postcomp_shiftIso_inv_app'
+ postcomposeShiftNatTrans
+ precompLocalizerMorphismsInverts_iff
+ precomposeShiftNatTrans
+ pred'
+ pred'_bot
+ pred'_le
+ pred'_monotone
+ pred'_some
+ pred_injective
+ pred_le
+ pred_monotone
+ preimageNatIso
+ preimageNatTrans
+ preimageNatTrans_comp
+ preimageNatTrans_id
+ preserves
+ preservesColimitOfIsZero
+ preservesColimitsOfShapeOfIsZero
+ preservesLimitsOfShapeOfIsZero
+ preservesQuasiIso_iff_of_factors
+ preservesQuasiIso_iff_preserves_acyclic
+ preservesQuasiIso_mapHomologicalComplex
+ preservesQuasiIso_mapHomologicalComplex_iff
+ preservesQuasiIso_mapHomotopyCategory_iff
+ preservesQuasiIso_shiftFunctor
+ preservesTotal_of_isStrictlyLE
+ preservesZeroMorphisms_of_fac_of_essSurj
+ preservesZeroMorphisms_of_preserves_terminal_object'
+ preserves_shortComplexQuasiIso
+ prod'
+ prod_isInvertedBy_iff
+ prod_mem_heart
+ productIsoOfEquiv
+ productOptionIso
+ prop_biprod_of_isClosedUnderBinaryProducts
+ prop_hom
+ prop_map_obj_iff
+ prop_pi
+ prop_succ_hom
+ pushout
+ pushouts_coproducts_ιSuccObj
+ quadrifunctorLeft
+ quadrifunctorRight
+ quadrifunctorRightCounit
+ quadrifunctorRightCounit_app_app_app_app
+ quarrable
+ quarrable.hasPullback
+ quarrable.hasPullback'
+ quarrable.op
+ quarrable.unop
+ quasiIsoAt_i'
+ quasiIsoAt_limit_π_of_isEventuallyConstantTo
+ quasiIsoAt_of_quasiIsoLE
+ quasiIsoAt_opEquivalence_map_iff
+ quasiIsoAt_π_f
+ quasiIsoAt_π_of_isLimit_of_isEventuallyConstantTo
+ quasiIsoAt₀_doubleFunctor_map_arrowHomToG_iff
+ quasiIsoAt₁_doubleFunctor_map_arrowHomToG_iff
+ quasiIsoLE_cofFibFactorization
+ quasiIso_doubleFunctor_map_arrowHomToG_iff_exact
+ quasiIso_f_iff_of_shortExact
+ quasiIso_functorCategory_iff
+ quasiIso_hom
+ quasiIso_iff_acyclic
+ quasiIso_iff_acyclic'
+ quasiIso_iff_homotopyEquivalences_of_isKInjective
+ quasiIso_iff_homotopyEquivalences_of_isKProjective
+ quasiIso_inv
+ quasiIso_leftResolutionπ_app
+ quasiIso_minusResolutionFunctor_map
+ quasiIso_minusResolutionNatTrans_app
+ quasiIso_opEquivalence_map_iff
+ quasiIso_resolutionNatTrans_app
+ quasiIso_respectsIso
+ quasiIso_truncGEπ
+ quasiIso_τ₁
+ quasiIso_τ₂
+ quotient'
+ quotientCompBifunctorMapHomotopyFlipObjIso
+ quotientCompBifunctorMapHomotopyObjIso
+ quotient_additive
+ quotient_map_whiskerLeft
+ quotient_map_whiskerRight
+ rFromMin
+ rFromMin_LE
+ rFromMin_LE_rMin
+ rFromMin_mem
+ rMin
+ rToMin
+ rToMin_LE
+ rToMin_LE_rMin
+ rToMin_mem
+ ranBaseChange
+ refinementsTopology
+ refinementsTopology_eq_regularTopology
+ refinementsTopology_subcanonical
+ refl
+ reflectsExactSequencesOfPreservesZeroMorphismsOfFaithful
+ reflectsExactSequences_iff_reflectsShortComplexExact'
+ relations
+ resolutionFunctor
+ resolutionNatTrans
+ restrictionStupidTruncIso
+ restrictionStupidTruncIso_hom_naturality
+ restrictionStupidTruncIso_inv_naturality
+ restrictionStupidTruncNatIso
+ retract_of_isIdempotentComplete
+ rightDerived'
+ rightDerivedBifunctor
+ rightDerivedFunctorPlus
+ rightDerivedFunctorPlusCompNatTrans
+ rightDerivedFunctorPlusUnit
+ rightDerivedNatTrans₁
+ rightDerivedNatTrans₁_fac_app
+ rightDerivedNatTrans₂
+ rightDerivedNatTrans₂_fac_app
+ rightDerivedUnit
+ rightDerived_exact₁
+ rightDerived_exact₂
+ rightDerived_exact₃
+ rightDerivedδ
+ rightDerivedδ_comp
+ rightExtensionOpEquivalence
+ rightHomologyDataShortComplexE
+ rightHomologyDataShortComplexE_g'
+ rightHomologyData_p_edgeMonoStep_compatibility
+ rightHomologyData_ι_edgeEpiStep_compatibility
+ rightHomologyIso
+ rightHomologyIso'
+ rightHomotopyClassToHom
+ rightHomotopyClassToHom_mk
+ rightShift_comp
+ rightUnitor_eq
+ rlp_ofHoms_iff_hasLiftingProperty
+ rowFiltrationGE
+ rowFiltrationGEFunctor
+ rowFiltrationGEMap
+ sc₁
+ sc₂
+ sc₃
+ segment
+ segment'
+ sequence
+ sequenceFromNext
+ sequenceΨ
+ sequenceΨ_exact
+ sgn₁
+ sgn₁_rel₁
+ sgn₁_rel₂
+ sgn₂
+ sgn₂_mul_self
+ shape_from
+ shape_to
+ shiftFunctorAdd'_inv_app
+ shiftFunctorAdd'_prod
+ shiftFunctorAdd_prod
+ shiftFunctorZero'_eq_shiftFunctorZero
+ shiftFunctorZero_inv_app
+ shiftFunctorZero_prod
+ shiftFunctor_additive
+ shiftFunctor_map
+ shiftFunctor_map_f''
+ shiftFunctor_obj_d''
+ shiftFunctor_prod
+ shiftSpectralObjectω₁IsoHomologyιHeart
+ shiftTruncGE
+ shiftTruncGELE
+ shiftTruncLE
+ shiftTruncLE_hom_app_ι
+ shift_ι_map_ιK
+ shiftedHom
+ shortComplexE
+ shortComplexEMap
+ shortComplexEMap_comp
+ shortComplexEMap_id
+ shortComplexIso
+ shortComplexOfCollapses
+ shortComplexOfCollapsesIso
+ shortComplexOpcyclesThreeδ₂Toδ₁
+ shortComplexOpcyclesThreeδ₂Toδ₁_exact
+ shortComplexOpcyclesThreeδ₂Toδ₁_shortExact
+ shortComplexSplittingEquiv
+ shortComplexStupidFiltrationGE
+ shortComplexStupidFiltrationGESplitting
+ shortComplexStupidTrunc
+ shortComplexStupidTruncSplitting
+ shortComplexStupidTruncSplitting₁
+ shortComplexStupidTruncSplitting₂
+ shortComplexULiftIsoMk
+ shortComplex_f_fac
+ shortComplex_g_fac
+ shortComplex_shortExact
+ shortComplex₁Functor
+ shortComplex₂Functor
+ shortComplex₃
+ shortComplex₄Functor₁₂₃₄
+ shortComplex₄Functor₂₃₄₅
+ shortExact_of_admissibleEpi_of_isLimit
+ shortExact_of_admissibleMono_of_isColimit
+ shortExact_of_collapses
+ shortExact_of_distTriang
+ shortExact_of_isIso_of_isZero
+ shortExact_of_isZero
+ shortExact_of_isZero_of_isIso
+ sigmaDesc
+ sigmaMap
+ sigmaSrc
+ sigmaTgt
+ singleColumn
+ singleColumnObjTotal
+ singleColumnObjTotalXIso
+ singleColumnObjTotalXIso_inv
+ singleColumnObjTotal_hom_naturality
+ singleColumnObjTotal_inv_naturality
+ singleColumnXIso
+ singleColumnXXIso
+ singleColumn_d₁
+ singleColumn_d₂
+ singleColumn_obj_X_d
+ singleColumn_ιTotal
+ singleFunctor_obj_mem_heart
+ singleFunctor_preimage
+ singleFunctors_shiftIso_hom_app_f
+ singleFunctors_shiftIso_inv_app_f
+ singleRow
+ singleRowObjTotal
+ singleRowObjTotalXIso
+ singleRowObjTotalXIso_inv
+ singleRowObjTotal_hom_naturality
+ singleRowObjTotal_inv_naturality
+ singleRowXXIso
+ singleRow_d₁
+ singleRow_d₂
+ singleRow_obj_d_f
+ singleRow_ιTotal
+ singleRow₀ObjTotal
+ singleRow₀ObjTotal_hom_naturality
+ singleShiftIso
+ singleShiftIso_add'
+ singleShiftIso_add'_hom_app
+ singleShiftIso_add'_inv_app
+ singleShiftIso_hom_app
+ singleShiftIso_hom_app_f
+ singleShiftIso_hom_app_self
+ small_index
+ snd
+ solutionSetCondition
+ spectralObject
+ spectralObjectFunctor
+ spectralObjectMappingCone
+ spectralObject_δ
+ spectralSequenceE₂Iso
+ spectralSequenceFin
+ spectralSequenceFin_rel_iff
+ spectralSequenceFirstPageXIso
+ spectralSequenceFirstPageXIso_hom
+ spectralSequenceFirstPageXIso_inv
+ spectralSequenceHasEdgeEpiAt
+ spectralSequenceHasEdgeEpiAtFrom
+ spectralSequenceHasEdgeEpiAt_iff
+ spectralSequenceHasEdgeMonoAt
+ spectralSequenceHasEdgeMonoAtFrom
+ spectralSequenceHasEdgeMonoAt_iff
+ spectralSequenceHomologyData
+ spectralSequenceHomologyData_left_i
+ spectralSequenceHomologyData_right_homologyIso_eq_left_homologyIso
+ spectralSequenceHomologyData_right_p
+ spectralSequenceNatE₂Iso
+ spectralSequenceNatStronglyConvergesTo
+ spectralSequenceNat_rel_iff
+ spectralSequencePageInfinityIso
+ spectralSequencePageInfinityIso_hom
+ spectralSequencePageSc'Iso
+ spectralSequencePageXIso
+ spectralSequenceStronglyConvergesTo
+ spectralSequence_edgeEpiStep_compatibility
+ spectralSequence_edgeEpiSteps_compatibility
+ spectralSequence_edgeMonoStep_compatibility
+ spectralSequence_edgeMonoSteps_compatibility
+ spectralSequence_first_page_d_eq
+ spectralSequence_iso
+ spectralSequence_page_d_eq
+ spectralSequence_page_d_eq_zero_iff_isIso₁
+ spectralSequence_page_d_eq_zero_iff_isIso₂
+ spectralSequence_page_d_eq_zero_of_isZero₁
+ spectralSequence_page_d_eq_zero_of_isZero₂
+ splitExactSequences
+ splitShortExact
+ splitShortExactPushoutCocone
+ splitShortExact_op
+ splitShortExact_unop
+ src
+ stationaryPage
+ stationaryPage_isZero₀
+ stationaryPage_isZero₃
+ stationarySet
+ step'
+ step₁
+ step₁₂
+ step₂
+ strictUniversalPropertyFixedTarget
+ strictUniversalPropertyFixedTargetToHoCat
+ stripe_eq
+ stripes
+ stripes.position_eq_iff
+ stronglyConvergesTo
+ stronglyConvergesToInDegree'
+ stupidFiltrationGE
+ stupidFiltrationGEFunctor
+ stupidFiltrationGEObjToSingle
+ stupidFiltrationGE_map_to_single
+ stupidTruncGEFiltration
+ stupidTruncLEFiltration
+ stupidTruncRetract
+ sub
+ sub'
+ sub_antitone
+ sub_bot
+ sub_eq_self_iff
+ sub_injective
+ sub_le_self
+ sub_liftCycles
+ sub_one
+ sub_sub
+ sub_succ
+ sub_succ_lt
+ sub_zero
+ succ
+ succObj
+ succStruct
+ succStruct_prop_le_inverseImage_rlp_llp_inter
+ tBounded
+ tMinus
+ tPlus
+ tStructure
+ tStructure_isGE_iff
+ tStructure_isLE_iff
+ tautological_sequence
+ tensorLeft
+ tensorObj_eq
+ tensorRight
+ tensorUnitLeftCounit
+ tensorUnitLeftCounit_app
+ tensorUnitRightCounit
+ tensorUnitRightCounit_app
+ terminalCone
+ terminalConeLimit
+ tgt
+ toCycles
+ toCycles_cyclesMap
+ toCycles_descCycles
+ toCycles_i
+ toCycles_Ψ
+ toCycles_πE_d
+ toCycles_πE_descE
+ toDerivedMonoidal
+ toE₂ZeroOne
+ toHoCat
+ toHoCatCompιCofibrantObject
+ toHoCatCompιFibrantObject
+ toHoCat_map_eq
+ toHoCat_map_eq_iff
+ toHoCat_obj_surjective
+ toHomology₀
+ toHomology₀_naturality
+ toHomotopyCategory
+ toHomotopyCategory_obj
+ toImageOfFac
+ toImageOfFac_fac
+ toImageOfFac_ι
+ toSingleEquiv
+ toSucc
+ toWhiskeringLeft₂Eval₂
+ to_break
+ to_truncLE_obj_ext
+ to_truncLT_obj_ext
+ tor
+ total.isIso_ιStupidTrunc_map_f
+ total.mapShortComplex
+ total.quasiIsoAt_ιStupidTrunc_map
+ total.quasiIso_map_of_finitely_many_columns
+ total.quasiIso_map_of_isStrictlyGE_of_isStrictlyLE
+ total.shortComplex
+ total.shortComplexSplitting
+ totalπ
+ totalπ'
+ totalπ'_naturality
+ trW_iff_of_distinguished'
+ trW_of_op
+ trW_of_unop
+ trW_op
+ trW_op_iff
+ trans
+ transfiniteCompositionOfShapeSigmaMap
+ triangleFunctorNatTransOfLE
+ triangleFunctorNatTransOfLE_app_hom₂
+ triangleFunctorNatTransOfLE_refl
+ triangleFunctorNatTransOfLE_trans
+ triangleGELEIso_aux
+ triangleIso
+ triangleLEGE
+ triangleLEGEIso
+ triangleLEGEIsoTriangleLTGE
+ triangleLEGE_distinguished
+ triangleLEGT
+ triangleLEGTIsoTriangleLEGE
+ triangleLEGT_distinguished
+ triangleLTLTGELT
+ triangleLTLTGELT_distinguished
+ triangleMapOfLE
+ triangleOpEquivalenceFunctorCompMapTriangleIso
+ triangleOpEquivalenceFunctorCompMapTriangleIso_aux
+ trianglehOfDegreewiseSplit_distinguished
+ triangleδ
+ triangleω₁δ
+ triangleω₁δObjIso
+ triangleω₁δ_distinguished
+ trifunctorComp₁₂₃
+ trifunctorComp₂₃₄
+ trifunctorComp₂₃₄Counit
+ trifunctor₁₂
+ trifunctor₂₃
+ truncGECompHomologyFunctorIso
+ truncGEComparison
+ truncGEComparison_app_fac
+ truncGEIso
+ truncGEIso_hom_inv_id_app
+ truncGEIso_inv_hom_id_app
+ truncGELE
+ truncGELECompHomologyFunctorIso
+ truncGELEIso
+ truncGELEIsoLEGE
+ truncGELEIsoTruncGELT
+ truncGELT
+ truncGELTIsoLTGE
+ truncGELTToLTGE
+ truncGELTToLTGE_app_pentagon
+ truncGELTToLTGE_app_pentagon_uniqueness
+ truncGELTδLT
+ truncGETriangle
+ truncGETriangle_distinguished
+ truncGEXIso
+ truncGEXIsoOpcycles
+ 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
+ truncGE₀LE₀_mem_heart
+ truncGT
+ truncGTIsoTruncGE
+ truncGTδLE
+ truncGTπ
+ truncLE
+ truncLECompHomologyFunctorIso
+ truncLEComparison
+ truncLEComparison_app_fac
+ truncLEGE
+ truncLEGEIso
+ truncLEIso
+ truncLEIsoTruncLT
+ truncLEIsoTruncLT_hom_ι
+ truncLEIsoTruncLT_hom_ι_app
+ truncLEIsoTruncLT_inv_ι
+ truncLEIsoTruncLT_inv_ι_app
+ truncLEIso_hom_inv_id_app
+ truncLEIso_inv_hom_id_app
+ truncLELEIsoOfLE
+ truncLEMapOfLE
+ truncLEMapOfLE_naturality
+ truncLEMapOfLE_ι
+ truncLETriangle
+ truncLETriangle_distinguished
+ truncLEι
+ truncLE₀GE₀ToHeart
+ truncLE₀GE₀ToHeartιHeart
+ truncLE₀GE₀_mem_heart
+ truncLTGE
+ truncLT_map_truncGE_map_truncLTι_app_fac
+ truncLT_map_truncLTι_app
+ truncLTι_comp_truncGEπ
+ truncLTι_comp_truncGEπ_app
+ uncurryCurryIso
+ uncurry₃_map_app
+ uncurry₃_obj_map
+ uncurry₄
+ uncurry₄_map_app
+ uncurry₄_obj_map
+ unit
+ unopFunctor
+ unopMap
+ unopMap_id
+ unopOp
+ vanishing_from_positive_shift
+ w_p'
+ weakEquivalence_op_iff
+ weakEquivalence_unop_iff
+ weakEquivalences_eq
+ whiskerHorizontal_iff
+ whiskerLeft_eq
+ whiskerLeft_of_kFlat
+ whiskerRight_eq
+ whiskerRight_of_kFlat
+ whiskeringLeft
+ whiskeringLeft₂
+ whiskeringLeft₂BifunctorMapHomotopyCategoryIso
+ whiskeringLeft₂Equiv'
+ whiskeringLeft₃Equiv
+ whiskeringLeft₄
+ whiskeringLeft₄Equiv
+ whiskeringLeft₄Map
+ whiskeringLeft₄Obj
+ whiskeringLeft₄ObjMap
+ whiskeringLeft₄ObjObj
+ whiskeringLeft₄ObjObjMap
+ whiskeringLeft₄ObjObjObj
+ whiskeringLeft₄ObjObjObjMap
+ whiskeringLeft₄ObjObjObjObj
+ zero
+ zero_add
+ zero_mem_heart
+ zero_τ₅
+ zero₁
+ zero₂
+ zero₃
+ Ψ
+ Ψ_fromOpcycles
+ Ψ_opcyclesMap
+ Ψ_opcyclesMap_exact
+ β
+ δ
+ δFromOpcycles
+ δToCycles
+ δToCycles_cyclesIso_inv
+ δToCycles_iCycles
+ δToCycles_πE
+ δ_eq
+ δ_eq_zero_of_isIso₁
+ δ_eq_zero_of_isIso₂
+ δ_pOpcycles
+ δ_toCycles
+ δ_δ
+ δ₀_map_δ₁Toδ₀_app
+ δ₀_map_δ₃Toδ₂_app_eq_δ₂Toδ₁_app_δ₀_obj
+ δ₂_map_δ₃Toδ₂_app
+ δ₂δ₂Toδ₃δ₁
+ δ₃Toδ₀
+ δ₃Toδ₂
+ δ₃δ₀Toδ₀δ₁
+ δ₃δ₁Toδ₀δ₁
+ δ₃δ₁Toδ₀δ₂
+ δ₃δ₁Toδ₂δ₀
+ δ₃δ₁Toδ₂δ₁
+ δ₄Toδ₃
+ δ₇
+ ιArrow
+ ιCofibrantObject
+ ιCofibrantObjectLocalizerMorphism
+ ιE
+ ιE_δFromOpcycles
+ ιE₂OneZero
+ ιE₂OneZero_πE₃ZeroOne
+ ιE₂OneZero_πE₃ZeroOne_exact
+ ιE₃TwoZero
+ ιFibrantObject
+ ιFibrantObjectLocalizerMorphism
+ ιHeart
+ ιHeartAddEquiv
+ ιHeartHomology_zero
+ ιHeartHomology₀
+ ιHeartIso
+ ιHeartObjHeartMkIso
+ ιHeartTruncGE
+ ιHeartTruncGELE
+ ιHeartTruncLE
+ ιHeart_map_liftHeart_map
+ ιHeart_obj_mem
+ ιInjectiveResolution
+ ιIterationFunctor_app_bot
+ ιK
+ ιK_lift
+ ιK_mor₁
+ ιStupidTrunc
+ ιStupidTruncNatTrans
+ ιStupidTrunc_f_naturality
+ ιStupidTrunc_naturality
+ ιStupidTrunc_πStupidTrunc
+ ιStupidTruncf
+ ιStupidTruncf'_eq
+ ιStupidTruncf_eq
+ ιStupidTruncf_πStupidTruncf
+ ιSuccObj
+ ιSuccObj_mem
+ ι_filtrationLEFunctorCompColimIso_hom_app
+ ι_mapTotalXIso_hom
+ ι_map_filtrationLEMinus_map
+ ι_map_πQ
+ ι_obj_filtrationLEMinus_obj
+ μNatTrans
+ π'
+ πAbutmentFiltration
+ πE
+ πE_EIsoH_hom
+ πE_EMap
+ πE_EToCycles
+ πE_d_ιE
+ πE_ιE
+ πE₃ZeroOne
+ πE₃ZeroOne_edgeMonoStep
+ πQ
+ πQ_desc
+ πStupidTrunc
+ πStupidTruncNatTrans
+ πStupidTrunc_f_naturality
+ πStupidTrunc_naturality
+ πStupidTruncf
+ πStupidTruncf_eq
+ πStupidTruncf_eq'
+ πSuccObj
+ π_comp_p'
+ π_descTruncGE
+ π_descTruncGT
+ π_f_cochain₁_v_ι_f
+ π_hom
+ π_inv
+ π_inv'
+ π_natTransTruncGEOfLE
+ π_natTransTruncGEOfLE_app
+ π_pageInfinityIso_hom
+ π_pageInfinityIso_hom_iso'_hom
+ π_pageInfinityIso_hom_iso_hom
+ π_pageInfinityIso_hom_iso₃_hom
+ π_pageInfinityι
+ π_shiftTruncGE_inv_app
+ π_truncGTIsoTruncGE_hom
+ π_truncGTIsoTruncGE_hom_ι_app
+ π_truncGTIsoTruncGE_inv
+ π_truncGTIsoTruncGE_inv_ι_app
+ π₀
+ π₀_ι
+ π₁
+ π₁_ι
+ τ₀_comp
+ τ₀_id
+ τ₁_comp
+ τ₁_id
+ τ₂_comp
+ τ₂_id
+ φ
+ ω₁
+ ω₁δ
+ ω₁δ_naturality
++ Exact
++ I
++ Index
++ IsEventuallyConstant.mk'
++ IsGE
++ IsLE
++ KFlat
++ KInjectives
++ Q
++ QhCompιIsoιCompQh
++ TStructure.t
++ associator
++ bifunctor
++ bifunctorComp₁₂Iso
++ bifunctorComp₂₃Iso
++ closedUnderLimitsOfShapeDiscrete
++ cochainComplex
++ cofibration_iff
++ comp_τ₆
++ f
++ f_eq
++ fibration_iff
++ forget
++ hom_fst
++ hom_inv_id
++ hom_snd
++ homologyFunctor
++ homologyIso
++ homologyIso'
++ homology_exact₁
++ homology_exact₂
++ homology_exact₃
++ i
++ i'
++ id_τ₆
++ inl_inv
++ inr
++ inr_inv
++ inr_p₁₀
++ inr_p₂
++ instance (A X : C) [t.IsGE X 0] [t.IsLE A 0] :
++ instance (A X : C) [t.IsLE X 0] [t.IsGE A 0] :
++ instance (J : Type) [Category J] [FinCategory J] :
++ instance (K : CochainComplex C ℤ) :
++ instance (K : CochainComplex.Plus (InjectiveObject C)) :
++ instance (K : HomologicalComplex C c) :
++ instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsGE n := by
++ instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsLE n := by
++ instance (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) :
++ instance (X : C) (n : ℤ) [t.IsLE X n] (i : EInt) :
++ instance (X : GradedObject I C₁) [HasColimitsOfShape B C₂]
++ instance (Y : GradedObject J C₂) [HasColimitsOfShape B C₁]
++ instance (a b : ℤ) (X : C) :
++ instance (n : ℤ) : (homologyFunctor C n).IsHomological := by
++ instance (n : ℤ) : Mono (K.ιTruncLE n) := by
++ instance (p : ℕ) : E.HasEdgeEpiAtFrom ⟨p, 0⟩ 2
++ instance (p : ℕ) : E.HasEdgeEpiAtFrom ⟨p, 1⟩ 3
++ instance (q : ℕ) : E.HasEdgeMonoAtFrom ⟨0, q⟩ 2
++ instance (q : ℕ) : E.HasEdgeMonoAtFrom ⟨1, q⟩ 2
++ instance (q : ℕ) : E.HasEdgeMonoAtFrom ⟨2, q⟩ 3
++ instance (r' : ℤ) (h : r ≤ r') :
++ instance (α : Type _) [AddRightCancelSemigroup α] [One α] [DecidableEq α] :
++ instance : (L C).IsInduced
++ instance : (L C).IsLocalizedEquivalence := by
++ instance : (L C).functor.EssSurj := by dsimp; infer_instance
++ instance : (L C).functor.Full := by dsimp; infer_instance
++ instance : (Qh (C := C)).EssSurj := by
++ instance : (Qh (C := C)).mapArrow.EssSurj
++ instance : (R C).IsInduced
++ instance : (R C).IsLocalizedEquivalence
++ instance : (R C).functor.EssSurj := by dsimp; infer_instance
++ instance : (R C).functor.Full := by dsimp; infer_instance
++ instance : (localizerMorphism C).IsInduced
++ instance : (quasiIso A (.up ℤ)).kFlat.ContainsZero
++ instance : (quasiIso A (.up ℤ)).kFlat.IsStableUnderRetracts
++ instance : (quasiIso A (.up ℤ)).kFlat.IsStableUnderShift ℤ
++ instance : (quasiIso A).IsCompatibleWithShift ℤ
++ instance : (quasiIso A).IsMultiplicative := by
++ instance : (quasiIso A).RespectsIso := by
++ instance : (quotient C).EssSurj
++ instance : (quotient C).Full := by dsimp [quotient]; infer_instance
++ instance : (ι C).CommShift ℤ
++ instance : (ι C).Faithful := ObjectProperty.faithful_ι _
++ instance : (ι C).Full := ObjectProperty.full_ι _
++ instance : HasZeroMorphisms (ShortComplex C)
++ instance [E.HasEdgeMonoAt (0, 1) 2] [E.HasEdgeEpiAt (2, 0) 2] :
++ instance [F.PreservesHomology] {ι : Type*} (c : ComplexShape ι) {K L : HomologicalComplex C c}
++ instance [HasColimitsOfShape J C] :
++ instance [HasCoproducts.{w} C] [IsStableUnderTransfiniteComposition.{w} W]
++ instance [HasFiniteCoproducts C] [W.IsMultiplicative]
++ instance [HasFunctorialFlatResolution A] :
++ instance [LocallySmall.{w} C] [MorphismProperty.IsSmall.{w} I] :
++ instance [P.IsTriangulated] [P.IsClosedUnderIsomorphisms] :
++ instance {A B X Y : CochainComplex.Plus C} (i : A ⟶ B) (p : X ⟶ Y)
++ instance {D : Type*} [Category* D] (L : Minus C ⥤ D) [L.IsLocalization (quasiIso C)] :
++ instance {D : Type*} [Category* D] (L : Plus C ⥤ D) [L.IsLocalization (quasiIso C)] :
++ instance {a a' : α} (φ : a ⟶ a') (K : HomologicalComplex C c') :
++ inv'
++ inv_hom_id
++ isGE_ι_obj_iff
++ isIso_EMapFourδ₁Toδ₀'
++ isIso_EMapFourδ₄Toδ₃'
++ isIso_p_f
++ isIso_quotient_map
++ isIso_ιStupidTrunc_f
++ isIso_ιTruncLE_f
++ isIso_πStupidTrunc_f
++ isIso_πTruncGE_f
++ isLE_ι_obj_iff
++ isTriangulated_of_isRightDerivedFunctor
++ isZero
++ iso₁
++ iso₂
++ kFlat_iff_preservesQuasiIso
++ leftUnitor
++ leftUnitor_hom_app
++ lift
++ mapStupidTruncGE
++ mapStupidTruncLE
++ map_shiftIso_hom_app
++ minus
++ mk_surjective
++ mono_iff
++ of
++ ofIso
++ p
++ pageInfinity
++ pageInfinityIso
++ pentagon
++ plus
++ p₁
++ p₁₀
++ p₂
++ quotientCompι
++ quotient_obj_surjective
++ respectsIso_shortExact
++ rightUnitor
++ rightUnitor_hom_app
++ shiftIso
++ shift_inv
++ shortComplex_exact
++ shortComplex₁
++ shortComplex₂
++ spectralSequence
++ spectralSequenceNat
++ subcategoryAcyclic
++ uncurry
++ weakEquivalence_iff
++ whiskerHorizontal
++ whiskeringLeft₂Equiv
++ zero_τ₁
++ zero_τ₂
++ zero_τ₃
++ zero_τ₄
++ α
++ δ_naturality
++ δ₂Toδ₁
++ δ₆
++ ιKFlat
++ ι_p₁₀_v
++ ι_p₂_v
++ ι_ι₁
++ ι₁
++ ι₁_p₁₀
++ ι₁_p₂
++ π
+++ L
+++ Minus
+++ Plus
+++ Qh
+++ R
+++ comm
+++ exists_injective_resolution
+++ fullyFaithfulι
+++ functor
+++ homMk
+++ instance (K : CochainComplex A ℤ) (i : ℤ) :
+++ instance (K : CochainComplex A ℤ) (i : ℤ) [K.IsStrictlyLE i] :
+++ instance (X : C) (a b : ℤ) :
+++ instance (X : C) (a b : ℤ) [t.IsGE X a] :
+++ instance (X : CofibrantObject C) :
+++ instance [HasDerivedCategory C] :
+++ inverse
+++ isIso_of_isLeftDerivabilityStructure
+++ isZero_homology_of_isGE
+++ isZero_homology_of_isLE
+++ map
+++ mapHomologicalComplexObjIso
+++ mk
+++ quasiIso_eq_subcategoryAcyclic_trW
+++ quotient
+++ triangle
+++ δ₁Toδ₀
+++ δ₅
++++ comp_τ₅
++++ fac
++++ id_τ₅
++++ instance (K : CochainComplex.Minus A) :
++++ instance (n : ℤ) : (singleFunctor C n).Additive := by
++++ instance (r' : ℤ) :
++++ isIso_iff
++++ mkOfLE
++++ shortExact
++++ singleFunctor
++++ singleFunctors
++++ singleFunctorιIso
++++ δ₄
+++++ comp_τ₀
+++++ id_τ₀
+++++ inv
+++++ isoMk
+++++ unop
+++++ δ₃
++++++ comp_τ₄
++++++ hom
++++++ id_τ₄
++++++ localizerMorphism
++++++ op
++++++ quasiIso
++++++ shortComplex
++++++ δ₀
++++++ δ₁
++++++ δ₂
+++++++ comp_τ₁
+++++++ comp_τ₂
+++++++ comp_τ₃
+++++++ id_τ₁
+++++++ id_τ₂
+++++++ id_τ₃
++++++++ iso
++++++++ mk'
+++++++++ ι
++++++++++ Hom.comp
++++++++++ Hom.id
+++++++++++++ Hom
+++++++++++++++++++ instance :
++++++++++++-+ hom_ext
+-+ map_neg
+-+ map_sub
+-++ map_add
+-++ map_zero
- comp_hom
- id_hom
- 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
- instance (n : ℤ) : (shiftFunctor (DerivedCategory C) n).Additive := by
- instance : (quotient V c).Additive
- instance {β : Type v} (g : β → C) [HasCoproduct g] [∀ b, Projective (g b)] : Projective (∐ g)
- isCocontinuous_comp
- isCocontinuous_id
- mapHomologicalComplex_commShiftIso_eq
- quasiIso_eq_subcategoryAcyclic_W
- weakEquivalences_op_iff
- weakEquivalences_unop_iff
-+++-+ prod
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 script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (11.02, 0.90)
| Current number | Change | Type |
|---|---|---|
| 499 | 4 | porting notes |
| 1361 | 1 | backwards compatibility flags |
| 1346 | 1 | privateInPublic flags |
| 718 | 88 | erw |
| 13 | 10 | maxHeartBeats modifications |
Current commit 4e50e585ae
Reference commit c70a3c4816
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).
github-actions
bot
added
the
merge-conflict
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
github-actions
bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
4 participants
This PR contains a redefinition of homology, theorems about localization of categories, including triangulated categories, a construction of the derived category of an abelian category, derived functors, spectral sequences, etc. (This is made a PR only to facilitate navigation in the code of this branch.)
This formalization is outlined in the paper Formalization of derived categories in Lean/mathlib https://hal.science/hal-04546712
The homology of
ShortComplex C(diagrams of two composable morphisms whose composition is zero) is developed inAlgebra.Homology.ShortComplex. The files in that folder have been added one by one in separate PRs, and then, the current definition ofhomologyhas been replaced by this new definition in a refactor PR.Homology refactor:
Homological complexes:
Localization of categories:
Shifts on categories:
Triangulated categories:
Construction of the derived category:
Derived functors:
Refactor of Ext-groups:
This PR continues the work from #4197.
Original PR: #4197