Documentation

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Multi-(co)equalizers #

A multiequalizer is an equalizer of two morphisms between two products. Since both products and equalizers are limits, such an object is again a limit. This file provides the diagram whose limit is indeed such an object. In fact, it is well-known that any limit can be obtained as a multiequalizer. The dual construction (multicoequalizers) is also provided.

Projects #

Prove that a multiequalizer can be identified with an equalizer between products (and analogously for multicoequalizers).

Prove that the limit of any diagram is a multiequalizer (and similarly for colimits).

inductive CategoryTheory.Limits.WalkingMulticospan {L : Type w} {R : Type w} (fst : R → L) (snd : R → L) :

The type underlying the multiequalizer diagram.

left: {L R : Type w} → {fst snd : R → L} → L → CategoryTheory.Limits.WalkingMulticospan fst snd
right: {L R : Type w} → {fst snd : R → L} → R → CategoryTheory.Limits.WalkingMulticospan fst snd

Instances For

inductive CategoryTheory.Limits.WalkingMultispan {L : Type w} {R : Type w} (fst : L → R) (snd : L → R) :

The type underlying the multiecoqualizer diagram.

left: {L R : Type w} → {fst snd : L → R} → L → CategoryTheory.Limits.WalkingMultispan fst snd
right: {L R : Type w} → {fst snd : L → R} → R → CategoryTheory.Limits.WalkingMultispan fst snd

Instances For

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedWalkingMulticospan {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} [Inhabited L] :

Inhabited (CategoryTheory.Limits.WalkingMulticospan fst snd)

Equations

CategoryTheory.Limits.WalkingMulticospan.instInhabitedWalkingMulticospan = { default := CategoryTheory.Limits.WalkingMulticospan.left default }

inductive CategoryTheory.Limits.WalkingMulticospan.Hom {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} :

CategoryTheory.Limits.WalkingMulticospan fst snd → CategoryTheory.Limits.WalkingMulticospan fst snd → Type w

Morphisms for WalkingMulticospan.

id: {L R : Type w} → {fst snd : R → L} → (A : CategoryTheory.Limits.WalkingMulticospan fst snd) → CategoryTheory.Limits.WalkingMulticospan.Hom A A
fst: {L R : Type w} → {fst snd : R → L} → (b : R) → CategoryTheory.Limits.WalkingMulticospan.Hom (CategoryTheory.Limits.WalkingMulticospan.left (fst b)) (CategoryTheory.Limits.WalkingMulticospan.right b)
snd: {L R : Type w} → {fst snd : R → L} → (b : R) → CategoryTheory.Limits.WalkingMulticospan.Hom (CategoryTheory.Limits.WalkingMulticospan.left (snd b)) (CategoryTheory.Limits.WalkingMulticospan.right b)

Instances For

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} {a : CategoryTheory.Limits.WalkingMulticospan fst snd} :

Inhabited (CategoryTheory.Limits.WalkingMulticospan.Hom a a)

Equations

CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom = { default := CategoryTheory.Limits.WalkingMulticospan.Hom.id a }

def CategoryTheory.Limits.WalkingMulticospan.Hom.comp {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} {A : CategoryTheory.Limits.WalkingMulticospan fst snd} {B : CategoryTheory.Limits.WalkingMulticospan fst snd} {C : CategoryTheory.Limits.WalkingMulticospan fst snd} :

CategoryTheory.Limits.WalkingMulticospan.Hom A B → CategoryTheory.Limits.WalkingMulticospan.Hom B C → CategoryTheory.Limits.WalkingMulticospan.Hom A C

Composition of morphisms for WalkingMulticospan.

Equations

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

Instances For

instance CategoryTheory.Limits.WalkingMulticospan.instSmallCategoryWalkingMulticospan {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} :

CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMulticospan fst snd)

Equations

CategoryTheory.Limits.WalkingMulticospan.instSmallCategoryWalkingMulticospan = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.Hom.id_eq_id {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} (X : CategoryTheory.Limits.WalkingMulticospan fst snd) :

CategoryTheory.Limits.WalkingMulticospan.Hom.id X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.Hom.comp_eq_comp {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} {X : CategoryTheory.Limits.WalkingMulticospan fst snd} {Y : CategoryTheory.Limits.WalkingMulticospan fst snd} {Z : CategoryTheory.Limits.WalkingMulticospan fst snd} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Limits.WalkingMulticospan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

