Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `desc`, `getStruct`, `EffectiveEpiFamily`, `desc`, `getStruct`, `EffectiveEpiFamilyStruct`, `desc`, `reindex`, `EffectiveEpiStruct`, `desc`, `effectiveEpiFamilyStructOfIsIsoDesc`, `effectiveEpiFamilyStructSingletonOfEffectiveEpi`, `effectiveEpiStructOfEffectiveEpiFamilySingleton`, `effectiveEpiStructOfIsIso`	14
Theorems `effectiveEpi`, `fac`, `fac_assoc`, `uniq`, `effectiveEpiFamily`, `fac`, `fac_assoc`, `hom_ext`, `reindex`, `uniq`, `fac`, `uniq`, `fac`, `uniq`, `effectiveEpi_iff_effectiveEpiFamily`, `epiOfEffectiveEpi`, `epi_of_effectiveEpi`, `instEffectiveEpiFamily`, `instEffectiveEpiFamilyOfIsIsoDesc`, `instEffectiveEpiOfEffectiveEpiFamily`, `instEffectiveEpiOfIsIso`, `strongEpi_of_effectiveEpi`	22
Total	36

CategoryTheory

Definitions

Name	Category	Theorems
`EffectiveEpiFamily` 📖	CompData	28 math math: `effectiveEpiFamily_of_effectiveEpi_epi_comp`, `instEffectiveEpiFamilyCompOfIsSplitEpi`, `Functor.PreservesFiniteEffectiveEpiFamilies.preserves`, `Functor.PreservesEffectiveEpiFamilies.preserves`, `Functor.finite_effectiveEpiFamily_of_map`, `Stonean.effectiveEpiFamily_tfae`, `precoherentEffectiveEpiFamilyCompEffectiveEpis`, `Functor.ReflectsEffectiveEpiFamilies.reflects`, `Functor.map_effectiveEpiFamily`, `coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily`, `Functor.map_finite_effectiveEpiFamily`, `Functor.ReflectsFiniteEffectiveEpiFamilies.reflects`, `Functor.effectiveEpiFamily_of_map`, `effectiveEpi_desc_iff_effectiveEpiFamily`, `instEffectiveEpiFamilyOfIsIsoDesc`, `Sieve.effectiveEpimorphic_family`, `EffectiveEpiFamily.reindex`, `CompHaus.effectiveEpiFamily_of_jointly_surjective`, `Precoherent.pullback`, `instEffectiveEpiFamilyObjMapOfIsEquivalence`, `coherentTopology.exists_effectiveEpiFamily_iff_mem_induced`, `Stonean.effectiveEpiFamily_of_jointly_surjective`, `effectiveEpi_iff_effectiveEpiFamily`, `CompHaus.effectiveEpiFamily_tfae`, `Profinite.effectiveEpiFamily_tfae`, `instEffectiveEpiFamily`, `instEffectiveEpiFamilyComp`, `Profinite.effectiveEpiFamily_of_jointly_surjective`
`EffectiveEpiFamilyStruct` 📖	CompData	1 math math: `EffectiveEpiFamily.effectiveEpiFamily`
`EffectiveEpiStruct` 📖	CompData	1 math math: `EffectiveEpi.effectiveEpi`
`effectiveEpiFamilyStructOfIsIsoDesc` 📖	CompOp	—
`effectiveEpiFamilyStructSingletonOfEffectiveEpi` 📖	CompOp	—
`effectiveEpiStructOfEffectiveEpiFamilySingleton` 📖	CompOp	—
`effectiveEpiStructOfIsIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpi_iff_effectiveEpiFamily` 📖	mathematical	—	`EffectiveEpi` `EffectiveEpiFamily` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	`instEffectiveEpiFamily` `instEffectiveEpiOfEffectiveEpiFamily`
`epiOfEffectiveEpi` 📖	mathematical	—	`Epi`	—	`epi_of_effectiveEpi`
`epi_of_effectiveEpi` 📖	mathematical	—	`Epi`	—	`EffectiveEpi.uniq`
`instEffectiveEpiFamily` 📖	mathematical	—	`EffectiveEpiFamily` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	—
`instEffectiveEpiFamilyOfIsIsoDesc` 📖	mathematical	—	`EffectiveEpiFamily`	—	—
`instEffectiveEpiOfEffectiveEpiFamily` 📖	mathematical	—	`EffectiveEpi`	—	—
`instEffectiveEpiOfIsIso` 📖	mathematical	—	`EffectiveEpi`	—	—
`strongEpi_of_effectiveEpi` 📖	mathematical	—	`StrongEpi`	—	`StrongEpi.mk'` `epi_of_effectiveEpi` `Category.assoc` `CommSq.w` `eq_whisker` `CommSq.HasLift.mk'` `EffectiveEpi.fac` `cancel_epi` `EffectiveEpi.fac_assoc`

CategoryTheory.EffectiveEpi

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	3 math math: `fac_assoc`, `uniq`, `fac`
`getStruct` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpi` 📖	mathematical	—	`CategoryTheory.EffectiveEpiStruct`	—	—
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	`CategoryTheory.EffectiveEpiStruct.fac`
`fac_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	`CategoryTheory.EffectiveEpiStruct.uniq`

CategoryTheory.EffectiveEpiFamily

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	3 math math: `uniq`, `fac`, `fac_assoc`
`getStruct` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpiFamily` 📖	mathematical	—	`CategoryTheory.EffectiveEpiFamilyStruct`	—	—
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	`CategoryTheory.EffectiveEpiFamilyStruct.fac`
`fac_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—	`uniq`
`reindex` 📖	mathematical	—	`CategoryTheory.EffectiveEpiFamily`	—	—
`uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	`CategoryTheory.EffectiveEpiFamilyStruct.uniq`

CategoryTheory.EffectiveEpiFamilyStruct

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	2 math math: `fac`, `uniq`
`reindex` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	—
`uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	—

CategoryTheory.EffectiveEpiStruct

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	2 math math: `fac`, `uniq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	—
`uniq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`desc`	—	—

---

← Back to Index