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.

instance CategoryTheory.Limits.Types.instHasProductsType : HasProducts (Type v)

@[simp]

theorem CategoryTheory.Limits.Types.pi_lift_π_apply {β : Type v} [Small.{u, v} β] (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : Pi.π f b (Pi.lift s x) = 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) : Pi.π f b (Pi.lift s x) = 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} [Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ᶜ f) : Pi.π g b (Pi.map α x) = α b (Pi.π f b x)

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

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

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

def CategoryTheory.Limits.Types.terminalLimitCone : LimitCone (Functor.empty (Type u))

The category of types has PUnit as a terminal object.

Equations

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

noncomputable def CategoryTheory.Limits.Types.terminalIso : ⊤_ Type u ≅ PUnit.{u + 1}

The terminal object in Type u is PUnit.

Equations

• CategoryTheory.Limits.Types.terminalIso = CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.terminalLimitCone

noncomputable def CategoryTheory.Limits.Types.isTerminalPunit : IsTerminal PUnit.{u + 1}

The terminal object in Type u is PUnit.

Equations

• CategoryTheory.Limits.Types.isTerminalPunit = CategoryTheory.Limits.terminalIsTerminal.ofIso CategoryTheory.Limits.Types.terminalIso

noncomputable instance CategoryTheory.Limits.Types.instInhabitedTerminalType : Inhabited (⊤_ Type u)

Equations

• CategoryTheory.Limits.Types.instInhabitedTerminalType = { default := CategoryTheory.Limits.terminal.from (ULift.{?u.9, 0} (Fin 1)) { down := 0 } }

instance CategoryTheory.Limits.Types.instSubsingletonTerminalType : Subsingleton (⊤_ Type u)

noncomputable instance CategoryTheory.Limits.Types.instUniqueTerminalType : Unique (⊤_ Type u)

Equations

• CategoryTheory.Limits.Types.instUniqueTerminalType = Unique.mk' (⊤_ Type ?u.9)

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivUnique (X : Type u) : IsTerminal X ≃ Unique X

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.

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit (X : Type u) : IsTerminal X ≃ (X ≅ PUnit.{u + 1})

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.

def CategoryTheory.Limits.Types.initialColimitCocone : ColimitCocone (Functor.empty (Type u))

The category of types has PEmpty as an initial object.

Equations

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

noncomputable def CategoryTheory.Limits.Types.initialIso : ⊥_ Type u ≅ PEmpty.{u + 1}

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.initialIso = CategoryTheory.Limits.colimit.isoColimitCocone CategoryTheory.Limits.Types.initialColimitCocone

noncomputable def CategoryTheory.Limits.Types.isInitialPunit : IsInitial PEmpty.{u + 1}

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.isInitialPunit = CategoryTheory.Limits.initialIsInitial.ofIso CategoryTheory.Limits.Types.initialIso

theorem CategoryTheory.Limits.Types.initial_iff_empty (X : Type u) : Nonempty (IsInitial X) ↔ IsEmpty X

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

def CategoryTheory.Limits.Types.binaryProductCone (X Y : Type u) : BinaryFan X Y

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

Equations

