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, instPreservesEffectiveEpiFamiliesComp, instPreservesEffectiveEpiFamiliesOfIsEquivalence, instPreservesEffectiveEpisComp, instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks, instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies, instPreservesFiniteEffectiveEpiFamiliesComp, instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies, instReflectsEffectiveEpiFamiliesComp, instReflectsEffectiveEpiFamiliesOfIsEquivalence, instReflectsEffectiveEpisComp, instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies, instReflectsFiniteEffectiveEpiFamiliesComp, instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies, map_effectiveEpi, map_effectiveEpiFamily, map_finite_effectiveEpiFamily, effectiveEpiFamilyStructOfEquivalence_aux, instEffectiveEpiFamilyObjMapOfIsEquivalence	27
Total	34

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	CategoryStruct.comp Category.toCategoryStruct Functor.obj 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	2 math math: instPreservesEffectiveEpiFamiliesComp, instPreservesEffectiveEpiFamiliesOfIsEquivalence
PreservesEffectiveEpis 📖	CompData	6 math math: instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies, Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus, instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks, Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite, instPreservesEffectiveEpisComp, Stonean.instPreservesEffectiveEpisCompHausToCompHaus
PreservesFiniteEffectiveEpiFamilies 📖	CompData	3 math math: instPreservesFiniteEffectiveEpiFamiliesComp, instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies, CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis
ReflectsEffectiveEpiFamilies 📖	CompData	2 math math: instReflectsEffectiveEpiFamiliesComp, instReflectsEffectiveEpiFamiliesOfIsEquivalence
ReflectsEffectiveEpis 📖	CompData	5 math math: Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus, Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite, Stonean.instReflectsEffectiveEpisCompHausToCompHaus, instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies, instReflectsEffectiveEpisComp
ReflectsFiniteEffectiveEpiFamilies 📖	CompData	3 math math: CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis, instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies, instReflectsFiniteEffectiveEpiFamiliesComp

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
instPreservesEffectiveEpiFamiliesComp 📖	mathematical	—	PreservesEffectiveEpiFamilies comp	—	map_effectiveEpiFamily
instPreservesEffectiveEpiFamiliesOfIsEquivalence 📖	mathematical	—	PreservesEffectiveEpiFamilies	—	CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence
instPreservesEffectiveEpisComp 📖	mathematical	—	PreservesEffectiveEpis comp	—	map_effectiveEpi
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
instPreservesFiniteEffectiveEpiFamiliesComp 📖	mathematical	—	PreservesFiniteEffectiveEpiFamilies comp	—	map_finite_effectiveEpiFamily
instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies 📖	mathematical	—	PreservesFiniteEffectiveEpiFamilies	—	map_effectiveEpiFamily
instReflectsEffectiveEpiFamiliesComp 📖	mathematical	—	ReflectsEffectiveEpiFamilies comp	—	effectiveEpiFamily_of_map
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
instReflectsEffectiveEpisComp 📖	mathematical	—	ReflectsEffectiveEpis comp	—	effectiveEpi_of_map
instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies 📖	mathematical	—	ReflectsEffectiveEpis	—	finite_effectiveEpiFamily_of_map Finite.of_fintype CategoryTheory.effectiveEpi_iff_effectiveEpiFamily CategoryTheory.instEffectiveEpiOfEffectiveEpiFamily
instReflectsFiniteEffectiveEpiFamiliesComp 📖	mathematical	—	ReflectsFiniteEffectiveEpiFamilies comp	—	finite_effectiveEpiFamily_of_map
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