Documentation

Mathlib.Topology.Category.Stonean.EffectiveEpi

Effective epimorphisms in Stonean #

This file proves that EffectiveEpi, Epi and Surjective are all equivalent in Stonean. As a consequence we deduce from the material in Mathlib.Topology.Category.CompHausLike.EffectiveEpi that Stonean is Preregular and Precoherent.

We also prove that for a finite family of morphisms in Stonean with fixed target, the conditions jointly surjective, jointly epimorphic and effective epimorphic are all equivalent.

source
theorem Stonean.effectiveEpi_tfae {B : Stonean} {X : Stonean} (π : X ⟶ B) :
[CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑π].TFAE
source
instance Stonean.instPreservesEffectiveEpisCompHausToCompHaus :
Stonean.toCompHaus.PreservesEffectiveEpis
Equations
source
instance Stonean.instReflectsEffectiveEpisCompHausToCompHaus :
Stonean.toCompHaus.ReflectsEffectiveEpis
Equations
source
noncomputable def Stonean.stoneanToCompHausEffectivePresentation (X : CompHaus) :
Stonean.toCompHaus.EffectivePresentation X

An effective presentation of an X : CompHaus with respect to the inclusion functor from Stonean

Equations
Instances For
    source
    instance Stonean.instEffectivelyEnoughCompHausToCompHaus :
    Stonean.toCompHaus.EffectivelyEnough
    Equations
    source
    instance Stonean.instPreregular :
    CategoryTheory.Preregular Stonean
    Equations
    source
    theorem Stonean.effectiveEpiFamily_tfae {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) :
    [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (π a) x = b].TFAE
    source
    theorem Stonean.effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (π a) x = b) :
    CategoryTheory.EffectiveEpiFamily X π