Documentation Verification Report

EffectiveEpi

📁 Source: Mathlib/Topology/Category/Profinite/EffectiveEpi.lean

Statistics

Metric	Count
Definitions `profiniteToCompHausEffectivePresentation`	1
Theorems `effectiveEpiFamily_of_jointly_surjective`, `effectiveEpiFamily_tfae`, `effectiveEpi_tfae`, `instEffectivelyEnoughCompHausProfiniteToCompHaus`, `instPreregular`, `instPreservesEffectiveEpisCompHausProfiniteToCompHaus`, `instReflectsEffectiveEpisCompHausProfiniteToCompHaus`	7
Total	8

Profinite

Definitions

Name	Category	Theorems
`profiniteToCompHausEffectivePresentation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpiFamily_of_jointly_surjective` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `ContinuousMap` `CompHausLike.toTop` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.EffectiveEpiFamily`	—	`List.TFAE.out` `CompHausLike.instHasCoproduct` `instHasPropTotallyDisconnectedSpaceCarrier` `instTotallyDisconnectedSpaceSigma` `instTotallyDisconnectedSpaceCarrierToTop` `effectiveEpiFamily_tfae`
`effectiveEpiFamily_tfae` 📖	mathematical	—	`List.TFAE` `CategoryTheory.EffectiveEpiFamily` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Epi` `CategoryTheory.Limits.sigmaObj` `CompHausLike.instHasCoproduct` `instHasPropTotallyDisconnectedSpaceCarrier` `CompHausLike.toTop` `instTopologicalSpaceSigma` `instTotallyDisconnectedSpaceSigma` `instTotallyDisconnectedSpaceCarrierToTop` `CategoryTheory.Limits.Sigma.desc`	—	`CompHausLike.instHasCoproduct` `instHasPropTotallyDisconnectedSpaceCarrier` `instTotallyDisconnectedSpaceSigma` `instTotallyDisconnectedSpaceCarrierToTop` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `List.TFAE.out` `effectiveEpi_tfae` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily` `CompHaus.instHasPropTrue` `CompHaus.effectiveEpiFamily_tfae` `CategoryTheory.Functor.finite_effectiveEpiFamily_of_map` `CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHaus.instHasExplicitPullbacksTrue` `CompHausLike.instPreservesFiniteCoproductsToCompHausLike` `instReflectsEffectiveEpisCompHausProfiniteToCompHaus` `CategoryTheory.Functor.map_finite_effectiveEpiFamily` `CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis` `instPreservesEffectiveEpisCompHausProfiniteToCompHaus` `List.tfae_of_cycle`
`effectiveEpi_tfae` 📖	mathematical	—	`List.TFAE` `CategoryTheory.EffectiveEpi` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Epi` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `CompHausLike.toTop` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	—	`CategoryTheory.epi_of_effectiveEpi` `epi_iff_surjective` `List.tfae_of_cycle`
`instEffectivelyEnoughCompHausProfiniteToCompHaus` 📖	mathematical	—	`CategoryTheory.Functor.EffectivelyEnough` `Profinite` `CompHaus` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `profiniteToCompHaus`	—	—
`instPreregular` 📖	mathematical	—	`CategoryTheory.Preregular` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str`	—	`CategoryTheory.Functor.reflects_preregular` `instPreservesEffectiveEpisCompHausProfiniteToCompHaus` `instReflectsEffectiveEpisCompHausProfiniteToCompHaus` `instEffectivelyEnoughCompHausProfiniteToCompHaus` `CompHaus.instPreregular` `CompHausLike.instFullToCompHausLike` `CompHausLike.instFaithfulToCompHausLike`
`instPreservesEffectiveEpisCompHausProfiniteToCompHaus` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEffectiveEpis` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CompHaus` `profiniteToCompHaus`	—	`List.TFAE.out` `CompHaus.effectiveEpi_tfae` `effectiveEpi_tfae`
`instReflectsEffectiveEpisCompHausProfiniteToCompHaus` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsEffectiveEpis` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CompHaus` `profiniteToCompHaus`	—	`List.TFAE.out` `effectiveEpi_tfae` `CompHaus.effectiveEpi_tfae`

---

← Back to Index