instance CategoryTheory.Limits.WalkingMultispan.instInhabitedWalkingMultispan {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} [Inhabited L] :

Inhabited (CategoryTheory.Limits.WalkingMultispan fst snd)

Equations

CategoryTheory.Limits.WalkingMultispan.instInhabitedWalkingMultispan = { default := CategoryTheory.Limits.WalkingMultispan.left default }

inductive CategoryTheory.Limits.WalkingMultispan.Hom {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} :

CategoryTheory.Limits.WalkingMultispan fst snd → CategoryTheory.Limits.WalkingMultispan fst snd → Type v

Morphisms for WalkingMultispan.

id: {L R : Type v} → {fst snd : L → R} → (A : CategoryTheory.Limits.WalkingMultispan fst snd) → CategoryTheory.Limits.WalkingMultispan.Hom A A
fst: {L R : Type v} → {fst snd : L → R} → (a : L) → CategoryTheory.Limits.WalkingMultispan.Hom (CategoryTheory.Limits.WalkingMultispan.left a) (CategoryTheory.Limits.WalkingMultispan.right (fst a))
snd: {L R : Type v} → {fst snd : L → R} → (a : L) → CategoryTheory.Limits.WalkingMultispan.Hom (CategoryTheory.Limits.WalkingMultispan.left a) (CategoryTheory.Limits.WalkingMultispan.right (snd a))

Instances For

instance CategoryTheory.Limits.WalkingMultispan.instInhabitedHom {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} {a : CategoryTheory.Limits.WalkingMultispan fst snd} :

Inhabited (CategoryTheory.Limits.WalkingMultispan.Hom a a)

Equations

CategoryTheory.Limits.WalkingMultispan.instInhabitedHom = { default := CategoryTheory.Limits.WalkingMultispan.Hom.id a }

def CategoryTheory.Limits.WalkingMultispan.Hom.comp {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} {A : CategoryTheory.Limits.WalkingMultispan fst snd} {B : CategoryTheory.Limits.WalkingMultispan fst snd} {C : CategoryTheory.Limits.WalkingMultispan fst snd} :

CategoryTheory.Limits.WalkingMultispan.Hom A B → CategoryTheory.Limits.WalkingMultispan.Hom B C → CategoryTheory.Limits.WalkingMultispan.Hom A C

Composition of morphisms for WalkingMultispan.

Equations

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

Instances For

instance CategoryTheory.Limits.WalkingMultispan.instSmallCategoryWalkingMultispan {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} :

CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMultispan fst snd)

Equations

CategoryTheory.Limits.WalkingMultispan.instSmallCategoryWalkingMultispan = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} (X : CategoryTheory.Limits.WalkingMultispan fst snd) :

CategoryTheory.Limits.WalkingMultispan.Hom.id X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.comp_eq_comp {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} {X : CategoryTheory.Limits.WalkingMultispan fst snd} {Y : CategoryTheory.Limits.WalkingMultispan fst snd} {Z : CategoryTheory.Limits.WalkingMultispan fst snd} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Limits.WalkingMultispan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

structure CategoryTheory.Limits.MulticospanIndex (C : Type u) [CategoryTheory.Category.{v, u} C] :

Type (max (max u v) (w + 1))

This is a structure encapsulating the data necessary to define a Multicospan.

L : Type w
R : Type w
fstTo : self.R → self.L
sndTo : self.R → self.L
left : self.L → C
right : self.R → C
fst : (b : self.R) → self.left (self.fstTo b) ⟶ self.right b
snd : (b : self.R) → self.left (self.sndTo b) ⟶ self.right b

Instances For

structure CategoryTheory.Limits.MultispanIndex (C : Type u) [CategoryTheory.Category.{v, u} C] :

Type (max (max u v) (w + 1))

This is a structure encapsulating the data necessary to define a Multispan.

L : Type w
R : Type w
fstFrom : self.L → self.R
sndFrom : self.L → self.R
left : self.L → C
right : self.R → C
fst : (a : self.L) → self.left a ⟶ self.right (self.fstFrom a)
snd : (a : self.L) → self.left a ⟶ self.right (self.sndFrom a)

Instances For

