Documentation

Mathlib.CategoryTheory.Extensive

Extensive categories #

Main definitions #

Main Results #

TODO #

Show that the following are finitary extensive:

References #

A category has pullback of inclusions if it has all pullbacks along coproduct injections.

Instances

    A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.

    Instances

      A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.

      Instances

        A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.

        Instances
          Equations
          • One or more equations did not get rendered due to their size.
          instance CategoryTheory.instMonoInl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] (X : C) (Y : C) :
          CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
          Equations
          • =
          instance CategoryTheory.instMonoInr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] (X : C) (Y : C) :
          CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
          Equations
          • =

          (Implementation) An auxiliary lemma for the proof that TopCat is finitary extensive.

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