# Special shapes for limits in Type. #

The general shape (co)limits defined in CategoryTheory.Limits.Types are intended for use through the limits API, and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in Type, giving the expected definitional implementation:

• the terminal object is PUnit
• the binary product of X and Y is X × Y
• the product of a family f : J → Type is Π j, f j
• the coproduct of a family f : J → Type is Σ j, f j
• the binary coproduct of X and Y is the sum type X ⊕ Y
• the equalizer of a pair of maps (g, h) is the subtype {x : Y // g x = h x}
• the coequalizer of a pair of maps (f, g) is the quotient of Y by ∀ x : Y, f x ~ g x
• the pullback of f : X ⟶ Z and g : Y ⟶ Z is the subtype { p : X × Y // f p.1 = g p.2 } of the product
• multiequalizers

We first construct terms of IsLimit and LimitCone, and then provide isomorphisms with the types generated by the HasLimit API.

As an example, when setting up the monoidal category structure on Type we use the Types.terminalLimitCone and Types.binaryProductLimitCone definitions.

@[simp]
theorem CategoryTheory.Limits.Types.pi_lift_π_apply {β : Type v} [] (f : βType u) {P : Type u} (s : (b : β) → P f b) (b : β) (x : P) :
= s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift.

theorem CategoryTheory.Limits.Types.pi_lift_π_apply' {β : Type v} (f : βType v) {P : Type v} (s : (b : β) → P f b) (b : β) (x : P) :
= s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift, with specialized universes.

@[simp]
theorem CategoryTheory.Limits.Types.pi_map_π_apply {β : Type v} [] {f : βType u} {g : βType u} (α : (j : β) → f j g j) (b : β) (x : ∏ᶜ f) :
= α b ()

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map.

theorem CategoryTheory.Limits.Types.pi_map_π_apply' {β : Type v} {f : βType v} {g : βType v} (α : (j : β) → f j g j) (b : β) (x : ∏ᶜ f) :
= α b ()

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map, with specialized universes.

The category of types has PUnit as a terminal object.

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

The terminal object in Type u is PUnit.

Equations
Instances For

The terminal object in Type u is PUnit.

Equations
Instances For

A type is terminal if and only if it contains exactly one element.

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

A type is terminal if and only if it is isomorphic to PUnit.

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

The category of types has PEmpty as an initial object.

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

The initial object in Type u is PEmpty.

Equations
Instances For

The initial object in Type u is PEmpty.

Equations
Instances For

An object in Type u is initial if and only if it is empty.

@[simp]

The product type X × Y forms a cone for the binary product of X and Y.

Equations
Instances For
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductLimit_lift (X : Type u) (Y : Type u) (s : ) (x : s.pt) :
s x = (s.fst x, s.snd x)

The product type X × Y is a binary product for X and Y.

Equations
• = { lift := fun (s : ) (x : s.pt) => (s.fst x, s.snd x), fac := , uniq := }
Instances For

The category of types has X × Y, the usual cartesian product, as the binary product of X and Y.

Equations
• = { cone := , isLimit := }
Instances For
noncomputable def CategoryTheory.Limits.Types.binaryProductIso (X : Type u) (Y : Type u) :
X Y X × Y

The categorical binary product in Type u is cartesian product.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst (X : Type u) (Y : Type u) :
= CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd (X : Type u) (Y : Type u) :
= CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst (X : Type u) (Y : Type u) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst = Prod.fst
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd (X : Type u) (Y : Type u) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd = Prod.snd
@[simp]
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductFunctor_map_app {X₁ : Type u} {X₂ : Type u} (f : X₁ X₂) (Y : Type u) :
@[simp]
theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_map (X : Type u) {Y₁ : Type u} {Y₂ : Type u} (f : Y₁ Y₂) :

The functor which sends X, Y to the product type X × Y.

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

The product functor given by the instance HasBinaryProducts (Type u) is isomorphic to the explicit binary product functor given by the product type.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app (X : Type u) (Y : Type u) :
∀ (x : ) (a : .obj x), x a = (match x.as with | CategoryTheory.Limits.WalkingPair.left => Sum.inl | CategoryTheory.Limits.WalkingPair.right => Sum.inr) a

The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.binaryCoproductColimit_desc (X : Type u) (Y : Type u) (s : ) :
∀ (a : X Y), s a = Sum.elim s.inl s.inr a

The sum type X ⊕ Y is a binary coproduct for X and Y.

Equations
• = { desc := fun (s : ) => Sum.elim s.inl s.inr, fac := , uniq := }
Instances For

The category of types has X ⊕ Y, as the binary coproduct of X and Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Types.binaryCoproductIso (X : Type u) (Y : Type u) :
X ⨿ Y X Y

The categorical binary coproduct in Type u is the sum X ⊕ Y.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom (X : Type u) (Y : Type u) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl = Sum.inl
@[simp]
theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom (X : Type u) (Y : Type u) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr = Sum.inr
@[simp]
theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv (X : Type u) (Y : Type u) :
= CategoryTheory.Limits.coprod.inl
@[simp]
theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv (X : Type u) (Y : Type u) :
= CategoryTheory.Limits.coprod.inr
noncomputable def CategoryTheory.Limits.Types.isCoprodOfMono {X : Type u} {Y : Type u} (f : X Y) :

Any monomorphism in Type is a coproduct injection.

Equations
Instances For

The category of types has Π j, f j as the product of a type family f : J → TypeMax.{v, u}.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Types.productIso {J : Type v} (F : JTypeMax) :
∏ᶜ F (j : J) → F j

The categorical product in TypeMax.{v, u} is the type theoretic product Π j, F j.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval {J : Type v} (F : JTypeMax) (j : J) :
(CategoryTheory.CategoryStruct.comp fun (f : (j : J) → F j) => f j) =
@[simp]
theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply {J : Type v} (F : JTypeMax) (j : J) (x : ∏ᶜ F) :
x j =
@[simp]
theorem CategoryTheory.Limits.Types.productIso_inv_comp_π_apply {J : Type v} (F : JTypeMax) (j : J) (x : (j : J) → F j) :
= x j
@[simp]
theorem CategoryTheory.Limits.Types.productIso_inv_comp_π {J : Type v} (F : JTypeMax) (j : J) :
= fun (f : (j : J) → F j) => f j
noncomputable def CategoryTheory.Limits.Types.Small.productLimitCone {J : Type v} (F : JType u) [] :

A variant of productLimitCone using a Small hypothesis rather than a function to TypeMax.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Types.Small.productIso {J : Type v} (F : JType u) [] :
∏ᶜ F Shrink.{u, max u v} ((j : J) → F j)

The categorical product in Type u indexed in Type v is the type theoretic product Π j, F j, after shrinking back to Type u.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval {J : Type v} (F : JType u) [] (j : J) :
(CategoryTheory.CategoryStruct.comp fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j) =
@[simp]
theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply {J : Type v} (F : JType u) [] (j : J) (x : ∏ᶜ F) :
(equivShrink ((j : J) → F j)).symm () j =
@[simp]
theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply {J : Type v} (F : JType u) [] (j : J) (x : Shrink.{u, max u v} ((j : J) → F j)) :
= (equivShrink ((j : J) → F j)).symm x j
@[simp]
theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π {J : Type v} (F : JType u) [] (j : J) :
= fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j

The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Types.coproductIso {J : Type v} (F : JTypeMax) :
F (j : J) × F j

The categorical coproduct in Type u is the type theoretic coproduct Σ j, F j.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom_apply {J : Type v} (F : JTypeMax) (j : J) (x : F j) :
= j, x
@[simp]
theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom {J : Type v} (F : JTypeMax) (j : J) :
= fun (x : F j) => j, x
noncomputable def CategoryTheory.Limits.Types.typeEqualizerOfUnique {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) {g : Y Z} {h : Y Z} (t : ∀ (y : Y), g y = h y∃! x : X, f x = y) :

Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.Types.unique_of_type_equalizer {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) {g : Y Z} {h : Y Z} (y : Y) (hy : g y = h y) :
∃! x : X, f x = y

The converse of type_equalizer_of_unique.

theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) {g : Y Z} {h : Y Z} :
∀ (y : Y), g y = h y∃! x : X, f x = y
def CategoryTheory.Limits.Types.equalizerLimit {Y : Type u} {Z : Type u} {g : Y Z} {h : Y Z} :

Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Types.equalizerIso {Y : Type u} {Z : Type u} (g : Y Z) (h : Y Z) :
{ x : Y // g x = h x }

The categorical equalizer in Type u is {x : Y // g x = h x}.

Equations
Instances For
@[simp]
@[simp]
theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply {Y : Type u} {Z : Type u} (g : Y Z) (h : Y Z) (x : { x : Y // g x = h x }) :
= x
@[simp]
theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι {Y : Type u} {Z : Type u} (g : Y Z) (h : Y Z) :
= Subtype.val
inductive CategoryTheory.Limits.Types.CoequalizerRel {X : Type u} {Y : Type u} (f : X Y) (g : X Y) :
YYProp

(Implementation) The relation to be quotiented to obtain the coequalizer.

Instances For
def CategoryTheory.Limits.Types.coequalizerColimit {X : Type u} {Y : Type u} (f : X Y) (g : X Y) :

Show that the quotient by the relation generated by f(x) ~ g(x) is a coequalizer for the pair (f, g).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : X Y) (π : Y Z) (U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) :
π ⁻¹' (π '' U) = U

If π : Y ⟶ Z is an equalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U, then π ⁻¹' (π '' U) = U.

noncomputable def CategoryTheory.Limits.Types.coequalizerIso {X : Type u} {Y : Type u} (f : X Y) (g : X Y) :

The categorical coequalizer in Type u is the quotient by f g ~ g x.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply {X : Type u} {Y : Type u} (f : X Y) (g : X Y) (x : Y) :
@[simp]
theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom {X : Type u} {Y : Type u} (f : X Y) (g : X Y) :
@[simp]
theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv {X : Type u} {Y : Type u} (f : X Y) (g : X Y) :
@[reducible, inline]
abbrev CategoryTheory.Limits.Types.PullbackObj {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :

The usual explicit pullback in the category of types, as a subtype of the product. The full LimitCone data is bundled as pullbackLimitCone f g.

Equations
• = { p : X × Y // f p.1 = g p.2 }
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.Types.pullbackCone {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :

The explicit pullback cone on PullbackObj f g. This is bundled with the IsLimit data as pullbackLimitCone f g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.pullbackLimitCone_isLimit {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :
.isLimit = .isLimitAux (fun (s : ) (x : s.pt) => (s.fst x, s.snd x), )
@[simp]
theorem CategoryTheory.Limits.Types.pullbackLimitCone_cone {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :
def CategoryTheory.Limits.Types.pullbackLimitCone {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :

The explicit pullback in the category of types, bundled up as a LimitCone for given f and g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : } (hc : ) :

A limit pullback cone in the category of types identifies to the explicit pullback.

Equations
• = (hc.conePointUniqueUpToIso .isLimit).toEquiv
Instances For
@[simp]
theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : } (hc : ) (x : c.pt) :
= c.fst x
@[simp]
theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : } (hc : ) (x : c.pt) :
= c.snd x
@[simp]
theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : } (hc : ) :
c.fst = (x).1
@[simp]
theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : } (hc : ) :
c.snd = (x).2
theorem CategoryTheory.Limits.PullbackCone.IsLimit.type_ext {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : } (hc : ) {x : c.pt} {y : c.pt} (h₁ : c.fst x = c.fst y) (h₂ : c.snd x = c.snd y) :
x = y
noncomputable def CategoryTheory.Limits.Types.pullbackIsoPullback {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :

The pullback given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback object given by PullbackObj.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) (p : ) :
(()).1 =
@[simp]
theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) (p : ) :
(()).2 =
@[simp]
theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) (x : ) :
= (fun (p : ) => (p).1) x
@[simp]
theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) (x : ) :
= (fun (p : ) => (p).2) x
@[simp]
theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :
= fun (p : ) => (p).1
@[simp]
theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :
= fun (p : ) => (p).2
inductive CategoryTheory.Limits.Types.Pushout.Rel {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
X₁ X₂X₁ X₂Prop

The pushout of two maps f : S ⟶ X₁ and g : S ⟶ X₂ is the quotient by the equivalence relation on X₁ ⊕ X₂ generated by this relation.

Instances For
def CategoryTheory.Limits.Types.Pushout {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

Construction of the pushout in the category of types, as a quotient of X₁ ⊕ X₂.

Equations
Instances For
inductive CategoryTheory.Limits.Types.Pushout.Rel' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
X₁ X₂X₁ X₂Prop

In case f : S ⟶ X₁ is a monomorphism, this relation is the equivalence relation generated by Pushout.Rel f g.

Instances For
def CategoryTheory.Limits.Types.Pushout' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

The quotient of X₁ ⊕ X₂ by the relation PushoutRel' f g.

Equations
Instances For
def CategoryTheory.Limits.Types.Pushout.inl {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

The left inclusion in the constructed pushout Pushout f g.

Equations
Instances For
def CategoryTheory.Limits.Types.Pushout.inr {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

The right inclusion in the constructed pushout Pushout f g.

Equations
Instances For
theorem CategoryTheory.Limits.Types.Pushout.condition {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
@[simp]
theorem CategoryTheory.Limits.Types.Pushout.cocone_ι_app {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
∀ (a : .obj j), .app j a = Option.rec (fun (val : CategoryTheory.Limits.WalkingPair) => ) j a
@[simp]
theorem CategoryTheory.Limits.Types.Pushout.cocone_pt {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
def CategoryTheory.Limits.Types.Pushout.cocone {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

The constructed pushout cocone in the category of types.

Equations
Instances For
def CategoryTheory.Limits.Types.Pushout.isColimitCocone {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

The cocone cocone f g is colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₁ : X₁) (y₁ : X₁) :
x₁ = y₁ ∃ (x₀ : S) (y₀ : S) (_ : g x₀ = g y₀), x₁ = f x₀ y₁ = f y₀
@[simp]
theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₁ : X₁) (x₂ : X₂) :
∃ (s : S), x₁ = f s x₂ = g s
@[simp]
theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₂ : X₂) (y₂ : X₂) :
x₂ = y₂
theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {x : X₁ X₂} {y : X₁ X₂} (h : ) :
theorem CategoryTheory.Limits.Types.Pushout.equivalence_rel' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
def CategoryTheory.Limits.Types.Pushout.equivPushout' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

The obvious equivalence Pushout f g ≃ Pushout' f g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (a : X₁ X₂) (b : X₁ X₂) :
theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₁ : X₁) (x₂ : X₂) :
∃ (s : S), f s = x₁ g s = x₂
theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {c : } {c' : } (e : c c') (x₁ : X₁) (x₂ : X₂) (h : c.inl x₁ = c.inr x₂) :
c'.inl x₁ = c'.inr x₂
theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {c : } {c' : } (e : c c') (x₁ : X₁) (x₂ : X₂) :
c.inl x₁ = c.inr x₂ c'.inl x₁ = c'.inr x₂
theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {c : } (hc : ) (h₁ : ) (x₁ : X₁) (x₂ : X₂) :
c.inl x₁ = c.inr x₂ ∃ (s : S), f s = x₁ g s = x₂
theorem CategoryTheory.Limits.MulticospanIndex.sections.ext_iff (x : I.sections) (y : I.sections) :
x = y x.val = y.val
theorem CategoryTheory.Limits.MulticospanIndex.sections.ext (x : I.sections) (y : I.sections) (val : x.val = y.val) :
x = y

Given I : MulticospanIndex (Type u), this is a type which identifies to the sections of the functor I.multicospan.

• val : (i : I.L) → I.left i

The data of an element in I.left i for each i : I.L.

• property : ∀ (r : I.R), I.fst r (self.val (I.fstTo r)) = I.snd r (self.val (I.sndTo r))
Instances For
theorem CategoryTheory.Limits.MulticospanIndex.sections.property (self : I.sections) (r : I.R) :
I.fst r (self.val (I.fstTo r)) = I.snd r (self.val (I.sndTo r))
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_symm_apply_val (s : I.multicospan.sections) (i : I.L) :
(I.sectionsEquiv.symm s).val i =
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_apply_coe (s : I.sections) (i : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) :
(I.sectionsEquiv s) i = match i with | => s.val i | => I.fst j (s.val (I.fstTo j))
def CategoryTheory.Limits.MulticospanIndex.sectionsEquiv :
I.sections I.multicospan.sections

The bijection I.sections ≃ I.multicospan.sections when I : MulticospanIndex (Type u) is a multiequalizer diagram in the category of types.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Multifork.toSections_val (x : c.pt) (i : I.L) :
(c.toSections x).val i = c i x

Given a multiequalizer diagram I : MulticospanIndex (Type u) in the category of types and c a multifork for I, this is the canonical map c.pt → I.sections.

Equations
• c.toSections x = { val := fun (i : I.L) => c i x, property := }
Instances For
theorem CategoryTheory.Limits.Multifork.toSections_fac :
I.sectionsEquiv.symm = c.toSections

A multifork c : Multifork I in the category of types is limit iff the map c.toSections : c.pt → I.sections is a bijection.

noncomputable def CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv (hc : ) :
I.sections c.pt

The bijection I.sections ≃ c.pt when c : Multifork I is a limit multifork in the category of types.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val (hc : ) (x : c.pt) (i : I.L) :
().val i = c i x
@[simp]
theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val (hc : ) (s : I.sections) (i : I.L) :
= s.val i