def CategoryTheory.Limits.MulticospanIndex.multicospan {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) :

CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) C

The multicospan associated to I : MulticospanIndex.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (a : I.L) :

(CategoryTheory.Limits.MulticospanIndex.multicospan I).obj (CategoryTheory.Limits.WalkingMulticospan.left a) = I.left a

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (b : I.R) :

(CategoryTheory.Limits.MulticospanIndex.multicospan I).obj (CategoryTheory.Limits.WalkingMulticospan.right b) = I.right b

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (b : I.R) :

(CategoryTheory.Limits.MulticospanIndex.multicospan I).map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst b) = I.fst b

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (b : I.R) :

(CategoryTheory.Limits.MulticospanIndex.multicospan I).map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd b) = I.snd b

noncomputable def CategoryTheory.Limits.MulticospanIndex.fstPiMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

∏ I.left ⟶ ∏ I.right

The induced map ∏ I.left ⟶ ∏ I.right via I.fst.

Equations

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

Instances For

noncomputable def CategoryTheory.Limits.MulticospanIndex.sndPiMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

∏ I.left ⟶ ∏ I.right

The induced map ∏ I.left ⟶ ∏ I.right via I.snd.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.fstTo b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.fstTo b)) (I.fst b)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.sndPiMap I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.sndPiMap I) (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y), (CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram I).map h = match X, Y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ I.right) | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.left => CategoryTheory.Limits.MulticospanIndex.fstPiMap I | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.right => CategoryTheory.Limits.MulticospanIndex.sndPiMap I

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (x : CategoryTheory.Limits.WalkingParallelPair) :

(CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram I).obj x = match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ I.right

noncomputable def CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C

Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over the two morphsims ∏ I.left ⇉ ∏ I.right. This is the diagram of the latter.

Equations

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

Instances For

def CategoryTheory.Limits.MultispanIndex.multispan {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) :

CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom) C

The multispan associated to I : MultispanIndex.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) :

(CategoryTheory.Limits.MultispanIndex.multispan I).obj (CategoryTheory.Limits.WalkingMultispan.left a) = I.left a

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (b : I.R) :

(CategoryTheory.Limits.MultispanIndex.multispan I).obj (CategoryTheory.Limits.WalkingMultispan.right b) = I.right b

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) :

(CategoryTheory.Limits.MultispanIndex.multispan I).map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) = I.fst a

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) :

(CategoryTheory.Limits.MultispanIndex.multispan I).map (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) = I.snd a

noncomputable def CategoryTheory.Limits.MultispanIndex.fstSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

∐ I.left ⟶ ∐ I.right

The induced map ∐ I.left ⟶ ∐ I.right via I.fst.

Equations

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

Instances For

noncomputable def CategoryTheory.Limits.MultispanIndex.sndSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

∐ I.left ⟶ ∐ I.right

The induced map ∐ I.left ⟶ ∐ I.right via I.snd.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) {Z : C} (h : ∐ I.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) h) = CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (I.fstFrom b)) h)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) = CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.Limits.Sigma.ι I.right (I.fstFrom b))

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) {Z : C} (h : ∐ I.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) h) = CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (I.sndFrom b)) h)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) = CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.Limits.Sigma.ι I.right (I.sndFrom b))

@[inline, reducible]

noncomputable abbrev CategoryTheory.Limits.MultispanIndex.parallelPairDiagram {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C

Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer over the two morphsims ∐ I.left ⇉ ∐ I.right. This is the diagram of the latter.

Equations

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

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.Multifork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) :

Type (max (max w u) v)

A multifork is a cone over a multicospan.

Equations

CategoryTheory.Limits.Multifork I = CategoryTheory.Limits.Cone (CategoryTheory.Limits.MulticospanIndex.multicospan I)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.Multicofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) :

Type (max (max w u) v)

A multicofork is a cocone over a multispan.

Equations

CategoryTheory.Limits.Multicofork I = CategoryTheory.Limits.Cocone (CategoryTheory.Limits.MultispanIndex.multispan I)

Instances For

def CategoryTheory.Limits.Multifork.ι {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (a : I.L) :

K.pt ⟶ I.left a

The maps from the cone point of a multifork to the objects on the left.

Equations

CategoryTheory.Limits.Multifork.ι K a = K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.app_left_eq_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (a : I.L) :

K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.Limits.Multifork.ι K a

@[simp]

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) :