• CategoryTheory.Limits.Types.binaryProductCone X Y = CategoryTheory.Limits.BinaryFan.mk Prod.fst Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_pt (X Y : Type u) : (binaryProductCone X Y).pt = (X × Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_fst (X Y : Type u) : (binaryProductCone X Y).fst = _root_.Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_snd (X Y : Type u) : (binaryProductCone X Y).snd = _root_.Prod.snd

def CategoryTheory.Limits.Types.binaryProductLimit (X Y : Type u) : IsLimit (binaryProductCone X Y)

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

Equations

• CategoryTheory.Limits.Types.binaryProductLimit X Y = { lift := fun (s : CategoryTheory.Limits.BinaryFan X Y) (x : s.pt) => (s.fst x, s.snd x), fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimit_lift (X Y : Type u) (s : BinaryFan X Y) (x : s.pt) : (binaryProductLimit X Y).lift s x = (s.fst x, s.snd x)

def CategoryTheory.Limits.Types.binaryProductLimitCone (X Y : Type u) : LimitCone (pair X Y)

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

Equations

• CategoryTheory.Limits.Types.binaryProductLimitCone X Y = { cone := CategoryTheory.Limits.Types.binaryProductCone X Y, isLimit := CategoryTheory.Limits.Types.binaryProductLimit X Y }

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_cone (X Y : Type u) : (binaryProductLimitCone X Y).cone = binaryProductCone X Y

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_isLimit (X Y : Type u) : (binaryProductLimitCone X Y).isLimit = binaryProductLimit X Y

noncomputable def CategoryTheory.Limits.Types.binaryProductIso (X Y : Type u) : X ⨯ Y ≅ X × Y

The categorical binary product in Type u is cartesian product.

Equations

• CategoryTheory.Limits.Types.binaryProductIso X Y = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).hom _root_.Prod.fst = prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply (X Y : Type u) (x : X ⨯ Y) : ((binaryProductIso X Y).hom x).1 = prod.fst x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).hom _root_.Prod.snd = prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd_apply (X Y : Type u) (x : X ⨯ Y) : ((binaryProductIso X Y).hom x).2 = prod.snd x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).inv prod.fst = _root_.Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst_apply (X Y : Type u) (x : X × Y) : prod.fst ((binaryProductIso X Y).inv x) = x.1

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).inv prod.snd = _root_.Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd_apply (X Y : Type u) (x : X × Y) : prod.snd ((binaryProductIso X Y).inv x) = x.2

def CategoryTheory.Limits.Types.binaryProductFunctor : Functor (Type u) (Functor (Type u) (Type u))

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.

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_obj (X Y : Type u) : (binaryProductFunctor.obj X).obj Y = (X × Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_map_app {X₁ X₂ : Type u} (f : X₁ ⟶ X₂) (Y : Type u) (a✝ : (BinaryFan.mk (CategoryStruct.comp _root_.Prod.fst f) _root_.Prod.snd).pt) : (binaryProductFunctor.map f).app Y a✝ = (binaryProductLimit X₂ Y).lift (BinaryFan.mk (CategoryStruct.comp _root_.Prod.fst f) _root_.Prod.snd) a✝

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_map (X : Type u) {x✝ Y₂ : Type u} (f : x✝ ⟶ Y₂) (a✝ : (BinaryFan.mk _root_.Prod.fst (CategoryStruct.comp _root_.Prod.snd f)).pt) : (binaryProductFunctor.obj X).map f a✝ = (binaryProductLimit X Y₂).lift (BinaryFan.mk _root_.Prod.fst (CategoryStruct.comp _root_.Prod.snd f)) a✝

noncomputable def CategoryTheory.Limits.Types.binaryProductIsoProd : binaryProductFunctor ≅ prod.functor

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.

def CategoryTheory.Limits.Types.binaryCoproductCocone (X Y : Type u) : Cocone (pair X Y)

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

Equations

• CategoryTheory.Limits.Types.binaryCoproductCocone X Y = CategoryTheory.Limits.BinaryCofan.mk Sum.inl Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_pt (X Y : Type u) : (binaryCoproductCocone X Y).pt = (X ⊕ Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app (X Y : Type u) (x✝ : Discrete WalkingPair) (a✝ : (pair X Y).obj x✝) : (binaryCoproductCocone X Y).ι.app x✝ a✝ = (match x✝.as with | WalkingPair.left => Sum.inl | WalkingPair.right => Sum.inr) a✝

def CategoryTheory.Limits.Types.binaryCoproductColimit (X Y : Type u) : IsColimit (binaryCoproductCocone X Y)

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

Equations

• CategoryTheory.Limits.Types.binaryCoproductColimit X Y = { desc := fun (s : CategoryTheory.Limits.BinaryCofan X Y) => Sum.elim s.inl s.inr, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductColimit_desc (X Y : Type u) (s : BinaryCofan X Y) (a✝ : X ⊕ Y) : (binaryCoproductColimit X Y).desc s a✝ = Sum.elim s.inl s.inr a✝

def CategoryTheory.Limits.Types.binaryCoproductColimitCocone (X Y : Type u) : ColimitCocone (pair X Y)

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.

noncomputable def CategoryTheory.Limits.Types.binaryCoproductIso (X Y : Type u) : X ⨿ Y ≅ X ⊕ Y

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

Equations

• CategoryTheory.Limits.Types.binaryCoproductIso X Y = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom (X Y : Type u) : CategoryStruct.comp coprod.inl (binaryCoproductIso X Y).hom = Sum.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom_apply (X Y : Type u) (x : X) : (binaryCoproductIso X Y).hom (coprod.inl x) = Sum.inl x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom (X Y : Type u) : CategoryStruct.comp coprod.inr (binaryCoproductIso X Y).hom = Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom_apply (X Y : Type u) (x : Y) : (binaryCoproductIso X Y).hom (coprod.inr x) = Sum.inr x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv (X Y : Type u) : CategoryStruct.comp (asHom Sum.inl) (binaryCoproductIso X Y).inv = coprod.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv_apply (X Y : Type u) (x : X) : (binaryCoproductIso X Y).inv (asHom Sum.inl x) = coprod.inl x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv (X Y : Type u) : CategoryStruct.comp (asHom Sum.inr) (binaryCoproductIso X Y).inv = coprod.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv_apply (X Y : Type u) (x : Y) : (binaryCoproductIso X Y).inv (asHom Sum.inr x) = coprod.inr x

theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff {X Y : Type u} (c : BinaryCofan X Y) : Nonempty (IsColimit c) ↔ Function.Injective c.inl ∧ Function.Injective c.inr ∧ IsCompl (Set.range c.inl) (Set.range c.inr)

noncomputable def CategoryTheory.Limits.Types.isCoprodOfMono {X Y : Type u} (f : X ⟶ Y) [Mono f] : IsColimit (BinaryCofan.mk f Subtype.val)

Any monomorphism in Type is a coproduct injection.

Equations

• CategoryTheory.Limits.Types.isCoprodOfMono f = ⋯.some

def CategoryTheory.Limits.Types.productLimitCone {J : Type v} (F : J → Type (max v u)) : LimitCone (Discrete.functor F)

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

Equations

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

noncomputable def CategoryTheory.Limits.Types.productIso {J : Type v} (F : J → Type (max v u)) : ∏ᶜ F ≅ (j : J) → F j

The categorical product in Type max v u is the type theoretic product Π j, F j.

Equations

• CategoryTheory.Limits.Types.productIso F = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.productLimitCone F)

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval {J : Type v} (F : J → Type (max v u)) (j : J) : (CategoryStruct.comp (productIso F).hom fun (f : (j : J) → F j) => f j) = Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : ∏ᶜ F) : (productIso F).hom x j = Pi.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryStruct.comp (productIso F).inv (Pi.π F j) = fun (f : (j : J) → F j) => f j

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : (j : J) → F j) : Pi.π F j ((productIso F).inv x) = x j

