mathlib3 documentation

category_theory.limits.shapes.multiequalizer

Multi-(co)equalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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).

source
@[nolint]
inductive category_theory.limits.walking_multicospan {L R : Type w} (fst snd : R → L) :
Type w

The type underlying the multiequalizer diagram.

Instances for category_theory.limits.walking_multicospan
source
@[nolint]
inductive category_theory.limits.walking_multispan {L R : Type w} (fst snd : L → R) :
Type w

The type underlying the multiecoqualizer diagram.

Instances for category_theory.limits.walking_multispan
source
@[protected, instance]
def category_theory.limits.walking_multicospan.inhabited {L R : Type w} {fst snd : R → L} [inhabited L] :
inhabited (category_theory.limits.walking_multicospan fst snd)
Equations
source
inductive category_theory.limits.walking_multicospan.hom {L R : Type w} {fst snd : R → L} (a b : category_theory.limits.walking_multicospan fst snd) :
Type w

Morphisms for walking_multicospan.

Instances for category_theory.limits.walking_multicospan.hom
source
@[protected, instance]
def category_theory.limits.walking_multicospan.hom.inhabited {L R : Type w} {fst snd : R → L} {a : category_theory.limits.walking_multicospan fst snd} :
inhabited (a.hom a)
Equations
source
def category_theory.limits.walking_multicospan.hom.comp {L R : Type w} {fst snd : R → L} {A B C : category_theory.limits.walking_multicospan fst snd} (f : A.hom B) (g : B.hom C) :
A.hom C

Composition of morphisms for walking_multicospan.

Equations
source
@[protected, instance]
def category_theory.limits.walking_multicospan.category_theory.small_category {L R : Type w} {fst snd : R → L} :
category_theory.small_category (category_theory.limits.walking_multicospan fst snd)
Equations
source
@[protected, instance]
def category_theory.limits.walking_multispan.inhabited {L R : Type v} {fst snd : L → R} [inhabited L] :
inhabited (category_theory.limits.walking_multispan fst snd)
Equations
source
inductive category_theory.limits.walking_multispan.hom {L R : Type v} {fst snd : L → R} (a b : category_theory.limits.walking_multispan fst snd) :
Type v

Morphisms for walking_multispan.

Instances for category_theory.limits.walking_multispan.hom
source
@[protected, instance]
def category_theory.limits.walking_multispan.hom.inhabited {L R : Type v} {fst snd : L → R} {a : category_theory.limits.walking_multispan fst snd} :
inhabited (a.hom a)
Equations
source
def category_theory.limits.walking_multispan.hom.comp {L R : Type v} {fst snd : L → R} {A B C : category_theory.limits.walking_multispan fst snd} (f : A.hom B) (g : B.hom C) :
A.hom C

Composition of morphisms for walking_multispan.

Equations
source
@[protected, instance]
def category_theory.limits.walking_multispan.category_theory.small_category {L R : Type v} {fst snd : L → R} :
category_theory.small_category (category_theory.limits.walking_multispan fst snd)
Equations
source
@[nolint]
structure category_theory.limits.multicospan_index (C : Type u) [category_theory.category C] :
Type (max u v (w+1))

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

Instances for category_theory.limits.multicospan_index
  • category_theory.limits.multicospan_index.has_sizeof_inst
source
@[nolint]
structure category_theory.limits.multispan_index (C : Type u) [category_theory.category C] :
Type (max u v (w+1))

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

Instances for category_theory.limits.multispan_index
  • category_theory.limits.multispan_index.has_sizeof_inst
source
def category_theory.limits.multicospan_index.multicospan {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) :
category_theory.limits.walking_multicospan I.fst_to I.snd_to ⥤ C

The multicospan associated to I : multicospan_index.