K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.fstTo b)) (I.fst b)

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) {Z : C} (h : (CategoryTheory.Limits.MulticospanIndex.multicospan I).obj (CategoryTheory.Limits.WalkingMulticospan.right b) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) :

K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.Multifork.hom_comp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K₁ : CategoryTheory.Limits.Multifork I) (K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : I.L) {Z : C} (h : I.left j ⟶ Z) :

CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K₂ j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K₁ j) h

@[simp]

theorem CategoryTheory.Limits.Multifork.hom_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K₁ : CategoryTheory.Limits.Multifork I) (K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : I.L) :

CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Limits.Multifork.ι K₂ j) = CategoryTheory.Limits.Multifork.ι K₁ j

@[simp]

theorem CategoryTheory.Limits.Multifork.ofι_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (P : C) (ι : (a : I.L) → P ⟶ I.left a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)) :

(CategoryTheory.Limits.Multifork.ofι I P ι w).pt = P

@[simp]

theorem CategoryTheory.Limits.Multifork.ofι_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (P : C) (ι : (a : I.L) → P ⟶ I.left a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)) (x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) :

(CategoryTheory.Limits.Multifork.ofι I P ι w).π.app x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => ι a | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b)

def CategoryTheory.Limits.Multifork.ofι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (P : C) (ι : (a : I.L) → P ⟶ I.left a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)) :

CategoryTheory.Limits.Multifork I

Construct a multifork using a collection ι of morphisms.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.fstTo b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

@[simp]

theorem CategoryTheory.Limits.Multifork.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.mk_lift {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) → m = lift E) (E : CategoryTheory.Limits.Multifork I) :

(CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E

def CategoryTheory.Limits.Multifork.IsLimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) → m = lift E) :

CategoryTheory.Limits.IsLimit K

This definition provides a convenient way to show that a multifork is a limit.

Equations

CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) :

(CategoryTheory.Limits.Multifork.toPiFork K).pt = K.pt

noncomputable def CategoryTheory.Limits.Multifork.toPiFork {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) :

CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

Given a multifork, we may obtain a fork over ∏ I.left ⇉ ∏ I.right.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.Multifork.toPiFork K) = CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_one {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

(CategoryTheory.Limits.Multifork.toPiFork K).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.Limits.MulticospanIndex.fstPiMap I)

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) :

(CategoryTheory.Limits.Multifork.ofPiFork I c).pt = c.pt

noncomputable def CategoryTheory.Limits.Multifork.ofPiFork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) :

CategoryTheory.Limits.Multifork I

Given a fork over ∏ I.left ⇉ ∏ I.right, we may obtain a multifork.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) (a : I.L) :

CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Multifork.ofPiFork I c) a = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.Limits.Pi.π I.left a)

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) (a : I.R) :

(CategoryTheory.Limits.Multifork.ofPiFork I c).π.app (CategoryTheory.Limits.WalkingMulticospan.right a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.Pi.π I.right a))

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) :

(CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I).obj K = CategoryTheory.Limits.Multifork.toPiFork K

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ : CategoryTheory.Limits.Multifork I} {K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) :

((CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I).map f).hom = f.hom

noncomputable def CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Multifork I) (CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I))

Multifork.toPiFork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) :

(CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I).obj c = CategoryTheory.Limits.Multifork.ofPiFork I c

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)} {K₂ : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)} (f : K₁ ⟶ K₂) :

((CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I).map f).hom = f.hom

noncomputable def CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) (CategoryTheory.Limits.Multifork I)

Multifork.ofPiFork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

(CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).counitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I) (CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

(CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).unitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Multifork I) => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

(CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).functor = CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

(CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).inverse = CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I

noncomputable def CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

The category of multiforks is equivalent to the category of forks over ∏ I.left ⇉ ∏ I.right. It then follows from CategoryTheory.IsLimit.ofPreservesConeTerminal (or reflects) that it preserves and reflects limit cones.

Equations

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

Instances For

def CategoryTheory.Limits.Multicofork.π {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (b : I.R) :

I.right b ⟶ K.pt

The maps to the cocone point of a multicofork from the objects on the right.

Equations

CategoryTheory.Limits.Multicofork.π K b = K.ι.app (CategoryTheory.Limits.WalkingMultispan.right b)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_eq_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (b : I.R) :

K.ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicofork.π K b

@[simp]

theorem CategoryTheory.Limits.Multicofork.fst_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) :

