Preserves

📁 Source: Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

Statistics

Metric	Count
Definitions PreservesEffectiveEpiFamilies, PreservesEffectiveEpis, PreservesFiniteEffectiveEpiFamilies, ReflectsEffectiveEpiFamilies, ReflectsEffectiveEpis, ReflectsFiniteEffectiveEpiFamilies, effectiveEpiFamilyStructOfEquivalence	7
Theorems preserves, preserves, preserves, reflects, reflects, reflects, effectiveEpiFamily_of_map, effectiveEpi_of_map, finite_effectiveEpiFamily_of_map, instPreservesEffectiveEpiFamiliesOfIsEquivalence, instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks, instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies, instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies, instReflectsEffectiveEpiFamiliesOfIsEquivalence, instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies, instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies, map_effectiveEpi, map_effectiveEpiFamily, map_finite_effectiveEpiFamily, effectiveEpiFamilyStructOfEquivalence_aux, instEffectiveEpiFamilyObjMapOfIsEquivalence	21
Total	28

CategoryTheory

Definitions

Name	Category	Theorems
effectiveEpiFamilyStructOfEquivalence 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpiFamilyStructOfEquivalence_aux 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct Functor.obj Equivalence.functor	Equivalence.inverse	—	Functor.map_comp Equivalence.inv_fun_map Category.assoc
instEffectiveEpiFamilyObjMapOfIsEquivalence 📖	mathematical	—	EffectiveEpiFamily Functor.obj Functor.map	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PreservesEffectiveEpiFamilies 📖	CompData	1 math math: instPreservesEffectiveEpiFamiliesOfIsEquivalence
PreservesEffectiveEpis 📖	CompData	5 math math: instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies, Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus, instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks, Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite, Stonean.instPreservesEffectiveEpisCompHausToCompHaus
PreservesFiniteEffectiveEpiFamilies 📖	CompData	2 math math: instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies, CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis
ReflectsEffectiveEpiFamilies 📖	CompData	1 math math: instReflectsEffectiveEpiFamiliesOfIsEquivalence
ReflectsEffectiveEpis 📖	CompData	4 math math: Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus, Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite, Stonean.instReflectsEffectiveEpisCompHausToCompHaus, instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies
ReflectsFiniteEffectiveEpiFamilies 📖	CompData	2 math math: CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis, instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpiFamily_of_map 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily	—	ReflectsEffectiveEpiFamilies.reflects
effectiveEpi_of_map 📖	mathematical	—	CategoryTheory.EffectiveEpi	—	ReflectsEffectiveEpis.reflects
finite_effectiveEpiFamily_of_map 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily	—	ReflectsFiniteEffectiveEpiFamilies.reflects
instPreservesEffectiveEpiFamiliesOfIsEquivalence 📖	mathematical	—	PreservesEffectiveEpiFamilies	—	CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence
instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks 📖	mathematical	—	PreservesEffectiveEpis	—	CategoryTheory.isRegularEpi_iff_effectiveEpi CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.IsRegularEpiCategory.regularEpiOfEpi map_epi CategoryTheory.epi_of_effectiveEpi
instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies 📖	mathematical	—	PreservesEffectiveEpis	—	CategoryTheory.instEffectiveEpiOfEffectiveEpiFamily map_finite_effectiveEpiFamily Finite.of_fintype CategoryTheory.instEffectiveEpiFamily
instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies 📖	mathematical	—	PreservesFiniteEffectiveEpiFamilies	—	map_effectiveEpiFamily
instReflectsEffectiveEpiFamiliesOfIsEquivalence 📖	mathematical	—	ReflectsEffectiveEpiFamilies	—	CategoryTheory.instEffectiveEpiFamilyCompOfIsSplitEpi instIsSplitEpiApp CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom map_effectiveEpiFamily instPreservesEffectiveEpiFamiliesOfIsEquivalence isEquivalence_inv CategoryTheory.instEffectiveEpiFamilyComp inv_fun_map CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.NatIso.inv_app_isIso CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Category.comp_id
instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies 📖	mathematical	—	ReflectsEffectiveEpis	—	finite_effectiveEpiFamily_of_map Finite.of_fintype CategoryTheory.effectiveEpi_iff_effectiveEpiFamily CategoryTheory.instEffectiveEpiOfEffectiveEpiFamily
instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies 📖	mathematical	—	ReflectsFiniteEffectiveEpiFamilies	—	effectiveEpiFamily_of_map
map_effectiveEpi 📖	mathematical	—	CategoryTheory.EffectiveEpi obj map	—	PreservesEffectiveEpis.preserves
map_effectiveEpiFamily 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily obj map	—	PreservesEffectiveEpiFamilies.preserves
map_finite_effectiveEpiFamily 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily obj map	—	PreservesFiniteEffectiveEpiFamilies.preserves

CategoryTheory.Functor.PreservesEffectiveEpiFamilies

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—

CategoryTheory.Functor.PreservesEffectiveEpis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.EffectiveEpi CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—

CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—

CategoryTheory.Functor.ReflectsEffectiveEpiFamilies

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily	—	—

CategoryTheory.Functor.ReflectsEffectiveEpis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.EffectiveEpi	—	—

CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflects 📖	mathematical	—	CategoryTheory.EffectiveEpiFamily	—	—

---

← Back to Index