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_val_app, sheafCongrPrecoherent_counitIso_inv_app_val_app, sheafCongrPrecoherent_functor_map_val_app, sheafCongrPrecoherent_functor_obj_val_map, sheafCongrPrecoherent_functor_obj_val_obj, sheafCongrPrecoherent_inverse_map_val_app, sheafCongrPrecoherent_inverse_obj_val_map, sheafCongrPrecoherent_inverse_obj_val_obj, sheafCongrPrecoherent_unitIso_hom_app_val_app, sheafCongrPrecoherent_unitIso_inv_app_val_app, sheafCongrPreregular_counitIso_hom_app_val_app, sheafCongrPreregular_counitIso_inv_app_val_app, sheafCongrPreregular_functor_map_val_app, sheafCongrPreregular_functor_obj_val_map, sheafCongrPreregular_functor_obj_val_obj, sheafCongrPreregular_inverse_map_val_app, sheafCongrPreregular_inverse_obj_val_map, sheafCongrPreregular_inverse_obj_val_obj, sheafCongrPreregular_unitIso_hom_app_val_app, sheafCongrPreregular_unitIso_inv_app_val_app	30
Total	32

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
sheafCongrPrecoherent 📖	CompOp	10 math math: sheafCongrPrecoherent_counitIso_hom_app_val_app, sheafCongrPrecoherent_functor_obj_val_obj, sheafCongrPrecoherent_functor_obj_val_map, sheafCongrPrecoherent_inverse_map_val_app, sheafCongrPrecoherent_inverse_obj_val_obj, sheafCongrPrecoherent_counitIso_inv_app_val_app, sheafCongrPrecoherent_unitIso_inv_app_val_app, sheafCongrPrecoherent_inverse_obj_val_map, sheafCongrPrecoherent_unitIso_hom_app_val_app, sheafCongrPrecoherent_functor_map_val_app
sheafCongrPreregular 📖	CompOp	10 math math: sheafCongrPreregular_counitIso_inv_app_val_app, sheafCongrPreregular_unitIso_hom_app_val_app, sheafCongrPreregular_inverse_obj_val_map, sheafCongrPreregular_functor_obj_val_obj, sheafCongrPreregular_functor_map_val_app, sheafCongrPreregular_inverse_map_val_app, sheafCongrPreregular_functor_obj_val_map, sheafCongrPreregular_counitIso_hom_app_val_app, sheafCongrPreregular_inverse_obj_val_obj, sheafCongrPreregular_unitIso_inv_app_val_app

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.Sheaf.cond 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.Sheaf.cond 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp inverse op functor CategoryTheory.Sheaf.val CategoryTheory.coherentTopology precoherent CategoryTheory.Functor.id CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafCongr.inverse instIsDenseSubsiteCoherentTopologyInverse sheafCongr.functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_counitIso_inv_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Sheaf.val CategoryTheory.coherentTopology precoherent inverse op functor CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafCongr.inverse instIsDenseSubsiteCoherentTopologyInverse sheafCongr.functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_functor_map_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op inverse CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val precoherent instIsDenseSubsiteCoherentTopologyInverse CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf functor sheafCongrPrecoherent Opposite.op CategoryTheory.Functor.obj Opposite.unop	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_functor_obj_val_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.coherentTopology precoherent CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf functor sheafCongrPrecoherent Opposite.op inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	precoherent
sheafCongrPrecoherent_functor_obj_val_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.coherentTopology precoherent CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf functor sheafCongrPrecoherent Opposite.op inverse Opposite.unop	—	precoherent
sheafCongrPrecoherent_inverse_map_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op functor CategoryTheory.Sheaf.val CategoryTheory.coherentTopology precoherent CategoryTheory.Sheaf.Hom.val instIsDenseSubsiteCoherentTopologyInverse CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf inverse sheafCongrPrecoherent Opposite.op CategoryTheory.Functor.obj Opposite.unop	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_inverse_obj_val_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf precoherent CategoryTheory.Sheaf.instCategorySheaf inverse sheafCongrPrecoherent Opposite.op functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	precoherent
sheafCongrPrecoherent_inverse_obj_val_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf precoherent CategoryTheory.Sheaf.instCategorySheaf inverse sheafCongrPrecoherent Opposite.op functor Opposite.unop	—	precoherent
sheafCongrPrecoherent_unitIso_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Sheaf.val CategoryTheory.coherentTopology functor op inverse CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf precoherent sheafCongr.functor instIsDenseSubsiteCoherentTopologyInverse sheafCongr.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPrecoherent_unitIso_inv_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp functor op inverse CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Functor.id CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf precoherent sheafCongr.functor instIsDenseSubsiteCoherentTopologyInverse sheafCongr.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso sheafCongrPrecoherent CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	precoherent instIsDenseSubsiteCoherentTopologyInverse
sheafCongrPreregular_counitIso_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp inverse op functor CategoryTheory.Sheaf.val CategoryTheory.regularTopology preregular CategoryTheory.Functor.id CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafCongr.inverse instIsDenseSubsiteRegularTopologyInverse sheafCongr.functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_counitIso_inv_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Sheaf.val CategoryTheory.regularTopology preregular inverse op functor CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafCongr.inverse instIsDenseSubsiteRegularTopologyInverse sheafCongr.functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_functor_map_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op inverse CategoryTheory.Sheaf.val CategoryTheory.regularTopology CategoryTheory.Sheaf.Hom.val preregular instIsDenseSubsiteRegularTopologyInverse CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf functor sheafCongrPreregular Opposite.op CategoryTheory.Functor.obj Opposite.unop	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_functor_obj_val_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.regularTopology preregular CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf functor sheafCongrPreregular Opposite.op inverse Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	preregular
sheafCongrPreregular_functor_obj_val_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.regularTopology preregular CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf functor sheafCongrPreregular Opposite.op inverse Opposite.unop	—	preregular
sheafCongrPreregular_inverse_map_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op functor CategoryTheory.Sheaf.val CategoryTheory.regularTopology preregular CategoryTheory.Sheaf.Hom.val instIsDenseSubsiteRegularTopologyInverse CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf inverse sheafCongrPreregular Opposite.op CategoryTheory.Functor.obj Opposite.unop	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_inverse_obj_val_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.regularTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf preregular CategoryTheory.Sheaf.instCategorySheaf inverse sheafCongrPreregular Opposite.op functor Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	preregular
sheafCongrPreregular_inverse_obj_val_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.regularTopology CategoryTheory.Sheaf preregular CategoryTheory.Sheaf.instCategorySheaf inverse sheafCongrPreregular Opposite.op functor Opposite.unop	—	preregular
sheafCongrPreregular_unitIso_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Sheaf.val CategoryTheory.regularTopology functor op inverse CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf preregular sheafCongr.functor instIsDenseSubsiteRegularTopologyInverse sheafCongr.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	preregular instIsDenseSubsiteRegularTopologyInverse
sheafCongrPreregular_unitIso_inv_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp functor op inverse CategoryTheory.Sheaf.val CategoryTheory.regularTopology CategoryTheory.Functor.id CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf preregular sheafCongr.functor instIsDenseSubsiteRegularTopologyInverse sheafCongr.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso sheafCongrPreregular CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	preregular instIsDenseSubsiteRegularTopologyInverse

---

← Back to Index