Equations
source
@[simp]
theorem category_theory.limits.multicospan_index.multicospan_obj_left {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (a : I.L) :
I.multicospan.obj (category_theory.limits.walking_multicospan.left a) = I.left a
source
@[simp]
theorem category_theory.limits.multicospan_index.multicospan_obj_right {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (b : I.R) :
I.multicospan.obj (category_theory.limits.walking_multicospan.right b) = I.right b
source
@[simp]
theorem category_theory.limits.multicospan_index.multicospan_map_fst {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (b : I.R) :
I.multicospan.map (category_theory.limits.walking_multicospan.hom.fst b) = I.fst b
source
@[simp]
theorem category_theory.limits.multicospan_index.multicospan_map_snd {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (b : I.R) :
I.multicospan.map (category_theory.limits.walking_multicospan.hom.snd b) = I.snd b
source
noncomputable def category_theory.limits.multicospan_index.fst_pi_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
∏ I.left ⟶ ∏ I.right

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

Equations
source
noncomputable def category_theory.limits.multicospan_index.snd_pi_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
∏ I.left ⟶ ∏ I.right

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

Equations
source
@[simp]
theorem category_theory.limits.multicospan_index.fst_pi_map_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (b : I.R) :
I.fst_pi_map ≫ category_theory.limits.pi.π I.right b = category_theory.limits.pi.π I.left (I.fst_to b) ≫ I.fst b
source
@[simp]
theorem category_theory.limits.multicospan_index.fst_pi_map_π_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (b : I.R) {X' : C} (f' : I.right b ⟶ X') :
I.fst_pi_map ≫ category_theory.limits.pi.π I.right b ≫ f' = category_theory.limits.pi.π I.left (I.fst_to b) ≫ I.fst b ≫ f'
source
@[simp]
theorem category_theory.limits.multicospan_index.snd_pi_map_π_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (b : I.R) {X' : C} (f' : I.right b ⟶ X') :
I.snd_pi_map ≫ category_theory.limits.pi.π I.right b ≫ f' = category_theory.limits.pi.π I.left (I.snd_to b) ≫ I.snd b ≫ f'
source
@[simp]
theorem category_theory.limits.multicospan_index.snd_pi_map_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (b : I.R) :
I.snd_pi_map ≫ category_theory.limits.pi.π I.right b = category_theory.limits.pi.π I.left (I.snd_to b) ≫ I.snd b
source
@[simp]
theorem category_theory.limits.multicospan_index.parallel_pair_diagram_obj {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (x : category_theory.limits.walking_parallel_pair) :
I.parallel_pair_diagram.obj x = category_theory.limits.parallel_pair._match_1 x
source
@[simp]
theorem category_theory.limits.multicospan_index.parallel_pair_diagram_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (x y : category_theory.limits.walking_parallel_pair) (h : x ⟶ y) :
I.parallel_pair_diagram.map h = category_theory.limits.parallel_pair._match_2 I.fst_pi_map I.snd_pi_map x y h
source
@[protected]
noncomputable def category_theory.limits.multicospan_index.parallel_pair_diagram {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.walking_parallel_pair ⥤ 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
source
def category_theory.limits.multispan_index.multispan {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) :
category_theory.limits.walking_multispan I.fst_from I.snd_from ⥤ C

The multispan associated to I : multispan_index.

Equations
Instances for category_theory.limits.multispan_index.multispan
source
@[simp]
theorem category_theory.limits.multispan_index.multispan_obj_left {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (a : I.L) :
I.multispan.obj (category_theory.limits.walking_multispan.left a) = I.left a
source
@[simp]
theorem category_theory.limits.multispan_index.multispan_obj_right {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (b : I.R) :
I.multispan.obj (category_theory.limits.walking_multispan.right b) = I.right b
source
@[simp]
theorem category_theory.limits.multispan_index.multispan_map_fst {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (a : I.L) :
I.multispan.map (category_theory.limits.walking_multispan.hom.fst a) = I.fst a
source
@[simp]
theorem category_theory.limits.multispan_index.multispan_map_snd {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (a : I.L) :
I.multispan.map (category_theory.limits.walking_multispan.hom.snd a) = I.snd a
source
noncomputable def category_theory.limits.multispan_index.fst_sigma_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
∐ I.left ⟶ ∐ I.right

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

Equations
source
noncomputable def category_theory.limits.multispan_index.snd_sigma_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
∐ I.left ⟶ ∐ I.right

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

Equations
source
@[simp]
theorem category_theory.limits.multispan_index.ι_fst_sigma_map_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (b : I.L) {X' : C} (f' : ∐ I.right ⟶ X') :
category_theory.limits.sigma.ι I.left b ≫ I.fst_sigma_map ≫ f' = I.fst b ≫ category_theory.limits.sigma.ι I.right (I.fst_from b) ≫ f'
source
@[simp]
theorem category_theory.limits.multispan_index.ι_fst_sigma_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (b : I.L) :
category_theory.limits.sigma.ι I.left b ≫ I.fst_sigma_map = I.fst b ≫ category_theory.limits.sigma.ι I.right (I.fst_from b)
source
@[simp]
theorem category_theory.limits.multispan_index.ι_snd_sigma_map_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (b : I.L) {X' : C} (f' : ∐ I.right ⟶ X') :
category_theory.limits.sigma.ι I.left b ≫ I.snd_sigma_map ≫ f' = I.snd b ≫ category_theory.limits.sigma.ι I.right (I.snd_from b) ≫ f'
source
@[simp]
theorem category_theory.limits.multispan_index.ι_snd_sigma_map {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (b : I.L) :
category_theory.limits.sigma.ι I.left b ≫ I.snd_sigma_map = I.snd b ≫ category_theory.limits.sigma.ι I.right (I.snd_from b)
source
@[protected, reducible]
noncomputable def category_theory.limits.multispan_index.parallel_pair_diagram {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.limits.walking_parallel_pair ⥤ 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.

source
@[nolint, reducible]
def category_theory.limits.multifork {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) :
Type (max u_1 u v)

A multifork is a cone over a multicospan.

source
@[nolint, reducible]
def category_theory.limits.multicofork {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) :
Type (max u_1 u v)

A multicofork is a cocone over a multispan.

source
def category_theory.limits.multifork.ι {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (a : I.L) :
K.X ⟶ I.left a

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

Equations
source
@[simp]
theorem category_theory.limits.multifork.app_left_eq_ι {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (a : I.L) :
K.π.app (category_theory.limits.walking_multicospan.left a) = K.ι a
source
@[simp]
theorem category_theory.limits.multifork.app_right_eq_ι_comp_fst {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (b : I.R) :
K.π.app (category_theory.limits.walking_multicospan.right b) = K.ι (I.fst_to b) ≫ I.fst b
source
theorem category_theory.limits.multifork.app_right_eq_ι_comp_snd {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (b : I.R) :
K.π.app (category_theory.limits.walking_multicospan.right b) = K.ι (I.snd_to b) ≫ I.snd b
source
theorem category_theory.limits.multifork.app_right_eq_ι_comp_snd_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (b : I.R) {X' : C} (f' : I.multicospan.obj (category_theory.limits.walking_multicospan.right b) ⟶ X') :
K.π.app (category_theory.limits.walking_multicospan.right b) ≫ f' = K.ι (I.snd_to b) ≫ I.snd b ≫ f'
source
@[simp]
theorem category_theory.limits.multifork.hom_comp_ι {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K₁ K₂ : category_theory.limits.multifork I) (f : K₁ ⟶ K₂) (j : I.L) :
f.hom ≫ K₂.ι j = K₁.ι j
source
@[simp]
theorem category_theory.limits.multifork.hom_comp_ι_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K₁ K₂ : category_theory.limits.multifork I) (f : K₁ ⟶ K₂) (j : I.L) {X' : C} (f' : I.left j ⟶ X') :
f.hom ≫ K₂.ι j ≫ f' = K₁.ι j ≫ f'
source
@[simp]
theorem category_theory.limits.multifork.of_ι_π_app {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (P : C) (ι : Π (a : I.L), P ⟶ I.left a) (w : ∀ (b : I.R), ι (I.fst_to b) ≫ I.fst b = ι (I.snd_to b) ≫ I.snd b) (x : category_theory.limits.walking_multicospan I.fst_to I.snd_to) :
(category_theory.limits.multifork.of_ι I P ι w).π.app x = category_theory.limits.multifork.of_ι._match_1 I P ι x
source
def category_theory.limits.multifork.of_ι {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (P : C) (ι : Π (a : I.L), P ⟶ I.left a) (w : ∀ (b : I.R), ι (I.fst_to b) ≫ I.fst b = ι (I.snd_to b) ≫ I.snd b) :
category_theory.limits.multifork I

Construct a multifork using a collection ι of morphisms.

Equations
source
@[simp]
theorem category_theory.limits.multifork.of_ι_X {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) (P : C) (ι : Π (a : I.L), P ⟶ I.left a) (w : ∀ (b : I.R), ι (I.fst_to b) ≫ I.fst b = ι (I.snd_to b) ≫ I.snd b) :
(category_theory.limits.multifork.of_ι I P ι w).X = P
source
@[simp]
theorem category_theory.limits.multifork.condition {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (b : I.R) :
K.ι (I.fst_to b) ≫ I.fst b = K.ι (I.snd_to b) ≫ I.snd b
source
@[simp]
theorem category_theory.limits.multifork.condition_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (b : I.R) {X' : C} (f' : I.right b ⟶ X') :
K.ι (I.fst_to b) ≫ I.fst b ≫ f' = K.ι (I.snd_to b) ≫ I.snd b ≫ f'
source
@[simp]
theorem category_theory.limits.multifork.is_limit.mk_lift {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (lift : Π (E : category_theory.limits.multifork I), E.X ⟶ K.X) (fac : ∀ (E : category_theory.limits.multifork I) (i : I.L), lift E ≫ K.ι i = E.ι i) (uniq : ∀ (E : category_theory.limits.multifork I) (m : E.X ⟶ K.X), (∀ (i : I.L), m ≫ K.ι i = E.ι i) → m = lift E) (E : category_theory.limits.multifork I) :
(category_theory.limits.multifork.is_limit.mk K lift fac uniq).lift E = lift E
source
def category_theory.limits.multifork.is_limit.mk {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) (lift : Π (E : category_theory.limits.multifork I), E.X ⟶ K.X) (fac : ∀ (E : category_theory.limits.multifork I) (i : I.L), lift E ≫ K.ι i = E.ι i) (uniq : ∀ (E : category_theory.limits.multifork I) (m : E.X ⟶ K.X), (∀ (i : I.L), m ≫ K.ι i = E.ι i) → m = lift E) :
category_theory.limits.is_limit K

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

Equations
source
@[simp]
theorem category_theory.limits.multifork.pi_condition {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.pi.lift K.ι ≫ I.fst_pi_map = category_theory.limits.pi.lift K.ι ≫ I.snd_pi_map
source
@[simp]
theorem category_theory.limits.multifork.pi_condition_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] {X' : C} (f' : ∏ I.right ⟶ X') :
category_theory.limits.pi.lift K.ι ≫ I.fst_pi_map ≫ f' = category_theory.limits.pi.lift K.ι ≫ I.snd_pi_map ≫ f'
source
noncomputable def category_theory.limits.multifork.to_pi_fork {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (K : category_theory.limits.multifork I) :
category_theory.limits.fork I.fst_pi_map I.snd_pi_map

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

Equations
source
@[simp]
theorem category_theory.limits.multifork.to_pi_fork_X {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (K : category_theory.limits.multifork I) :
K.to_pi_fork.X = K.X
source
@[simp]
theorem category_theory.limits.multifork.to_pi_fork_π_app_zero {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
K.to_pi_fork.ι = category_theory.limits.pi.lift K.ι
source
@[simp]
theorem category_theory.limits.multifork.to_pi_fork_π_app_one {C : Type u} [category_theory.category C] {I : category_theory.limits.multicospan_index C} (K : category_theory.limits.multifork I) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
K.to_pi_fork.π.app category_theory.limits.walking_parallel_pair.one = category_theory.limits.pi.lift K.ι ≫ I.fst_pi_map
source
noncomputable def category_theory.limits.multifork.of_pi_fork {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (c : category_theory.limits.fork I.fst_pi_map I.snd_pi_map) :
category_theory.limits.multifork I

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

Equations
source
@[simp]
theorem category_theory.limits.multifork.of_pi_fork_X {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (c : category_theory.limits.fork I.fst_pi_map I.snd_pi_map) :
(category_theory.limits.multifork.of_pi_fork I c).X = c.X
source
@[simp]
theorem category_theory.limits.multifork.of_pi_fork_π_app_left {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (c : category_theory.limits.fork I.fst_pi_map I.snd_pi_map) (a : I.L) :
(category_theory.limits.multifork.of_pi_fork I c).ι a = c.ι ≫ category_theory.limits.pi.π I.left a
source
@[simp]
theorem category_theory.limits.multifork.of_pi_fork_π_app_right {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (c : category_theory.limits.fork I.fst_pi_map I.snd_pi_map) (a : I.R) :
(category_theory.limits.multifork.of_pi_fork I c).π.app (category_theory.limits.walking_multicospan.right a) = c.ι ≫ I.fst_pi_map ≫ category_theory.limits.pi.π I.right a
source
@[simp]
theorem category_theory.limits.multicospan_index.to_pi_fork_functor_obj {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (K : category_theory.limits.multifork I) :
I.to_pi_fork_functor.obj K = K.to_pi_fork
source
@[simp]
theorem category_theory.limits.multicospan_index.to_pi_fork_functor_map_hom {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (K₁ K₂ : category_theory.limits.multifork I) (f : K₁ ⟶ K₂) :
(I.to_pi_fork_functor.map f).hom = f.hom
source
noncomputable def category_theory.limits.multicospan_index.to_pi_fork_functor {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.multifork I ⥤ category_theory.limits.fork I.fst_pi_map I.snd_pi_map

multifork.to_pi_fork is functorial.

Equations
source
@[simp]
theorem category_theory.limits.multicospan_index.of_pi_fork_functor_obj {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (c : category_theory.limits.fork I.fst_pi_map I.snd_pi_map) :
I.of_pi_fork_functor.obj c = category_theory.limits.multifork.of_pi_fork I c
source
noncomputable def category_theory.limits.multicospan_index.of_pi_fork_functor {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.fork I.fst_pi_map I.snd_pi_map ⥤ category_theory.limits.multifork I

multifork.of_pi_fork is functorial.

Equations
source
@[simp]
theorem category_theory.limits.multicospan_index.of_pi_fork_functor_map_hom {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (K₁ K₂ : category_theory.limits.fork I.fst_pi_map I.snd_pi_map) (f : K₁ ⟶ K₂) :
(I.of_pi_fork_functor.map f).hom = f.hom
source
@[simp]
theorem category_theory.limits.multicospan_index.multifork_equiv_pi_fork_functor {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
I.multifork_equiv_pi_fork.functor = I.to_pi_fork_functor
source
@[simp]
theorem category_theory.limits.multicospan_index.multifork_equiv_pi_fork_unit_iso {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
I.multifork_equiv_pi_fork.unit_iso = category_theory.nat_iso.of_components (λ (K : category_theory.limits.multifork I), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.multifork I)).obj K).X) _) _
source
@[simp]
theorem category_theory.limits.multicospan_index.multifork_equiv_pi_fork_counit_iso {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
I.multifork_equiv_pi_fork.counit_iso = category_theory.nat_iso.of_components (λ (K : category_theory.limits.fork I.fst_pi_map I.snd_pi_map), category_theory.limits.fork.ext (category_theory.iso.refl ((I.of_pi_fork_functor ⋙ I.to_pi_fork_functor).obj K).X) _) _
source
@[simp]
theorem category_theory.limits.multicospan_index.multifork_equiv_pi_fork_inverse {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
I.multifork_equiv_pi_fork.inverse = I.of_pi_fork_functor
source
noncomputable def category_theory.limits.multicospan_index.multifork_equiv_pi_fork {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.multifork I ≌ category_theory.limits.fork I.fst_pi_map I.snd_pi_map

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

Equations
source
def category_theory.limits.multicofork.π {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (b : I.R) :
I.right b ⟶ K.X

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

Equations
source
@[simp]
theorem category_theory.limits.multicofork.π_eq_app_right {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (b : I.R) :
K.ι.app (category_theory.limits.walking_multispan.right b) = K.π b
source
@[simp]
theorem category_theory.limits.multicofork.fst_app_right {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (a : I.L) :
K.ι.app (category_theory.limits.walking_multispan.left a) = I.fst a ≫ K.π (I.fst_from a)
source
theorem category_theory.limits.multicofork.snd_app_right {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (a : I.L) :
K.ι.app (category_theory.limits.walking_multispan.left a) = I.snd a ≫ K.π (I.snd_from a)
source
theorem category_theory.limits.multicofork.snd_app_right_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (a : I.L) {X' : C} (f' : ((category_theory.functor.const (category_theory.limits.walking_multispan I.fst_from I.snd_from)).obj K.X).obj (category_theory.limits.walking_multispan.left a) ⟶ X') :
K.ι.app (category_theory.limits.walking_multispan.left a) ≫ f' = I.snd a ≫ K.π (I.snd_from a) ≫ f'
source
@[simp]
theorem category_theory.limits.multicofork.of_π_ι_app {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (P : C) (π : Π (b : I.R), I.right b ⟶ P) (w : ∀ (a : I.L), I.fst a ≫ π (I.fst_from a) = I.snd a ≫ π (I.snd_from a)) (x : category_theory.limits.walking_multispan I.fst_from I.snd_from) :
(category_theory.limits.multicofork.of_π I P π w).ι.app x = category_theory.limits.multicofork.of_π._match_1 I P π x
source
def category_theory.limits.multicofork.of_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (P : C) (π : Π (b : I.R), I.right b ⟶ P) (w : ∀ (a : I.L), I.fst a ≫ π (I.fst_from a) = I.snd a ≫ π (I.snd_from a)) :
category_theory.limits.multicofork I

Construct a multicofork using a collection π of morphisms.

Equations
source
@[simp]
theorem category_theory.limits.multicofork.of_π_X {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) (P : C) (π : Π (b : I.R), I.right b ⟶ P) (w : ∀ (a : I.L), I.fst a ≫ π (I.fst_from a) = I.snd a ≫ π (I.snd_from a)) :
(category_theory.limits.multicofork.of_π I P π w).X = P
source
@[simp]
theorem category_theory.limits.multicofork.condition_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (a : I.L) {X' : C} (f' : K.X ⟶ X') :
I.fst a ≫ K.π (I.fst_from a) ≫ f' = I.snd a ≫ K.π (I.snd_from a) ≫ f'
source
@[simp]
theorem category_theory.limits.multicofork.condition {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (a : I.L) :
I.fst a ≫ K.π (I.fst_from a) = I.snd a ≫ K.π (I.snd_from a)
source
@[simp]
theorem category_theory.limits.multicofork.is_colimit.mk_desc {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (desc : Π (E : category_theory.limits.multicofork I), K.X ⟶ E.X) (fac : ∀ (E : category_theory.limits.multicofork I) (i : I.R), K.π i ≫ desc E = E.π i) (uniq : ∀ (E : category_theory.limits.multicofork I) (m : K.X ⟶ E.X), (∀ (i : I.R), K.π i ≫ m = E.π i) → m = desc E) (E : category_theory.limits.multicofork I) :
(category_theory.limits.multicofork.is_colimit.mk K desc fac uniq).desc E = desc E
source
def category_theory.limits.multicofork.is_colimit.mk {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) (desc : Π (E : category_theory.limits.multicofork I), K.X ⟶ E.X) (fac : ∀ (E : category_theory.limits.multicofork I) (i : I.R), K.π i ≫ desc E = E.π i) (uniq : ∀ (E : category_theory.limits.multicofork I) (m : K.X ⟶ E.X), (∀ (i : I.R), K.π i ≫ m = E.π i) → m = desc E) :
category_theory.limits.is_colimit K

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

Equations
source
@[simp]
theorem category_theory.limits.multicofork.sigma_condition_assoc {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] {X' : C} (f' : K.X ⟶ X') :
I.fst_sigma_map ≫ category_theory.limits.sigma.desc K.π ≫ f' = I.snd_sigma_map ≫ category_theory.limits.sigma.desc K.π ≫ f'
source
@[simp]
theorem category_theory.limits.multicofork.sigma_condition {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
I.fst_sigma_map ≫ category_theory.limits.sigma.desc K.π = I.snd_sigma_map ≫ category_theory.limits.sigma.desc K.π
source
noncomputable def category_theory.limits.multicofork.to_sigma_cofork {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (K : category_theory.limits.multicofork I) :
category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map

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

Equations
source
@[simp]
theorem category_theory.limits.multicofork.to_sigma_cofork_X {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (K : category_theory.limits.multicofork I) :
K.to_sigma_cofork.X = K.X
source
@[simp]
theorem category_theory.limits.multicofork.to_sigma_cofork_π {C : Type u} [category_theory.category C] {I : category_theory.limits.multispan_index C} (K : category_theory.limits.multicofork I) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
K.to_sigma_cofork.π = category_theory.limits.sigma.desc K.π
source
noncomputable def category_theory.limits.multicofork.of_sigma_cofork {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (c : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map) :
category_theory.limits.multicofork I

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

Equations
source
@[simp]
theorem category_theory.limits.multicofork.of_sigma_cofork_X {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (c : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map) :
(category_theory.limits.multicofork.of_sigma_cofork I c).X = c.X
source
@[simp]
theorem category_theory.limits.multicofork.of_sigma_cofork_ι_app_left {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (c : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map) (a : I.L) :
(category_theory.limits.multicofork.of_sigma_cofork I c).ι.app (category_theory.limits.walking_multispan.left a) = category_theory.limits.sigma.ι I.left a ≫ I.fst_sigma_map ≫ c.π
source
@[simp]
theorem category_theory.limits.multicofork.of_sigma_cofork_ι_app_right {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (c : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map) (b : I.R) :
(category_theory.limits.multicofork.of_sigma_cofork I c).ι.app (category_theory.limits.walking_multispan.right b) = category_theory.limits.sigma.ι I.right b ≫ c.π
source
@[simp]
theorem category_theory.limits.multispan_index.to_sigma_cofork_functor_obj {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (K : category_theory.limits.multicofork I) :
I.to_sigma_cofork_functor.obj K = K.to_sigma_cofork
source
noncomputable def category_theory.limits.multispan_index.to_sigma_cofork_functor {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.limits.multicofork I ⥤ category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map

multicofork.to_sigma_cofork is functorial.

Equations
source
@[simp]
theorem category_theory.limits.multispan_index.to_sigma_cofork_functor_map_hom {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (K₁ K₂ : category_theory.limits.multicofork I) (f : K₁ ⟶ K₂) :
(I.to_sigma_cofork_functor.map f).hom = f.hom
source
@[simp]
theorem category_theory.limits.multispan_index.of_sigma_cofork_functor_map_hom {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (K₁ K₂ : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map) (f : K₁ ⟶ K₂) :
(I.of_sigma_cofork_functor.map f).hom = f.hom
source
noncomputable def category_theory.limits.multispan_index.of_sigma_cofork_functor {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map ⥤ category_theory.limits.multicofork I

multicofork.of_sigma_cofork is functorial.

Equations
source
@[simp]
theorem category_theory.limits.multispan_index.of_sigma_cofork_functor_obj {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (c : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map) :
I.of_sigma_cofork_functor.obj c = category_theory.limits.multicofork.of_sigma_cofork I c
source
@[simp]
theorem category_theory.limits.multispan_index.multicofork_equiv_sigma_cofork_inverse {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
I.multicofork_equiv_sigma_cofork.inverse = I.of_sigma_cofork_functor
source
@[simp]
theorem category_theory.limits.multispan_index.multicofork_equiv_sigma_cofork_counit_iso {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
I.multicofork_equiv_sigma_cofork.counit_iso = category_theory.nat_iso.of_components (λ (K : category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map), category_theory.limits.cofork.ext (category_theory.iso.refl ((I.of_sigma_cofork_functor ⋙ I.to_sigma_cofork_functor).obj K).X) _) _
source
noncomputable def category_theory.limits.multispan_index.multicofork_equiv_sigma_cofork {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.limits.multicofork I ≌ category_theory.limits.cofork I.fst_sigma_map I.snd_sigma_map

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

Equations
source
@[simp]
theorem category_theory.limits.multispan_index.multicofork_equiv_sigma_cofork_functor {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
I.multicofork_equiv_sigma_cofork.functor = I.to_sigma_cofork_functor
source
@[simp]
theorem category_theory.limits.multispan_index.multicofork_equiv_sigma_cofork_unit_iso {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
I.multicofork_equiv_sigma_cofork.unit_iso = category_theory.nat_iso.of_components (λ (K : category_theory.limits.multicofork I), category_theory.limits.cocones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.multicofork I)).obj K).X) _) _
source
@[reducible]
def category_theory.limits.has_multiequalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) :
Prop

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

source
@[reducible]
noncomputable def category_theory.limits.multiequalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] :
C

The multiequalizer of I : multicospan_index C.

source
@[reducible]
def category_theory.limits.has_multicoequalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) :
Prop

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

source
@[reducible]
noncomputable def category_theory.limits.multicoequalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] :
C

The multiecoqualizer of I : multispan_index C.

source
@[reducible]
noncomputable def category_theory.limits.multiequalizer.ι {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (a : I.L) :
category_theory.limits.multiequalizer I ⟶ I.left a

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

source
@[reducible]
noncomputable def category_theory.limits.multiequalizer.multifork {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] :
category_theory.limits.multifork I

The multifork associated to the multiequalizer.

source
@[simp]
theorem category_theory.limits.multiequalizer.multifork_ι {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (a : I.L) :
(category_theory.limits.multiequalizer.multifork I).ι a = category_theory.limits.multiequalizer.ι I a
source
@[simp]
theorem category_theory.limits.multiequalizer.multifork_π_app_left {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (a : I.L) :
(category_theory.limits.multiequalizer.multifork I).π.app (category_theory.limits.walking_multicospan.left a) = category_theory.limits.multiequalizer.ι I a
source
theorem category_theory.limits.multiequalizer.condition_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (b : I.R) {X' : C} (f' : I.right b ⟶ X') :
category_theory.limits.multiequalizer.ι I (I.fst_to b) ≫ I.fst b ≫ f' = category_theory.limits.multiequalizer.ι I (I.snd_to b) ≫ I.snd b ≫ f'
source
theorem category_theory.limits.multiequalizer.condition {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (b : I.R) :
category_theory.limits.multiequalizer.ι I (I.fst_to b) ≫ I.fst b = category_theory.limits.multiequalizer.ι I (I.snd_to b) ≫ I.snd b
source
@[reducible]
noncomputable def category_theory.limits.multiequalizer.lift {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (W : C) (k : Π (a : I.L), W ⟶ I.left a) (h : ∀ (b : I.R), k (I.fst_to b) ≫ I.fst b = k (I.snd_to b) ≫ I.snd b) :
W ⟶ category_theory.limits.multiequalizer I

Construct a morphism to the multiequalizer from its universal property.

source
@[simp]
theorem category_theory.limits.multiequalizer.lift_ι_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (W : C) (k : Π (a : I.L), W ⟶ I.left a) (h : ∀ (b : I.R), k (I.fst_to b) ≫ I.fst b = k (I.snd_to b) ≫ I.snd b) (a : I.L) {X' : C} (f' : I.left a ⟶ X') :
category_theory.limits.multiequalizer.lift I W k h ≫ category_theory.limits.multiequalizer.ι I a ≫ f' = k a ≫ f'
source
@[simp]
theorem category_theory.limits.multiequalizer.lift_ι {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] (W : C) (k : Π (a : I.L), W ⟶ I.left a) (h : ∀ (b : I.R), k (I.fst_to b) ≫ I.fst b = k (I.snd_to b) ≫ I.snd b) (a : I.L) :
category_theory.limits.multiequalizer.lift I W k h ≫ category_theory.limits.multiequalizer.ι I a = k a
source
@[ext]
theorem category_theory.limits.multiequalizer.hom_ext {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] {W : C} (i j : W ⟶ category_theory.limits.multiequalizer I) (h : ∀ (a : I.L), i ≫ category_theory.limits.multiequalizer.ι I a = j ≫ category_theory.limits.multiequalizer.ι I a) :
i = j
source
@[protected, instance]
def category_theory.limits.multiequalizer.category_theory.limits.multicospan_index.snd_pi_map.category_theory.limits.has_equalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.has_equalizer I.fst_pi_map I.snd_pi_map
source
noncomputable def category_theory.limits.multiequalizer.iso_equalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.multiequalizer I ≅ category_theory.limits.equalizer I.fst_pi_map I.snd_pi_map

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

Equations
source
noncomputable def category_theory.limits.multiequalizer.ι_pi {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.limits.multiequalizer I ⟶ ∏ I.left

The canonical injection multiequalizer I ⟶ ∏ I.left.

Equations
Instances for category_theory.limits.multiequalizer.ι_pi
source
@[simp]
theorem category_theory.limits.multiequalizer.ι_pi_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (a : I.L) :
category_theory.limits.multiequalizer.ι_pi I ≫ category_theory.limits.pi.π I.left a = category_theory.limits.multiequalizer.ι I a
source
@[simp]
theorem category_theory.limits.multiequalizer.ι_pi_π_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] (a : I.L) {X' : C} (f' : I.left a ⟶ X') :
category_theory.limits.multiequalizer.ι_pi I ≫ category_theory.limits.pi.π I.left a ≫ f' = category_theory.limits.multiequalizer.ι I a ≫ f'
source
@[protected, instance]
def category_theory.limits.multiequalizer.ι_pi.category_theory.mono {C : Type u} [category_theory.category C] (I : category_theory.limits.multicospan_index C) [category_theory.limits.has_multiequalizer I] [category_theory.limits.has_product I.left] [category_theory.limits.has_product I.right] :
category_theory.mono (category_theory.limits.multiequalizer.ι_pi I)
source
@[reducible]
noncomputable def category_theory.limits.multicoequalizer.π {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (b : I.R) :
I.right b ⟶ category_theory.limits.multicoequalizer I

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

source
@[reducible]
noncomputable def category_theory.limits.multicoequalizer.multicofork {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] :
category_theory.limits.multicofork I

The multicofork associated to the multicoequalizer.

source
@[simp]
theorem category_theory.limits.multicoequalizer.multicofork_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (b : I.R) :
(category_theory.limits.multicoequalizer.multicofork I).π b = category_theory.limits.multicoequalizer.π I b
source
@[simp]
theorem category_theory.limits.multicoequalizer.multicofork_ι_app_right {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (b : I.R) :
(category_theory.limits.multicoequalizer.multicofork I).ι.app (category_theory.limits.walking_multispan.right b) = category_theory.limits.multicoequalizer.π I b
source
theorem category_theory.limits.multicoequalizer.condition {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (a : I.L) :
I.fst a ≫ category_theory.limits.multicoequalizer.π I (I.fst_from a) = I.snd a ≫ category_theory.limits.multicoequalizer.π I (I.snd_from a)
source
theorem category_theory.limits.multicoequalizer.condition_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (a : I.L) {X' : C} (f' : category_theory.limits.multicoequalizer I ⟶ X') :
I.fst a ≫ category_theory.limits.multicoequalizer.π I (I.fst_from a) ≫ f' = I.snd a ≫ category_theory.limits.multicoequalizer.π I (I.snd_from a) ≫ f'
source
@[reducible]
noncomputable def category_theory.limits.multicoequalizer.desc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (W : C) (k : Π (b : I.R), I.right b ⟶ W) (h : ∀ (a : I.L), I.fst a ≫ k (I.fst_from a) = I.snd a ≫ k (I.snd_from a)) :
category_theory.limits.multicoequalizer I ⟶ W

Construct a morphism from the multicoequalizer from its universal property.

source
@[simp]
theorem category_theory.limits.multicoequalizer.π_desc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (W : C) (k : Π (b : I.R), I.right b ⟶ W) (h : ∀ (a : I.L), I.fst a ≫ k (I.fst_from a) = I.snd a ≫ k (I.snd_from a)) (b : I.R) :
category_theory.limits.multicoequalizer.π I b ≫ category_theory.limits.multicoequalizer.desc I W k h = k b
source
@[simp]
theorem category_theory.limits.multicoequalizer.π_desc_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] (W : C) (k : Π (b : I.R), I.right b ⟶ W) (h : ∀ (a : I.L), I.fst a ≫ k (I.fst_from a) = I.snd a ≫ k (I.snd_from a)) (b : I.R) {X' : C} (f' : W ⟶ X') :
category_theory.limits.multicoequalizer.π I b ≫ category_theory.limits.multicoequalizer.desc I W k h ≫ f' = k b ≫ f'
source
@[ext]
theorem category_theory.limits.multicoequalizer.hom_ext {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] {W : C} (i j : category_theory.limits.multicoequalizer I ⟶ W) (h : ∀ (b : I.R), category_theory.limits.multicoequalizer.π I b ≫ i = category_theory.limits.multicoequalizer.π I b ≫ j) :
i = j
source
@[protected, instance]
def category_theory.limits.multicoequalizer.category_theory.limits.multispan_index.snd_sigma_map.category_theory.limits.has_coequalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.limits.has_coequalizer I.fst_sigma_map I.snd_sigma_map
source
noncomputable def category_theory.limits.multicoequalizer.iso_coequalizer {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.limits.multicoequalizer I ≅ category_theory.limits.coequalizer I.fst_sigma_map I.snd_sigma_map

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

Equations
source
noncomputable def category_theory.limits.multicoequalizer.sigma_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
∐ I.right ⟶ category_theory.limits.multicoequalizer I

The canonical projection ∐ I.right ⟶ multicoequalizer I.

Equations
Instances for category_theory.limits.multicoequalizer.sigma_π
source
@[simp]
theorem category_theory.limits.multicoequalizer.ι_sigma_π {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (b : I.R) :
category_theory.limits.sigma.ι I.right b ≫ category_theory.limits.multicoequalizer.sigma_π I = category_theory.limits.multicoequalizer.π I b
source
@[simp]
theorem category_theory.limits.multicoequalizer.ι_sigma_π_assoc {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] (b : I.R) {X' : C} (f' : category_theory.limits.multicoequalizer I ⟶ X') :
category_theory.limits.sigma.ι I.right b ≫ category_theory.limits.multicoequalizer.sigma_π I ≫ f' = category_theory.limits.multicoequalizer.π I b ≫ f'
source
@[protected, instance]
def category_theory.limits.multicoequalizer.sigma_π.category_theory.epi {C : Type u} [category_theory.category C] (I : category_theory.limits.multispan_index C) [category_theory.limits.has_multicoequalizer I] [category_theory.limits.has_coproduct I.left] [category_theory.limits.has_coproduct I.right] :
category_theory.epi (category_theory.limits.multicoequalizer.sigma_π I)