Documentation Verification Report

EpiMono

📁 Source: Mathlib/CategoryTheory/Sites/EpiMono.lean

Statistics

Metric	Count
Definitions `functorialLocallySurjectiveInjectiveFactorization`, `locallyInjective`, `locallySurjective`	3
Theorems `instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instHasFunctorialFactorizationLocallySurjectiveLocallyInjective`, `instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `isLocallySurjective_iff_epi'`	6
Total	9

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`functorialLocallySurjectiveInjectiveFactorization` 📖	CompOp	4 math math: `instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`
`locallyInjective` 📖	CompOp	5 math math: `instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instHasFunctorialFactorizationLocallySurjectiveLocallyInjective`, `instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`
`locallySurjective` 📖	CompOp	5 math math: `instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instHasFunctorialFactorizationLocallySurjectiveLocallyInjective`, `instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`, `instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Sheaf` `instCategorySheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.Arrow.leftFunc` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z` `locallySurjective` `locallyInjective` `functorialLocallySurjectiveInjectiveFactorization` `CategoryTheory.NatTrans.app` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.i`	—	`epi_of_isLocallySurjective` `instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`
`instHasFunctorialFactorizationLocallySurjectiveLocallyInjective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFunctorialFactorization` `CategoryTheory.Sheaf` `instCategorySheaf` `locallySurjective` `locallyInjective`	—	—
`instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization` 📖	mathematical	—	`IsLocallyInjective` `CategoryTheory.Functor.obj` `CategoryTheory.Arrow` `CategoryTheory.Sheaf` `instCategorySheaf` `CategoryTheory.instCategoryArrow` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z` `locallySurjective` `locallyInjective` `functorialLocallySurjectiveInjectiveFactorization` `CategoryTheory.Arrow.rightFunc` `CategoryTheory.NatTrans.app` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.p`	—	`CategoryTheory.MorphismProperty.FunctorialFactorizationData.hp`
`instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization` 📖	mathematical	—	`IsLocallySurjective` `CategoryTheory.Functor.obj` `CategoryTheory.Arrow` `CategoryTheory.Sheaf` `instCategorySheaf` `CategoryTheory.instCategoryArrow` `CategoryTheory.Arrow.leftFunc` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z` `locallySurjective` `locallyInjective` `functorialLocallySurjectiveInjectiveFactorization` `CategoryTheory.NatTrans.app` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.i`	—	`CategoryTheory.MorphismProperty.FunctorialFactorizationData.hi`
`instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Sheaf` `instCategorySheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.Z` `locallySurjective` `locallyInjective` `functorialLocallySurjectiveInjectiveFactorization` `CategoryTheory.Arrow.rightFunc` `CategoryTheory.NatTrans.app` `CategoryTheory.MorphismProperty.FunctorialFactorizationData.p`	—	`mono_of_isLocallyInjective` `instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization`
`isLocallySurjective_iff_epi'` 📖	mathematical	—	`IsLocallySurjective` `CategoryTheory.Epi` `CategoryTheory.Sheaf` `instCategorySheaf`	—	`epi_of_isLocallySurjective` `CategoryTheory.MorphismProperty.instHasFactorizationOfHasFunctorialFactorization` `instHasFunctorialFactorizationLocallySurjectiveLocallyInjective` `CategoryTheory.instHasWeakSheafifyOfHasSheafify` `CategoryTheory.MorphismProperty.MapFactorizationData.hi` `CategoryTheory.MorphismProperty.MapFactorizationData.hp` `CategoryTheory.epi_of_epi_fac` `CategoryTheory.MorphismProperty.MapFactorizationData.fac` `mono_of_isLocallyInjective` `CategoryTheory.isIso_of_mono_of_epi` `isLocallySurjective_comp` `isLocallySurjective_of_iso`

---

← Back to Index