noncomputable def CategoryTheory.Limits.Types.Small.productLimitCone {J : Type v} (F : J → Type u) [Small.{u, v} J] : LimitCone (Discrete.functor F)

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

Equations

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

noncomputable def CategoryTheory.Limits.Types.Small.productIso {J : Type v} (F : J → Type u) [Small.{u, v} J] : ∏ᶜ 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

• CategoryTheory.Limits.Types.Small.productIso F = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.Small.productLimitCone F)

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : (CategoryStruct.comp (productIso F).hom fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j) = Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : ∏ᶜ F) : (equivShrink ((j : J) → F j)).symm ((productIso F).hom x) j = Pi.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : CategoryStruct.comp (productIso F).inv (Pi.π F j) = 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_inv_comp_π_apply {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : Shrink.{u, max u v} ((j : J) → F j)) : Pi.π F j ((productIso F).inv x) = (equivShrink ((j : J) → F j)).symm x j

def CategoryTheory.Limits.Types.coproductColimitCocone {J : Type v} (F : J → Type (max v u)) : ColimitCocone (Discrete.functor F)

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.

noncomputable def CategoryTheory.Limits.Types.coproductIso {J : Type v} (F : J → Type (max v u)) : ∐ F ≅ (j : J) × F j

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

Equations

• CategoryTheory.Limits.Types.coproductIso F = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coproductColimitCocone F)

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryStruct.comp (Sigma.ι F j) (coproductIso F).hom = fun (x : F j) => ⟨j, x⟩

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : F j) : (coproductIso F).hom (Sigma.ι F j x) = ⟨j, x⟩

theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryStruct.comp (asHom fun (x : F j) => ⟨j, x⟩) (coproductIso F).inv = Sigma.ι F j

noncomputable def CategoryTheory.Limits.Types.typeEqualizerOfUnique {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryStruct.comp f g = CategoryStruct.comp f h) (t : ∀ (y : Y), g y = h y → ∃! x : X, f x = y) : IsLimit (Fork.ofι f w)

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.

theorem CategoryTheory.Limits.Types.unique_of_type_equalizer {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryStruct.comp f g = CategoryStruct.comp f h) (t : IsLimit (Fork.ofι f w)) (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 Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : CategoryStruct.comp f g = CategoryStruct.comp f h) : Nonempty (IsLimit (Fork.ofι f w)) ↔ ∀ (y : Y), g y = h y → ∃! x : X, f x = y

def CategoryTheory.Limits.Types.equalizerLimit {Y Z : Type u} {g h : Y ⟶ Z} : LimitCone (parallelPair g h)

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.

noncomputable def CategoryTheory.Limits.Types.equalizerIso {Y Z : Type u} (g h : Y ⟶ Z) : equalizer g h ≅ { x : Y // g x = h x }

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

Equations

• CategoryTheory.Limits.Types.equalizerIso g h = CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.equalizerLimit

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype {Y Z : Type u} (g h : Y ⟶ Z) : CategoryStruct.comp (equalizerIso g h).hom Subtype.val = equalizer.ι g h

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι {Y Z : Type u} (g h : Y ⟶ Z) : CategoryStruct.comp (equalizerIso g h).inv (equalizer.ι g h) = Subtype.val

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply {Y Z : Type u} (g h : Y ⟶ Z) (x : { x : Y // g x = h x }) : equalizer.ι g h ((equalizerIso g h).inv x) = ↑x

def CategoryTheory.Limits.Types.coequalizerColimit {X Y : Type u} (f g : X ⟶ Y) : ColimitCocone (parallelPair f g)

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.

theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq {X Y Z : Type u} (f g : X ⟶ Y) (π : Y ⟶ Z) (e : CategoryStruct.comp f π = CategoryStruct.comp g π) (h : IsColimit (Cofork.ofπ π e)) (U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) : π ⁻¹' (π '' U) = U

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

noncomputable def CategoryTheory.Limits.Types.coequalizerIso {X Y : Type u} (f g : X ⟶ Y) : coequalizer f g ≅ Function.Coequalizer f g

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

Equations

• CategoryTheory.Limits.Types.coequalizerIso f g = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coequalizerColimit f g)

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom {X Y : Type u} (f g : X ⟶ Y) : CategoryStruct.comp (coequalizer.π f g) (coequalizerIso f g).hom = Function.Coequalizer.mk f g

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply {X Y : Type u} (f g : X ⟶ Y) (x : Y) : (coequalizerIso f g).hom (coequalizer.π f g x) = Function.Coequalizer.mk f g x

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv {X Y : Type u} (f g : X ⟶ Y) : CategoryStruct.comp (asHom (Function.Coequalizer.mk f g)) (coequalizerIso f g).inv = coequalizer.π f g

instance CategoryTheory.Limits.Types.instHasPullbacksType : HasPullbacks (Type u)

instance CategoryTheory.Limits.Types.instHasPushoutsType : HasPushouts (Type u)

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.PullbackObj {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : Type u

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

• CategoryTheory.Limits.Types.PullbackObj f g = { p : X × Y // f p.1 = g p.2 }

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.pullbackCone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g

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.

def CategoryTheory.Limits.Types.pullbackLimitCone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : LimitCone (cospan f g)

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.

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_cone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (pullbackLimitCone f g).cone = pullbackCone f g

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_isLimit {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (pullbackLimitCone f g).isLimit = (pullbackCone f g).isLimitAux (fun (s : PullbackCone f g) (x : s.pt) => ⟨(s.fst x, s.snd x), ⋯⟩) ⋯ ⋯ ⋯

noncomputable def CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) : c.pt ≃ Types.PullbackObj f g

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

Equations

• CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc = (hc.conePointUniqueUpToIso (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit).toEquiv

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : c.pt) : (↑((equivPullbackObj hc) x)).1 = c.fst x

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : c.pt) : (↑((equivPullbackObj hc) x)).2 = c.snd x

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : Types.PullbackObj f g) : c.fst ((equivPullbackObj hc).symm x) = (↑x).1

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) (x : Types.PullbackObj f g) : c.snd ((equivPullbackObj hc).symm x) = (↑x).2

theorem CategoryTheory.Limits.PullbackCone.IsLimit.type_ext {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : PullbackCone f g} (hc : IsLimit c) {x y : c.pt} (h₁ : c.fst x = c.fst y) (h₂ : c.snd x = c.snd y) : x = y

def CategoryTheory.Limits.PullbackCone.toPullbackObj {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) (x : c.pt) : Types.PullbackObj f g

Given c : PullbackCone f g in the category of types, this is the canonical map c.pt → Types.PullbackObj f g.

Equations

• c.toPullbackObj x = ⟨(c.fst x, c.snd x), ⋯⟩

@[simp]

theorem CategoryTheory.Limits.PullbackCone.toPullbackObj_coe_fst {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) (x : c.pt) : (↑(c.toPullbackObj x)).1 = c.fst x

@[simp]

theorem CategoryTheory.Limits.PullbackCone.toPullbackObj_coe_snd {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) (x : c.pt) : (↑(c.toPullbackObj x)).2 = c.snd x

noncomputable def CategoryTheory.Limits.PullbackCone.isLimitEquivBijective {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} (c : PullbackCone f g) : IsLimit c ≃ Function.Bijective c.toPullbackObj

A pullback cone c in the category of types is limit iff the map c.toPullbackObj : c.pt → Types.PullbackObj f g is a bijection.

Equations

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

noncomputable def CategoryTheory.Limits.Types.pullbackIsoPullback {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ≅ PullbackObj f g

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

Equations

• CategoryTheory.Limits.Types.pullbackIsoPullback f g = (CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj (CategoryTheory.Limits.pullbackIsPullback f g)).toIso

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : pullback f g) : (↑((pullbackIsoPullback f g).hom p)).1 = pullback.fst f g p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : pullback f g) : (↑((pullbackIsoPullback f g).hom p)).2 = pullback.snd f g p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (pullbackCone f g).pt) : pullback.fst f g ((pullbackIsoPullback f g).inv x) = (fun (p : (pullbackCone f g).pt) => (↑p).1) x

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (pullbackCone f g).pt) : pullback.snd f g ((pullbackIsoPullback f g).inv x) = (fun (p : (pullbackCone f g).pt) => (↑p).2) x

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (pullbackIsoPullback f g).inv (pullback.fst f g) = fun (p : PullbackObj f g) => (↑p).1

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (pullbackIsoPullback f g).inv (pullback.snd f g) = fun (p : PullbackObj f g) => (↑p).2

