Structures · Category theory
CategoryTheory.Precoherent
The condition Precoherent C is essentially the minimal condition required to define the
coherent coverage on C.
- Shape
- One type argument · adds pullback
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.SmallModel
How is a type an instance?
Loading the hierarchy index…
Assumed by36
- CategoryTheory.coherentTopology
- CategoryTheory.Equivalence.sheafCongrPrecoherent
- CategoryTheory.Equivalence.precoherent
- CategoryTheory.coherentCoverage
- CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily
- CategoryTheory.Functor.reflects_precoherent
- CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
- CategoryTheory.Precoherent.pullback
- CategoryTheory.isSheaf_coherent
- CategoryTheory.Equivalence.precoherent_isSheaf_iff
- CategoryTheory.coherentTopology.isSheaf_yoneda_obj
- CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced
- CategoryTheory.EffectiveEpiFamily.transitive_of_finite
- CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app
- CategoryTheory.Equivalence.instPrecoherentSmallModel
- CategoryTheory.instPreregularOfPrecoherentOfHasFiniteCoproducts
- CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app
- CategoryTheory.coherentTopology.eq_induced
- CategoryTheory.coherentTopology.instIsDenseSubsite
- CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app
- CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_hom_app
- CategoryTheory.coherentTopology.congr_simp
- CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app
- CategoryTheory.coherentCoverage.congr_simp
- CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_map
- CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_obj_obj
- CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_map
- CategoryTheory.coherentTopology.instIsCoverDense
- CategoryTheory.coherentTopology.coverPreserving
- CategoryTheory.coherentTopology.subcanonical
- CategoryTheory.Equivalence.precoherent_isSheaf_iff_of_essentiallySmall
- CategoryTheory.coherentTopology.equivalence
- CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_obj_obj
- CategoryTheory.Equivalence.instIsDenseSubsiteCoherentTopologyInverse
- CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_hom_app
- CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis
Ancestors0
No ancestors.