Mathlib Map

Structures · Category theory

CategoryTheory.IsFiltered

A category IsFiltered if 1. for every pair of objects there exists another object "to the right", 2. for every pair of parallel morphisms there exists a morphism to the right so the compositions are equal, and 3. there exists some object.

Defined in
Mathlib.CategoryTheory.Filtered.Basic
Shape
One type argument · adds nonempty
Open in Mathlib docs

Extends1

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances20

  • CategoryTheory.Discrete
  • CategoryTheory.Comma
  • CategoryTheory.WithInitial
  • CategoryTheory.Under
  • CategoryTheory.CostructuredArrow
  • CategoryTheory.StructuredArrow
  • CategoryTheory.ULiftHom
  • CategoryTheory.Grothendieck
  • CategoryTheory.FinallySmall.FilteredFinalModel
  • CategoryTheory.Limits.ColimitPresentation.Total
  • CategoryTheory.AsSmall
  • PartOrdEmb.carrier
  • CategoryTheory.IsFiltered.SmallFilteredIntermediate
  • HasCardinalLT.Set
  • CategoryTheory.Limits.IndObjectPresentation.I
  • CategoryTheory.IndParallelPairPresentation.I
  • Subtype
  • Prod
  • ULift
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by294

Ancestors1