Documentation

Mathlib.CategoryTheory.Extensive

Extensive categories #

Main definitions #

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

Main Results #

CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive: The initial object in extensive categories is strict.
CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit: Coproduct injections are monic in extensive categories.
CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen: In extensive categories, sums are disjoint, i.e. the pullback of X ⟶ X ⨿ Y and Y ⟶ X ⨿ Y is the initial object.
CategoryTheory.types.finitaryExtensive: The category of types is extensive.
CategoryTheory.FinitaryExtensive_TopCat: The category Top is extensive.
CategoryTheory.FinitaryExtensive_functor: The category C ⥤ D is extensive if D has all pullbacks and is extensive.
CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts: Finite coproducts in a finitary extensive category are van Kampen.

TODO #

Show that the following are finitary extensive:

Scheme
AffineScheme (CommRingᵒᵖ)

References #

https://ncatlab.org/nlab/show/extensive+category
[Carboni et al, Introduction to extensive and distributive categories][CARBONI1993145]

class CategoryTheory.HasPullbacksOfInclusions (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] :

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

hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f

Instances

theorem CategoryTheory.HasPullbacksOfInclusions.hasPullbackInl {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.HasPullbacksOfInclusions C] {X Y Z : C} (f : Z ⟶ X ⨿ Y), CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f

class CategoryTheory.PreservesPullbacksOfInclusions {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] :

Type (max (max (max u_1 u_2) u_3) u_4)

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

preservesPullbackInl : {X Y Z : C} → (f : Z ⟶ X ⨿ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inl f) F

Instances

class CategoryTheory.FinitaryPreExtensive (C : Type u) [CategoryTheory.Category.{v, u} C] :

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

hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C
hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C
universal' : ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsUniversalColimit c
In a finitary extensive category, all coproducts are van Kampen

Instances

theorem CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C], CategoryTheory.Limits.HasFiniteCoproducts C

theorem CategoryTheory.FinitaryPreExtensive.hasPullbacksOfInclusions {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C], CategoryTheory.HasPullbacksOfInclusions C

theorem CategoryTheory.FinitaryPreExtensive.universal' {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsUniversalColimit c

In a finitary extensive category, all coproducts are van Kampen

class CategoryTheory.FinitaryExtensive (C : Type u) [CategoryTheory.Category.{v, u} C] :

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

hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C
hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C
van_kampen' : ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsVanKampenColimit c
In a finitary extensive category, all coproducts are van Kampen

Instances

theorem CategoryTheory.FinitaryExtensive.hasFiniteCoproducts {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C], CategoryTheory.Limits.HasFiniteCoproducts C

theorem CategoryTheory.FinitaryExtensive.hasPullbacksOfInclusions {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C], CategoryTheory.HasPullbacksOfInclusions C

theorem CategoryTheory.FinitaryExtensive.van_kampen' {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsVanKampenColimit c

In a finitary extensive category, all coproducts are van Kampen

theorem CategoryTheory.FinitaryExtensive.vanKampen {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.IsVanKampenColimit c

@[instance 100]

instance CategoryTheory.HasPullbacksOfInclusions.instOfHasPullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPullbacks C] :

CategoryTheory.HasPullbacksOfInclusions C

Equations

⋯ = ⋯

instance CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] {X : C} {Y : C} {Z : C} (f : Z ⟶ X ⨿ Y) :

CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.coprod.inl

Equations

⋯ = ⋯

instance CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] {X : C} {Y : C} {Z : C} (f : Z ⟶ X ⨿ Y) :

CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.coprod.inr

Equations

⋯ = ⋯

instance CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] {X : C} {Y : C} {Z : C} (f : Z ⟶ X ⨿ Y) :

CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inr f

Equations

⋯ = ⋯

@[instance 100]

noncomputable instance CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] :

CategoryTheory.PreservesPullbacksOfInclusions F

Equations

CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan F = CategoryTheory.PreservesPullbacksOfInclusions.mk

noncomputable instance CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.PreservesPullbacksOfInclusions F] {X : C} {Y : C} {Z : C} (f : Z ⟶ X ⨿ Y) :

CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inl) F

Equations

CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' F f = CategoryTheory.Limits.preservesPullbackSymmetry F CategoryTheory.Limits.coprod.inl f

noncomputable instance CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.PreservesPullbacksOfInclusions F] {X : C} {Y : C} {Z : C} (f : Z ⟶ X ⨿ Y) :

CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inr) F

Equations