K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicofork.π K (I.fstFrom a))

theorem CategoryTheory.Limits.Multicofork.snd_app_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom)).obj K.pt).obj (CategoryTheory.Limits.WalkingMultispan.left a) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a)) h = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K (I.sndFrom a)) h)

theorem CategoryTheory.Limits.Multicofork.snd_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) :

K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicofork.π K (I.sndFrom a))

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_comp_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K₁ : CategoryTheory.Limits.Multicofork I) (K₂ : CategoryTheory.Limits.Multicofork I) (f : K₁ ⟶ K₂) (b : I.R) {Z : C} (h : K₂.pt ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K₁ b) (CategoryTheory.CategoryStruct.comp f.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K₂ b) h

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_comp_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K₁ : CategoryTheory.Limits.Multicofork I) (K₂ : CategoryTheory.Limits.Multicofork I) (f : K₁ ⟶ K₂) (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K₁ b) f.hom = CategoryTheory.Limits.Multicofork.π K₂ b

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofπ_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (P : C) (π : (b : I.R) → I.right b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))) :

(CategoryTheory.Limits.Multicofork.ofπ I P π w).pt = P

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofπ_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (P : C) (π : (b : I.R) → I.right b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))) (x : CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom) :

(CategoryTheory.Limits.Multicofork.ofπ I P π w).ι.app x = match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) | CategoryTheory.Limits.WalkingMultispan.right b => π b

def CategoryTheory.Limits.Multicofork.ofπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (P : C) (π : (b : I.R) → I.right b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))) :

CategoryTheory.Limits.Multicofork I

Construct a multicofork using a collection π of morphisms.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) {Z : C} (h : K.pt ⟶ Z) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K (I.fstFrom a)) h) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K (I.sndFrom a)) h)

@[simp]

theorem CategoryTheory.Limits.Multicofork.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicofork.π K (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicofork.π K (I.sndFrom a))

@[simp]

theorem CategoryTheory.Limits.Multicofork.IsColimit.mk_desc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : CategoryTheory.Limits.Multicofork I) (i : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K i) (desc E) = CategoryTheory.Limits.Multicofork.π E i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K i) m = CategoryTheory.Limits.Multicofork.π E i) → m = desc E) (E : CategoryTheory.Limits.Multicofork I) :

(CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq).desc E = desc E

def CategoryTheory.Limits.Multicofork.IsColimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : CategoryTheory.Limits.Multicofork I) (i : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K i) (desc E) = CategoryTheory.Limits.Multicofork.π E i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K i) m = CategoryTheory.Limits.Multicofork.π E i) → m = desc E) :

CategoryTheory.Limits.IsColimit K

This definition provides a convenient way to show that a multicofork is a colimit.

Equations

CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq = { desc := desc, fac := ⋯, uniq := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π K)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π K))

@[simp]

theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) :

(CategoryTheory.Limits.Multicofork.toSigmaCofork K).pt = K.pt

noncomputable def CategoryTheory.Limits.Multicofork.toSigmaCofork {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) :

CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

Given a multicofork, we may obtain a cofork over ∐ I.left ⇉ ∐ I.right.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_π {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.Multicofork.toSigmaCofork K) = CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π K)

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).pt = c.pt

noncomputable def CategoryTheory.Limits.Multicofork.ofSigmaCofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) :

CategoryTheory.Limits.Multicofork I

Given a cofork over ∐ I.left ⇉ ∐ I.right, we may obtain a multicofork.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (a : I.L) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.Cofork.π c))

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (b : I.R) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Cofork.π c)

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right' {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (b : I.R) :

CategoryTheory.Limits.Multicofork.π (CategoryTheory.Limits.Multicofork.ofSigmaCofork I c) b = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Cofork.π c)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {K₁ : CategoryTheory.Limits.Multicofork I} {K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂) :

((CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) :

(CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I).obj K = CategoryTheory.Limits.Multicofork.toSigmaCofork K

noncomputable def CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Multicofork I) (CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I))

Multicofork.toSigmaCofork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {K₁ : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)} {K₂ : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)} (f : K₁ ⟶ K₂) :

((CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) :

(CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I).obj c = CategoryTheory.Limits.Multicofork.ofSigmaCofork I c

noncomputable def CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (CategoryTheory.Limits.Multicofork I)

Multicofork.ofSigmaCofork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

(CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).functor = CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

(CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).inverse = CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

(CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).unitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Multicofork I) => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multicofork I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

(CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).counitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) => CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I) (CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I)).obj K).pt) ⋯) ⋯

noncomputable def CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.Multicofork I ≌ CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

The category of multicoforks is equivalent to the category of coforks over ∐ I.left ⇉ ∐ I.right. It then follows from CategoryTheory.IsColimit.ofPreservesCoconeInitial (or reflects) that it preserves and reflects colimit cocones.

Equations

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

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.HasMultiequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) :

For I : MulticospanIndex C, we say that it has a multiequalizer if the associated multicospan has a limit.

Equations

CategoryTheory.Limits.HasMultiequalizer I = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.MulticospanIndex.multicospan I)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.multiequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] :

C

The multiequalizer of I : MulticospanIndex C.

Equations

CategoryTheory.Limits.multiequalizer I = CategoryTheory.Limits.limit (CategoryTheory.Limits.MulticospanIndex.multicospan I)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.HasMulticoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) :

For I : MultispanIndex C, we say that it has a multicoequalizer if the associated multicospan has a limit.

Equations

CategoryTheory.Limits.HasMulticoequalizer I = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.MultispanIndex.multispan I)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.multicoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] :

C

The multiecoqualizer of I : MultispanIndex C.

Equations

CategoryTheory.Limits.multicoequalizer I = CategoryTheory.Limits.colimit (CategoryTheory.Limits.MultispanIndex.multispan I)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.Multiequalizer.ι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (a : I.L) :

CategoryTheory.Limits.multiequalizer I ⟶ I.left a

The canonical map from the multiequalizer to the objects on the left.

Equations

CategoryTheory.Limits.Multiequalizer.ι I a = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.MulticospanIndex.multicospan I) (CategoryTheory.Limits.WalkingMulticospan.left a)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.Multiequalizer.multifork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] :

CategoryTheory.Limits.Multifork I

The multifork associated to the multiequalizer.

Equations

CategoryTheory.Limits.Multiequalizer.multifork I = CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.MulticospanIndex.multicospan I)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.multifork_ι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (a : I.L) :

CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Multiequalizer.multifork I) a = CategoryTheory.Limits.Multiequalizer.ι I a

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.multifork_π_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (a : I.L) :

(CategoryTheory.Limits.Multiequalizer.multifork I).π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.Limits.Multiequalizer.ι I a

theorem CategoryTheory.Limits.Multiequalizer.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.fstTo b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

theorem CategoryTheory.Limits.Multiequalizer.condition {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.sndTo b)) (I.snd b)

@[inline, reducible]

abbrev CategoryTheory.Limits.Multiequalizer.lift {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : I.L) → W ⟶ I.left a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) :

W ⟶ CategoryTheory.Limits.multiequalizer I

Construct a morphism to the multiequalizer from its universal property.

Equations

CategoryTheory.Limits.Multiequalizer.lift I W k h = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.MulticospanIndex.multicospan I) (CategoryTheory.Limits.Multifork.ofι I W k h)

Instances For

theorem CategoryTheory.Limits.Multiequalizer.lift_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : I.L) → W ⟶ I.left a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) (a : I.L) {Z : C} (h : I.left a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h) = CategoryTheory.CategoryStruct.comp (k a) h

theorem CategoryTheory.Limits.Multiequalizer.lift_ι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : I.L) → W ⟶ I.left a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) (a : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h) (CategoryTheory.Limits.Multiequalizer.ι I a) = k a

theorem CategoryTheory.Limits.Multiequalizer.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] {W : C} (i : W ⟶ CategoryTheory.Limits.multiequalizer I) (j : W ⟶ CategoryTheory.Limits.multiequalizer I) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) = CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)) :

i = j

