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
          theorem CategoryTheory.finitaryExtensive_of_reflective {C : Type u} [Category.{v, u} C] {D : Type u''} [Category.{v'', u''} D] [Limits.HasFiniteCoproducts D] [HasPullbacksOfInclusions D] [FinitaryExtensive C] {Gl : Functor C D} {Gr : Functor D C} (adj : Gl Gr) [Gr.Full] [Gr.Faithful] [∀ (X : D) (Y : C) (f : X Gl.obj Y), Limits.HasPullback (Gr.map f) (adj.unit.app Y)] [∀ (X : D) (Y : C) (f : X Gl.obj Y), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app Y)) Gl] [PreservesPullbacksOfInclusions Gl] :
          instance CategoryTheory.instMonoι {C : Type u} [Category.{v, u} C] [FinitaryExtensive C] {ι : Type u_1} [Finite ι] (X : ιC) (i : ι) :
          instance CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {X Z : C} {α : Type u_1} (f : X Z) {Y : αC} (i : (a : α) → Y a Z) [Finite α] [hi : IsIso (Limits.Sigma.desc i)] (a : α) :
          theorem CategoryTheory.FinitaryPreExtensive.sigma_desc_iso {C : Type u} [Category.{v, u} C] [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} {Z : αC} (π : (a : α) → Z a X) {Y : C} (f : Y X) (hπ : IsIso (Limits.Sigma.desc π)) :
          IsIso (Limits.Sigma.desc fun (x : α) => Limits.pullback.fst f (π x))