inductive CategoryTheory.Limits.Types.Pushout.Rel {S X₁ 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.

• inl_inr {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S) : Rel f g (Sum.inl (f s)) (Sum.inr (g s))

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

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

Equations

• CategoryTheory.Limits.Types.Pushout f g = Quot (CategoryTheory.Limits.Types.Pushout.Rel f g)

inductive CategoryTheory.Limits.Types.Pushout.Rel' {S X₁ 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.

• refl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x : X₁ ⊕ X₂) : Rel' f g x x
• inl_inl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x₀ y₀ : S) (h : g x₀ = g y₀) : Rel' f g (Sum.inl (f x₀)) (Sum.inl (f y₀))
• inl_inr {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S) : Rel' f g (Sum.inl (f s)) (Sum.inr (g s))
• inr_inl {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S) : Rel' f g (Sum.inr (g s)) (Sum.inl (f s))

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

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

Equations

• CategoryTheory.Limits.Types.Pushout' f g = Quot (CategoryTheory.Limits.Types.Pushout.Rel' f g)

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

The left inclusion in the constructed pushout Pushout f g.

Equations

• CategoryTheory.Limits.Types.Pushout.inl f g x = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inl x)

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

The right inclusion in the constructed pushout Pushout f g.

Equations

• CategoryTheory.Limits.Types.Pushout.inr f g x = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inr x)

