Documentation

Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Effective epimorphic families and coproducts #

This file proves that an effective epimorphic family induces an effective epi from the coproduct if the coproduct exists, and the converse under some more conditions on the coproduct (that it interacts well with pullbacks).

Given an EffectiveEpiFamily X π and a corresponding coproduct cocone, the family descends to an EffectiveEpi from the coproduct.

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

    Given an EffectiveEpiFamily X π such that the coproduct of X exists, Sigma.desc π is an EffectiveEpi.

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

      This is an auxiliary lemma used twice in the definition of EffectiveEpiFamilyOfEffectiveEpiDesc. It is the h hypothesis of EffectiveEpi.desc and EffectiveEpi.fac.

      If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of the coproduct is effective epimorphic whenever Sigma.desc induces an effective epimorphism from the coproduct itself.

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