instance CategoryTheory.Limits.Multiequalizer.instHasEqualizerPiObjLLeftRRightFstPiMapSndPiMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.HasEqualizer (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

Equations

⋯ = ⋯

def CategoryTheory.Limits.Multiequalizer.isoEqualizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.multiequalizer I ≅ CategoryTheory.Limits.equalizer (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

The multiequalizer is isomorphic to the equalizer of ∏ I.left ⇉ ∏ I.right.

Equations

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

Instances For

def CategoryTheory.Limits.Multiequalizer.ιPi {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.multiequalizer I ⟶ ∏ I.left

The canonical injection multiequalizer I ⟶ ∏ I.left.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.ιPi_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : I.L) {Z : C} (h : I.left a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left a) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.ιPi_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.Limits.Pi.π I.left a) = CategoryTheory.Limits.Multiequalizer.ι I a

instance CategoryTheory.Limits.Multiequalizer.instMonoMultiequalizerPiObjLLeftιPi {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Mono (CategoryTheory.Limits.Multiequalizer.ιPi I)

Equations

⋯ = ⋯

@[inline, reducible]

abbrev CategoryTheory.Limits.Multicoequalizer.π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

I.right b ⟶ CategoryTheory.Limits.multicoequalizer I

The canonical map from the multiequalizer to the objects on the left.

Equations

CategoryTheory.Limits.Multicoequalizer.π I b = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.MultispanIndex.multispan I) (CategoryTheory.Limits.WalkingMultispan.right b)

Instances For

@[inline, reducible]

abbrev CategoryTheory.Limits.Multicoequalizer.multicofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] :

CategoryTheory.Limits.Multicofork I

The multicofork associated to the multicoequalizer.

Equations

CategoryTheory.Limits.Multicoequalizer.multicofork I = CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.MultispanIndex.multispan I)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.multicofork_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

CategoryTheory.Limits.Multicofork.π (CategoryTheory.Limits.Multicoequalizer.multicofork I) b = CategoryTheory.Limits.Multicoequalizer.π I b

theorem CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

(CategoryTheory.Limits.Multicoequalizer.multicofork I).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right' {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.MultispanIndex.multispan I) (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b

theorem CategoryTheory.Limits.Multicoequalizer.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (a : I.L) {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (I.fstFrom a)) h) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (I.sndFrom a)) h)

theorem CategoryTheory.Limits.Multicoequalizer.condition {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (a : I.L) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicoequalizer.π I (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicoequalizer.π I (I.sndFrom a))

@[inline, reducible]

abbrev CategoryTheory.Limits.Multicoequalizer.desc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))) :

CategoryTheory.Limits.multicoequalizer I ⟶ W

Construct a morphism from the multicoequalizer from its universal property.

Equations

CategoryTheory.Limits.Multicoequalizer.desc I W k h = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.MultispanIndex.multispan I) (CategoryTheory.Limits.Multicofork.ofπ I W k h)

Instances For

theorem CategoryTheory.Limits.Multicoequalizer.π_desc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))) (b : I.R) {Z : C} (h : W ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.desc I W k h✝) h) = CategoryTheory.CategoryStruct.comp (k b) h

theorem CategoryTheory.Limits.Multicoequalizer.π_desc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))) (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.Limits.Multicoequalizer.desc I W k h) = k b

theorem CategoryTheory.Limits.Multicoequalizer.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] {W : C} (i : CategoryTheory.Limits.multicoequalizer I ⟶ W) (j : CategoryTheory.Limits.multicoequalizer I ⟶ W) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j) :

i = j

instance CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerSigmaObjLLeftRRightFstSigmaMapSndSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.HasCoequalizer (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

Equations

⋯ = ⋯

def CategoryTheory.Limits.Multicoequalizer.isoCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.multicoequalizer I ≅ CategoryTheory.Limits.coequalizer (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

The multicoequalizer is isomorphic to the coequalizer of ∐ I.left ⇉ ∐ I.right.

Equations

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

Instances For

def CategoryTheory.Limits.Multicoequalizer.sigmaπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

∐ I.right ⟶ CategoryTheory.Limits.multicoequalizer I

The canonical projection ∐ I.right ⟶ multicoequalizer I.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.R) {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) h

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) = CategoryTheory.Limits.Multicoequalizer.π I b

instance CategoryTheory.Limits.Multicoequalizer.instEpiSigmaObjRRightMulticoequalizerSigmaπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Epi (CategoryTheory.Limits.Multicoequalizer.sigmaπ I)

Equations

⋯ = ⋯