Theorems · Inductive type · category theory
CategoryTheory.ObjectProperty.IsSerreClass
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → CategoryTheory.ObjectProperty C → PropA Serre class in an abelian category consists of a predicate which holds for the zero object and is closed under subobjects, quotients, extensions.
- Cited by
- 61 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Abelianstatement · cited by 1,753
- CategoryTheory.ObjectPropertystatement · cited by 798
Cited by69
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.isoModSerrestatement and proof · cited by 50
- CategoryTheory.ObjectProperty.monoModSerrestatement and proof · cited by 16
- CategoryTheory.ObjectProperty.epiModSerrestatement and proof · cited by 16
- CategoryTheory.ObjectProperty.SerreClassLocalization.abelianstatement and proof · cited by 6
- CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iffstatement and proof · cited by 5
- CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_iffstatement and proof · cited by 4
- CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_iffstatement and proof · cited by 4
- CategoryTheory.ObjectProperty.monoModSerre_of_monostatement and proof · cited by 4
- CategoryTheory.ObjectProperty.epiModSerre_of_epistatement and proof · cited by 4
- CategoryTheory.ObjectProperty.isoModSerre_iff_of_monostatement and proof · cited by 3
- CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernelstatement and proof · cited by 3
- CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernelstatement and proof · cited by 3