theorem CategoryTheory.Limits.Types.Pushout.condition {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : CategoryStruct.comp f (inl f g) = CategoryStruct.comp g (inr f g)

def CategoryTheory.Limits.Types.Pushout.cocone {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : PushoutCocone f g

The constructed pushout cocone in the category of types.

Equations

• CategoryTheory.Limits.Types.Pushout.cocone f g = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.Types.Pushout.inl f g) (CategoryTheory.Limits.Types.Pushout.inr f g) ⋯

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.cocone_ι_app {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (j : WalkingSpan) (a✝ : (span f g).obj j) : (cocone f g).ι.app j a✝ = Option.rec (CategoryStruct.comp f (inl f g)) (fun (val : WalkingPair) => WalkingPair.rec (inl f g) (inr f g) val) j a✝

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.cocone_pt {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : (cocone f g).pt = Pushout f g

def CategoryTheory.Limits.Types.Pushout.isColimitCocone {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : IsColimit (cocone f g)

The cocone cocone f g is colimit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ y₁ : X₁) : Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ 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 X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ : X₁) (x₂ : X₂) : Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ (s : S), x₁ = f s ∧ x₂ = g s

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₂ y₂ : X₂) : Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {x y : X₁ ⊕ X₂} (h : Rel' f g x y) : Rel' f g y x

theorem CategoryTheory.Limits.Types.Pushout.equivalence_rel' {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] : _root_.Equivalence (Rel' f g)

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

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

Equations

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

theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] (a b : X₁ ⊕ X₂) : Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b

theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [Mono f] (x₁ : X₁) (x₂ : X₂) : inl f g x₁ = inr f g x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c c' : PushoutCocone f g} (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 X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c c' : PushoutCocone f g} (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 X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : PushoutCocone f g} (hc : IsColimit c) (h₁ : Function.Injective f) (x₁ : X₁) (x₂ : X₂) : c.inl x₁ = c.inr x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂

structure CategoryTheory.Limits.MulticospanIndex.sections {J : MulticospanShape} (I : MulticospanIndex J (Type u)) : Type (max u u_1)

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

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

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

• property (r : J.R) : I.fst r (self.val (J.fst r)) = I.snd r (self.val (J.snd r))

theorem CategoryTheory.Limits.MulticospanIndex.sections.ext {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {x y : I.sections} (val : x.val = y.val) : x = y

def CategoryTheory.Limits.MulticospanIndex.sectionsEquiv {J : MulticospanShape} (I : MulticospanIndex J (Type u)) : 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.

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_symm_apply_val {J : MulticospanShape} (I : MulticospanIndex J (Type u)) (s : ↑I.multicospan.sections) (i : J.L) : (I.sectionsEquiv.symm s).val i = ↑s (WalkingMulticospan.left i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_apply_coe {J : MulticospanShape} (I : MulticospanIndex J (Type u)) (s : I.sections) (i : WalkingMulticospan J) : ↑(I.sectionsEquiv s) i = match i with | WalkingMulticospan.left i => s.val i | WalkingMulticospan.right j => I.fst j (s.val (J.fst j))

def CategoryTheory.Limits.Multifork.toSections {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) (x : c.pt) : I.sections

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 : J.L) => c.ι i x, property := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Multifork.toSections_val {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) (x : c.pt) (i : J.L) : (c.toSections x).val i = c.ι i x

theorem CategoryTheory.Limits.Multifork.toSections_fac {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) : ⇑I.sectionsEquiv.symm ∘ Types.sectionOfCone c = c.toSections

theorem CategoryTheory.Limits.Multifork.isLimit_types_iff {J : MulticospanShape} {I : MulticospanIndex J (Type u)} (c : Multifork I) : Nonempty (IsLimit c) ↔ Function.Bijective 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 {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {c : Multifork I} (hc : IsLimit c) : I.sections ≃ c.pt

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

Equations

• CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc = (Equiv.ofBijective c.toSections ⋯).symm

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {c : Multifork I} (hc : IsLimit c) (x : c.pt) (i : J.L) : ((sectionsEquiv hc).symm x).val i = c.ι i x

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val {J : MulticospanShape} {I : MulticospanIndex J (Type u)} {c : Multifork I} (hc : IsLimit c) (s : I.sections) (i : J.L) : c.ι i ((sectionsEquiv hc) s) = s.val i