Structures · Category theory
CategoryTheory.IsCofilteredOrEmpty
A category IsCofilteredOrEmpty if
1. for every pair of objects there exists another object "to the left", and
2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
are equal.
- Defined in
- Mathlib.CategoryTheory.Filtered.Basic
- Shape
- One type argument · adds cone_objs, cone_maps
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances5
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.PreGaloisCategory.PointedGaloisObject
- CategoryTheory.IsCofiltered.SmallCofilteredIntermediate
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by79
- CategoryTheory.IsCofiltered.eq
- CategoryTheory.IsCofiltered.min
- CategoryTheory.IsCofilteredOrEmpty.cone_objs
- CategoryTheory.IsCofiltered.minToLeft
- CategoryTheory.IsCofiltered.minToRight
- CategoryTheory.IsCofiltered.cospan
- CategoryTheory.IsCofiltered.eqHom
- CategoryTheory.IsCofilteredOrEmpty.cone_maps
- CategoryTheory.Functor.initial_iff_of_isCofiltered
- nonempty_sections_of_finite_cofiltered_system
- CategoryTheory.IsCofiltered.eq_condition
- CategoryTheory.Functor.toEventualRanges
- CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint
- CategoryTheory.Functor.initial_of_exists_of_isCofiltered
- TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system
- CategoryTheory.IsCofiltered.bowtie
- CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists
- CategoryTheory.Functor.eval_section_surjective_of_surjective
- AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty'
- CategoryTheory.initiallySmall_of_small_weakly_initial_set
- CategoryTheory.Functor.eventualRange_mapsTo
- CategoryTheory.Functor.ranges_directed
- AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty
- CategoryTheory.IsCofilteredOrEmpty.of_equivalence
- CategoryTheory.Functor.toPreimages_nonempty_of_surjective
- CategoryTheory.Functor.toEventualRanges_obj
- nonempty_sections_of_finite_cofiltered_system.init
- AlgebraicGeometry.Scheme.nonempty_of_isLimit
- CategoryTheory.IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful
- CategoryTheory.Functor.initial_iff_isCofiltered_costructuredArrow
- CategoryTheory.Functor.thin_diagram_of_surjective
- CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful
- CategoryTheory.IsCofilteredOrEmpty.isPreconnected
- TopCat.partialSections.nonempty
- CategoryTheory.IsCofiltered.wideCospan
- CategoryTheory.Functor.isMittagLeffler_iff_subset_range_comp
- CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty
- CategoryTheory.Functor.toEventualRanges_finite
- CategoryTheory.Functor.eventually_injective
- CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instOfNonempty
- CategoryTheory.IsCofilteredOrEmpty.of_initial
- CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoringCompInclusion
- CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFullInclusion
- CategoryTheory.IsCofiltered.min.congr_simp
- CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring
- CategoryTheory.IsCofiltered.instIsCofilteredOrEmptyFullSubcategoryCofilteredClosure
- CategoryTheory.Functor.isMittagLeffler_of_exists_finite_range
- CategoryTheory.Functor.initial_diag_of_isFiltered
- CategoryTheory.IsCofiltered.over
- CategoryTheory.Functor.IsMittagLeffler.toPreimages
Ancestors0
No ancestors.