Structures · Category theory
CategoryTheory.Preregular
The condition Preregular C is a property that effective epis can be "pulled back" along any
morphism. This is satisfied e.g. by categories that have pullbacks that preserve effective
epimorphisms (like Profinite and CompHaus), and categories where every object is projective
(like Stonean).
- Shape
- One type argument · adds exists_fac
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- LightProfinite
- Profinite
- CompHaus
- Stonean
- CategoryTheory.SmallModel
How is a type an instance?
Loading the hierarchy index…
Assumed by64
- CategoryTheory.regularTopology
- CategoryTheory.Equivalence.sheafCongrPreregular
- CategoryTheory.Equivalence.preregular
- CategoryTheory.Presheaf.coherentExtensiveEquivalence
- CategoryTheory.regularCoverage
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
- CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi
- CategoryTheory.Functor.reflects_preregular
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
- CategoryTheory.regularTopology.isLocallySurjective_iff
- CategoryTheory.coherentTopology.isLocallySurjective_iff
- CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive
- CategoryTheory.extensive_regular_generate_coherent
- CategoryTheory.Preregular.exists_fac
- CategoryTheory.regularTopology.equalizerCondition_iff_isSheaf
- CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff
- CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced
- CategoryTheory.coherentTopology.epi_π_app_zero_of_epi
- CategoryTheory.Equivalence.preregular_isSheaf_iff
- CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map
- CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types
- CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi
- CategoryTheory.regularTopology.isSheaf_of_projective
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp
- CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app
- CategoryTheory.regularTopology.subcanonical
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_hom
- CategoryTheory.regularTopology.coverPreserving
- CategoryTheory.Equivalence.instPreregularSmallModel
- CategoryTheory.regularCoverage.congr_simp
- CategoryTheory.coherentTopology.equivalence'
- CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp
- CategoryTheory.regularTopology.eq_induced
- CategoryTheory.regularTopology.isSheaf_yoneda_obj
- CategoryTheory.regularTopology.instEffectiveEpiComp
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app
- CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits
- CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular
- CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_obj
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app
- CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeObjFunctorIsSheafCoherentTopology
- CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp
- CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts
- CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_obj
- CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_map
- CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app
- CategoryTheory.regularTopology.equivalence
- CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app
- CategoryTheory.Equivalence.preregular_isSheaf_iff_of_essentiallySmall
Ancestors0
No ancestors.