Documentation

Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Effective epimorphic sieves #

We define the notion of effective epimorphic (pre)sieves and provide some API for relating the notion with the notions of effective epimorphism and effective epimorphic family.

More precisely, if f is a morphism, then f is an effective epi if and only if the sieve it generates is effective epimorphic; see CategoryTheory.Sieve.effectiveEpimorphic_singleton. The analogous statement for a family of morphisms is in the theorem CategoryTheory.Sieve.effectiveEpimorphic_family.

A sieve is effective epimorphic if the associated cocone is a colimit cocone.

Equations
Instances For
    @[reducible, inline]

    A presieve is effective epimorphic if the cocone associated to the sieve it generates is a colimit cocone.

    Equations
    Instances For

      The sieve of morphisms which factor through a given morphism f. This is equal to Sieve.generate (Presieve.singleton f), but has more convenient definitional properties.

      Equations
      Instances For

        Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def CategoryTheory.Sieve.generateFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :

            The sieve of morphisms which factor through a morphism in a given family. This is equal to Sieve.generate (Presieve.ofArrows X π), but has more convenient definitional properties.

            Equations
            Instances For

              Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem CategoryTheory.Sieve.effectiveEpimorphic_family {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) :