Structures · Category theory
CategoryTheory.IsFilteredOrEmpty
A category IsFilteredOrEmpty if
1. for every pair of objects there exists another object "to the right", and
2. for every pair of parallel morphisms there exists a morphism to the right so the compositions
are equal.
- Defined in
- Mathlib.CategoryTheory.Filtered.Basic
- Shape
- One type argument · adds cocone_objs, cocone_maps
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances5
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.Grothendieck
- CategoryTheory.IsFiltered.SmallFilteredIntermediate
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by83
- CategoryTheory.IsFiltered.max
- CategoryTheory.IsFiltered.leftToMax
- CategoryTheory.IsFiltered.rightToMax
- CategoryTheory.IsFiltered.coeq
- CategoryTheory.IsFiltered.coeqHom
- CategoryTheory.IsFiltered.coeq_condition
- CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff'
- CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff
- CategoryTheory.Functor.final_iff_of_isFiltered
- CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'
- CategoryTheory.IsFilteredOrEmpty.cocone_maps
- CategoryTheory.IsFiltered.bowtie
- CategoryTheory.IsFiltered.span
- CategoryTheory.IsFiltered.tulip
- CategoryTheory.IsFilteredOrEmpty.cocone_objs
- CategoryTheory.Functor.final_of_exists_of_isFiltered
- CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists
- CategoryTheory.IsFilteredOrEmpty.of_right_adjoint
- CategoryTheory.IsFiltered.coeq₃
- CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful
- CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful
- CategoryTheory.IsFiltered.coeq₃Hom
- CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff
- CategoryTheory.IsFiltered.crown
- CategoryTheory.IsFilteredOrEmpty.of_final
- CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op
- CategoryTheory.finallySmall_of_small_weakly_terminal_set
- CategoryTheory.Limits.IsColimit.eq_iff
- CategoryTheory.IsFilteredOrEmpty.of_equivalence
- CategoryTheory.Limits.IsColimit.eq_iff'
- CategoryTheory.IsFiltered.SmallFilteredIntermediate
- CategoryTheory.Limits.Types.FilteredColimit.rel_equiv
- CategoryTheory.IsFilteredOrEmpty.isPreconnected
- CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring
- CategoryTheory.IsFiltered.coeq₃_condition₂
- CategoryTheory.Functor.Final.exists_coeq_of_locally_small
- CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimit₂
- CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion
- CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoringCompInclusion
- CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_colimitTypeRel
- CategoryTheory.IsFiltered.coeq₃_condition₁
- CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux
- CategoryTheory.IsFiltered.coeq_condition_assoc
- CategoryTheory.IsFiltered.instSmallCategorySmallFilteredIntermediate
- CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure
- CategoryTheory.IsFiltered.crown₄
- CommRingCat.FilteredColimits.nontrivial
- CategoryTheory.Functor.final_diag_of_isFiltered
- CategoryTheory.Under.final_forget
- CategoryTheory.IsFiltered.secondToMax₃
Ancestors0
No ancestors.