Theorems · Definition · category theory

CompHausLike.effectiveEpiStruct

{P : TopCat → Prop} →
  {B X : CompHausLike P} →
    (π : X ⟶ B) → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π) → CategoryTheory.EffectiveEpiStruct π

If π is a surjective morphism in CompHausLike P, then it is an effective epi.

Defined in: Mathlib.Topology.Category.CompHausLike.EffectiveEpi
Cited by: 5 results in Mathlib
Foundations: Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
TopCat.carrierstatement · cited by 3,184
ContinuousMapstatement · cited by 2,491
TopCatstatement and proof · cited by 1,889
CategoryTheory.InducedCategory.Hom.homproof · cited by 850
CompHausLike.toTopstatement · cited by 258
TopCat.Hom.homproof · cited by 169
CompHausLikestatement and proof · cited by 145
CompHausLike.ofHomproof · cited by 11

Cited by5

Results whose statement or proof uses this declaration.

CompHausLike.preregularproof · cited by 19
CompHaus.effectiveEpi_tfaeproof · cited by 2
LightProfinite.effectiveEpi_iff_surjectiveproof · cited by 1
Stonean.effectiveEpi_tfaeproof · cited by 1
Profinite.effectiveEpi_tfaeproof · cited by 1