One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D) [CategoryTheory.PreservesPullbacksOfInclusions F] {X : C} {Y : C} {Z : C} (f : Z ⟶ X ⨿ Y) :

CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inr f) F

Equations

CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr F f = CategoryTheory.Limits.preservesPullbackSymmetry F f CategoryTheory.Limits.coprod.inr

@[instance 100]

instance CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] :

CategoryTheory.FinitaryPreExtensive C

Equations

⋯ = ⋯

theorem CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.Mono c.inr

theorem CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.Mono c.inl

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

⋯ = ⋯

theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr

@[instance 100]

instance CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] :

CategoryTheory.Limits.HasStrictInitialObjects C

Equations

⋯ = ⋯

theorem CategoryTheory.finitaryExtensive_iff_of_isTerminal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] (T : C) (HT : CategoryTheory.Limits.IsTerminal T) (c₀ : CategoryTheory.Limits.BinaryCofan T T) (hc₀ : CategoryTheory.Limits.IsColimit c₀) :

CategoryTheory.FinitaryExtensive C ↔ CategoryTheory.IsVanKampenColimit c₀

instance CategoryTheory.types.finitaryExtensive :

CategoryTheory.FinitaryExtensive (Type u)

Equations

CategoryTheory.types.finitaryExtensive = ⋯

noncomputable def CategoryTheory.finitaryExtensiveTopCatAux (Z : TopCat) (f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1} )) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1} ).binaryCofan (TopCat.of PUnit.{u + 1} )).inl) (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1} ).binaryCofan (TopCat.of PUnit.{u + 1} )).inr))

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

Equations

CategoryTheory.finitaryExtensiveTopCatAux Z f = ⋯.some

Instances For

instance CategoryTheory.finitaryExtensive_TopCat :

CategoryTheory.FinitaryExtensive TopCat

Equations

CategoryTheory.finitaryExtensive_TopCat = ⋯

theorem CategoryTheory.finitaryExtensive_of_reflective {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteCoproducts D] [CategoryTheory.HasPullbacksOfInclusions D] [CategoryTheory.FinitaryExtensive C] {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] [∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app Y)] [(X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app Y)) Gl] [CategoryTheory.PreservesPullbacksOfInclusions Gl] :

CategoryTheory.FinitaryExtensive D

instance CategoryTheory.finitaryExtensive_functor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.FinitaryExtensive C] :

CategoryTheory.FinitaryExtensive (CategoryTheory.Functor D C)

Equations

⋯ = ⋯

noncomputable instance CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso f] :

CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F

Equations

One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.IsIso g] :

CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F

Equations

CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1 F f g = CategoryTheory.Limits.preservesPullbackSymmetry F g f

theorem CategoryTheory.finitaryExtensive_of_preserves_and_reflects_isomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] (F : CategoryTheory.Functor C D) [CategoryTheory.FinitaryExtensive D] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [F.ReflectsIsomorphisms] :

CategoryTheory.FinitaryExtensive C

theorem CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {n : ℕ} {F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.IsUniversalColimit c

theorem CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1} [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.IsUniversalColimit c

theorem CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {n : ℕ} {F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.IsVanKampenColimit c

theorem CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) :

CategoryTheory.IsVanKampenColimit c

theorem CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1} [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (i : CategoryTheory.Discrete ι) {X : C} (g : X ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete ι)).obj c.pt).obj i) :

CategoryTheory.Limits.HasPullback g (c.ι.app i)

theorem CategoryTheory.FinitaryExtensive.mono_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (i : CategoryTheory.Discrete ι) :

CategoryTheory.Mono (c.ι.app i)

instance CategoryTheory.instMonoι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι] (X : ι → C) (i : ι) :

CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)

Equations

⋯ = ⋯

theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (i : CategoryTheory.Discrete ι) (j : CategoryTheory.Discrete ι) (e : i ≠ j) :

CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i)) (CategoryTheory.Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι] (X : ι → C) (i : ι) (j : ι) (e : i ≠ j) :

CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j)

instance CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} {Z : C} {α : Type u_1} (f : X ⟶ Z) {Y : α → C} (i : (a : α) → Y a ⟶ Z) [Finite α] [hi : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc i)] (a : α) :

CategoryTheory.Limits.HasPullback f (i a)

Equations

⋯ = ⋯

theorem CategoryTheory.FinitaryPreExtensive.sigma_desc_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)) :

CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun (x : α) => CategoryTheory.Limits.pullback.fst f (π x))