Equivalence

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

Statistics

Metric	Count
Definitions sheafCongrPrecoherent, sheafCongrPreregular	2
Theorems instIsDenseSubsiteCoherentTopologyInverse, instIsDenseSubsiteRegularTopologyInverse, instPrecoherentSmallModel, instPreregularSmallModel, precoherent, precoherent_isSheaf_iff, precoherent_isSheaf_iff_of_essentiallySmall, preregular, preregular_isSheaf_iff, preregular_isSheaf_iff_of_essentiallySmall, sheafCongrPrecoherent_counitIso_hom_app_hom_app, sheafCongrPrecoherent_counitIso_inv_app_hom_app, sheafCongrPrecoherent_functor_map_hom_app, sheafCongrPrecoherent_functor_obj_obj_map, sheafCongrPrecoherent_functor_obj_obj_obj, sheafCongrPrecoherent_inverse_map_hom_app, sheafCongrPrecoherent_inverse_obj_obj_map, sheafCongrPrecoherent_inverse_obj_obj_obj, sheafCongrPrecoherent_unitIso_hom_app_hom_app, sheafCongrPrecoherent_unitIso_inv_app_hom_app, sheafCongrPreregular_counitIso_hom_app_hom_app, sheafCongrPreregular_counitIso_inv_app_hom_app, sheafCongrPreregular_functor_map_hom_app, sheafCongrPreregular_functor_obj_obj_map, sheafCongrPreregular_functor_obj_obj_obj, sheafCongrPreregular_inverse_map_hom_app, sheafCongrPreregular_inverse_obj_obj_map, sheafCongrPreregular_inverse_obj_obj_obj, sheafCongrPreregular_unitIso_hom_app_hom_app, sheafCongrPreregular_unitIso_inv_app_hom_app	30
Total	32

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
sheafCongrPrecoherent 📖	CompOp	10 math math: sheafCongrPrecoherent_unitIso_inv_app_hom_app, sheafCongrPrecoherent_functor_obj_obj_obj, sheafCongrPrecoherent_counitIso_inv_app_hom_app, sheafCongrPrecoherent_counitIso_hom_app_hom_app, sheafCongrPrecoherent_functor_obj_obj_map, sheafCongrPrecoherent_inverse_obj_obj_obj, sheafCongrPrecoherent_inverse_obj_obj_map, sheafCongrPrecoherent_functor_map_hom_app, sheafCongrPrecoherent_inverse_map_hom_app, sheafCongrPrecoherent_unitIso_hom_app_hom_app
sheafCongrPreregular 📖	CompOp	10 math math: sheafCongrPreregular_functor_obj_obj_obj, sheafCongrPreregular_counitIso_hom_app_hom_app, sheafCongrPreregular_unitIso_hom_app_hom_app, sheafCongrPreregular_inverse_obj_obj_obj, sheafCongrPreregular_inverse_map_hom_app, sheafCongrPreregular_inverse_obj_obj_map, sheafCongrPreregular_functor_map_hom_app, sheafCongrPreregular_counitIso_inv_app_hom_app, sheafCongrPreregular_unitIso_inv_app_hom_app, sheafCongrPreregular_functor_obj_obj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsDenseSubsiteCoherentTopologyInverse 📖	mathematical	—	CategoryTheory.Functor.IsDenseSubsite CategoryTheory.coherentTopology precoherent inverse	—	precoherent CategoryTheory.coherentTopology.instIsCoverDense CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence isEquivalence_inverse CategoryTheory.Functor.IsLocallyFull.of_full full_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful faithful_inverse CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.reflects_precoherent CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence CategoryTheory.coherentTopology.eq_induced
instIsDenseSubsiteRegularTopologyInverse 📖	mathematical	—	CategoryTheory.Functor.IsDenseSubsite CategoryTheory.regularTopology preregular inverse	—	preregular CategoryTheory.regularTopology.instIsCoverDense CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence isEquivalence_inverse CategoryTheory.Functor.IsLocallyFull.of_full full_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful faithful_inverse CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.reflects_preregular CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence CategoryTheory.regularTopology.eq_induced
instPrecoherentSmallModel 📖	mathematical	—	CategoryTheory.Precoherent CategoryTheory.SmallModel CategoryTheory.smallCategorySmallModel	—	precoherent
instPreregularSmallModel 📖	mathematical	—	CategoryTheory.Preregular CategoryTheory.SmallModel CategoryTheory.smallCategorySmallModel	—	preregular
precoherent 📖	mathematical	—	CategoryTheory.Precoherent	—	CategoryTheory.Functor.reflects_precoherent CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence isEquivalence_inverse CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence full_inverse faithful_inverse
precoherent_isSheaf_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology precoherent CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op inverse	—	precoherent CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Presheaf.isSheaf_of_iso_iff
precoherent_isSheaf_iff_of_essentiallySmall 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.SmallModel CategoryTheory.smallCategorySmallModel instPrecoherentSmallModel CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op inverse CategoryTheory.equivSmallModel	—	precoherent_isSheaf_iff
preregular 📖	mathematical	—	CategoryTheory.Preregular	—	CategoryTheory.Functor.reflects_preregular CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence isEquivalence_inverse CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence full_inverse faithful_inverse
preregular_isSheaf_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology preregular CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op inverse	—	preregular CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Presheaf.isSheaf_of_iso_iff
preregular_isSheaf_iff_of_essentiallySmall 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology CategoryTheory.SmallModel CategoryTheory.smallCategorySmallModel instPreregularSmallModel CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op inverse CategoryTheory.equivSmallModel	—	preregular_isSheaf_iff
sheafCongrPrecoherent_counitIso_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology precoherent CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.comp sheafCongr.inverse instIsDenseSubsiteCoherentTopologyInverse sheafCongr.functor CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom counitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op functor inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_counitIso_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology precoherent CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.id CategoryTheory.Functor.comp sheafCongr.inverse instIsDenseSubsiteCoherentTopologyInverse sheafCongr.functor CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv counitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op functor inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_functor_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op inverse CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory precoherent CategoryTheory.ObjectProperty.FullSubcategory.obj instIsDenseSubsiteCoherentTopologyInverse CategoryTheory.Functor.map functor sheafCongrPrecoherent Opposite.op Opposite.unop	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_functor_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology precoherent CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category functor sheafCongrPrecoherent Opposite.op inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	precoherent
sheafCongrPrecoherent_functor_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology precoherent CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category functor sheafCongrPrecoherent Opposite.op inverse Opposite.unop	—	precoherent
sheafCongrPrecoherent_inverse_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.coherentTopology precoherent CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op functor CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj instIsDenseSubsiteCoherentTopologyInverse CategoryTheory.Functor.map inverse sheafCongrPrecoherent Opposite.op Opposite.unop	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_inverse_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf precoherent CategoryTheory.ObjectProperty.FullSubcategory.category inverse sheafCongrPrecoherent Opposite.op functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	precoherent
sheafCongrPrecoherent_inverse_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf precoherent CategoryTheory.ObjectProperty.FullSubcategory.category inverse sheafCongrPrecoherent Opposite.op functor Opposite.unop	—	precoherent
sheafCongrPrecoherent_unitIso_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.id CategoryTheory.Functor.comp precoherent sheafCongr.functor instIsDenseSubsiteCoherentTopologyInverse sheafCongr.inverse CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom unitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op inverse functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_unitIso_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.comp precoherent sheafCongr.functor instIsDenseSubsiteCoherentTopologyInverse sheafCongr.inverse CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv unitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op inverse functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPreregular_counitIso_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology preregular CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.comp sheafCongr.inverse instIsDenseSubsiteRegularTopologyInverse sheafCongr.functor CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom counitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op functor inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_counitIso_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology preregular CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.id CategoryTheory.Functor.comp sheafCongr.inverse instIsDenseSubsiteRegularTopologyInverse sheafCongr.functor CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv counitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op functor inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_functor_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.regularTopology CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op inverse CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory preregular CategoryTheory.ObjectProperty.FullSubcategory.obj instIsDenseSubsiteRegularTopologyInverse CategoryTheory.Functor.map functor sheafCongrPreregular Opposite.op Opposite.unop	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_functor_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology preregular CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category functor sheafCongrPreregular Opposite.op inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	preregular
sheafCongrPreregular_functor_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology preregular CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category functor sheafCongrPreregular Opposite.op inverse Opposite.unop	—	preregular
sheafCongrPreregular_inverse_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.regularTopology preregular CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op functor CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj instIsDenseSubsiteRegularTopologyInverse CategoryTheory.Functor.map inverse sheafCongrPreregular Opposite.op Opposite.unop	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_inverse_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf preregular CategoryTheory.ObjectProperty.FullSubcategory.category inverse sheafCongrPreregular Opposite.op functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	preregular
sheafCongrPreregular_inverse_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology CategoryTheory.Sheaf preregular CategoryTheory.ObjectProperty.FullSubcategory.category inverse sheafCongrPreregular Opposite.op functor Opposite.unop	—	preregular
sheafCongrPreregular_unitIso_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.id CategoryTheory.Functor.comp preregular sheafCongr.functor instIsDenseSubsiteRegularTopologyInverse sheafCongr.inverse CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom unitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op inverse functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_unitIso_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.regularTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.comp preregular sheafCongr.functor instIsDenseSubsiteRegularTopologyInverse sheafCongr.inverse CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv unitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op inverse functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	preregular instIsDenseSubsiteRegularTopologyInverse

---

← Back to Index