Special shapes for limits in Type. #
The general shape (co)limits defined in category_theory.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
XandYisX × Y - the product of a family
f : J → TypeisΠ j, f j - the coproduct of a family
f : J → TypeisΣ j, f j - the binary coproduct of
XandYis the sum typeX ⊕ 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 ofYby∀ x : Y, f x ~ g x - the pullback of
f : X ⟶ Zandg : Y ⟶ Zis the subtype{ p : X × Y // f p.1 = g p.2 }of the product
We first construct terms of is_limit and limit_cone, and then provide isomorphisms with the
types generated by the has_limit API.
As an example, when setting up the monoidal category structure on Type
we use the types_has_terminal and types_has_binary_products instances.
@[simp]
theorem
category_theory.limits.types.pi_lift_π_apply
{β : Type u}
(f : β → Type u)
{P : Type u}
(s : Π (b : β), P ⟶ f b)
(b : β)
(x : P) :
category_theory.limits.pi.π f b (category_theory.limits.pi.lift s x) = s b x
A restatement of types.lift_π_apply that uses pi.π and pi.lift.
@[simp]
theorem
category_theory.limits.types.pi_map_π_apply
{β : Type u}
{f g : β → Type u}
(α : Π (j : β), f j ⟶ g j)
(b : β)
(x : ∏ λ (j : β), f j) :
category_theory.limits.pi.π g b (category_theory.limits.pi.map α x) = α b (category_theory.limits.pi.π f b x)
A restatement of types.map_π_apply that uses pi.π and pi.map.
The category of types has punit as a terminal object.
Equations
- category_theory.limits.types.terminal_limit_cone = {cone := {X := punit, π := {app := category_theory.limits.types.terminal_limit_cone._aux_1, naturality' := category_theory.limits.types.terminal_limit_cone._proof_1}}, is_limit := id {lift := category_theory.limits.types.terminal_limit_cone._aux_2, fac' := category_theory.limits.types.terminal_limit_cone._proof_3, uniq' := category_theory.limits.types.terminal_limit_cone._proof_4}}
The terminal object in Type u is punit.
The category of types has pempty as an initial object.
Equations
- category_theory.limits.types.initial_colimit_cocone = {cocone := {X := pempty, ι := {app := category_theory.limits.types.initial_colimit_cocone._aux_1, naturality' := category_theory.limits.types.initial_colimit_cocone._proof_1}}, is_colimit := id {desc := category_theory.limits.types.initial_colimit_cocone._aux_2, fac' := category_theory.limits.types.initial_colimit_cocone._proof_3, uniq' := category_theory.limits.types.initial_colimit_cocone._proof_4}}
The initial object in Type u is punit.
The product type X × Y forms a cone for the binary product of X and Y.
@[simp]
theorem
category_theory.limits.types.binary_product_cone_X
(X Y : Type u) :
(category_theory.limits.types.binary_product_cone X Y).X = (X × Y)
@[simp]
@[simp]
@[simp]
theorem
category_theory.limits.types.binary_product_limit_lift
(X Y : Type u)
(s : category_theory.limits.binary_fan X Y)
(x : s.X) :
(category_theory.limits.types.binary_product_limit X Y).lift s x = (s.fst x, s.snd x)
The product type X × Y is a binary product for X and Y.
Equations
- category_theory.limits.types.binary_product_limit X Y = {lift := λ (s : category_theory.limits.binary_fan X Y) (x : s.X), (s.fst x, s.snd x), fac' := _, uniq' := _}
The category of types has X × Y, the usual cartesian product,
as the binary product of X and Y.
@[simp]
@[simp]
The categorical binary product in Type u is cartesian product.
@[simp]
theorem
category_theory.limits.types.binary_product_iso_hom_comp_fst_apply
(X Y : Type u)
(x : ↥(X ⨯ Y)) :
@[simp]
@[simp]
@[simp]
theorem
category_theory.limits.types.binary_product_iso_hom_comp_snd_apply
(X Y : Type u)
(x : ↥(X ⨯ Y)) :
@[simp]
theorem
category_theory.limits.types.binary_product_iso_inv_comp_fst_apply
(X Y : Type u)
(x : ↥(X × Y)) :
@[simp]
@[simp]
@[simp]
theorem
category_theory.limits.types.binary_product_iso_inv_comp_snd_apply
(X Y : Type u)
(x : ↥(X × Y)) :
The functor which sends X, Y to the product type X × Y.
Equations
- category_theory.limits.types.binary_product_functor = {obj := λ (X : Type u), {obj := λ (Y : Type u), X × Y, map := λ (Y₁ Y₂ : Type u) (f : Y₁ ⟶ Y₂), (category_theory.limits.types.binary_product_limit X Y₂).lift (category_theory.limits.binary_fan.mk prod.fst (prod.snd ≫ f)), map_id' := _, map_comp' := _}, map := λ (X₁ X₂ : Type u) (f : X₁ ⟶ X₂), {app := λ (Y : Type u), (category_theory.limits.types.binary_product_limit X₂ Y).lift (category_theory.limits.binary_fan.mk (prod.fst ≫ f) prod.snd), naturality' := _}, map_id' := category_theory.limits.types.binary_product_functor._proof_8, map_comp' := category_theory.limits.types.binary_product_functor._proof_9}
@[simp]
theorem
category_theory.limits.types.binary_product_functor_obj_obj
(X Y : Type u) :
(category_theory.limits.types.binary_product_functor.obj X).obj Y = (X × Y)
@[simp]
theorem
category_theory.limits.types.binary_product_functor_map_app
(X₁ X₂ : Type u)
(f : X₁ ⟶ X₂)
(Y : Type u) :
@[simp]
theorem
category_theory.limits.types.binary_product_functor_obj_map
(X Y₁ Y₂ : Type u)
(f : Y₁ ⟶ Y₂) :
The product functor given by the instance has_binary_products (Type u) is isomorphic to the
explicit binary product functor given by the product type.
Equations
- category_theory.limits.types.binary_product_iso_prod = category_theory.nat_iso.of_components (λ (X : Type u), category_theory.nat_iso.of_components (λ (Y : Type u), ((category_theory.limits.limit.is_limit (category_theory.limits.pair X Y)).cone_point_unique_up_to_iso (category_theory.limits.types.binary_product_limit X Y)).symm) _) category_theory.limits.types.binary_product_iso_prod._proof_6
@[simp]
theorem
category_theory.limits.types.binary_coproduct_cocone_X
(X Y : Type u) :
(category_theory.limits.types.binary_coproduct_cocone X Y).X = (X ⊕ Y)
The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.
@[simp]
theorem
category_theory.limits.types.binary_coproduct_cocone_ι_app
(X Y : Type u)
(j : category_theory.discrete category_theory.limits.walking_pair)
(ᾰ : (category_theory.limits.pair X Y).obj j) :
The sum type X ⊕ Y is a binary coproduct for X and Y.
Equations
- category_theory.limits.types.binary_coproduct_colimit X Y = {desc := λ (s : category_theory.limits.binary_cofan X Y), sum.elim s.inl s.inr, fac' := _, uniq' := _}
@[simp]
theorem
category_theory.limits.types.binary_coproduct_colimit_desc
(X Y : Type u)
(s : category_theory.limits.binary_cofan X Y)
(ᾰ : X ⊕ Y) :
The category of types has X ⊕ Y,
as the binary coproduct of X and Y.
The categorical binary coproduct in Type u is the sum X ⊕ Y.
@[simp]
theorem
category_theory.limits.types.binary_coproduct_iso_inl_comp_hom_apply
(X Y : Type u)
(x : ↥X) :
@[simp]
@[simp]
theorem
category_theory.limits.types.binary_coproduct_iso_inr_comp_hom_apply
(X Y : Type u)
(x : ↥Y) :
@[simp]
@[simp]
@[simp]
theorem
category_theory.limits.types.binary_coproduct_iso_inl_comp_inv_apply
(X Y : Type u)
(x : ↥X) :
@[simp]
theorem
category_theory.limits.types.binary_coproduct_iso_inr_comp_inv_apply
(X Y : Type u)
(x : ↥Y) :
@[simp]
The category of types has Π j, f j as the product of a type family f : J → Type.
Equations
- category_theory.limits.types.product_limit_cone F = {cone := {X := Π (j : J), F j, π := {app := λ (j : category_theory.discrete J) (f : ((category_theory.functor.const (category_theory.discrete J)).obj (Π (j : J), F j)).obj j), f j, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor F)) (x : s.X) (j : J), s.π.app j x, fac' := _, uniq' := _}}
The categorical product in Type u is the type theoretic product Π j, F j.
@[simp]
theorem
category_theory.limits.types.product_iso_hom_comp_eval
{J : Type u}
(F : J → Type u)
(j : J) :
((category_theory.limits.types.product_iso F).hom ≫ λ (f : Π (j : J), F j), f j) = category_theory.limits.pi.π F j
@[simp]
theorem
category_theory.limits.types.product_iso_hom_comp_eval_apply
{J : Type u}
(F : J → Type u)
(j : J)
(x : ↥∏ F) :
@[simp]
theorem
category_theory.limits.types.product_iso_inv_comp_π
{J : Type u}
(F : J → Type u)
(j : J) :
(category_theory.limits.types.product_iso F).inv ≫ category_theory.limits.pi.π F j = λ (f : Π (j : J), F j), f j
@[simp]
theorem
category_theory.limits.types.product_iso_inv_comp_π_apply
{J : Type u}
(F : J → Type u)
(j : J)
(x : ↥(Π (j : J), F j)) :
category_theory.limits.pi.π F j ((category_theory.limits.types.product_iso F).inv x) = x j
The category of types has Σ j, f j as the coproduct of a type family f : J → Type.
Equations
- category_theory.limits.types.coproduct_colimit_cocone F = {cocone := {X := Σ (j : J), F j, ι := {app := λ (j : category_theory.discrete J) (x : (category_theory.discrete.functor F).obj j), ⟨j, x⟩, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone (category_theory.discrete.functor F)) (x : {X := Σ (j : J), F j, ι := {app := λ (j : category_theory.discrete J) (x : (category_theory.discrete.functor F).obj j), ⟨j, x⟩, naturality' := _}}.X), s.ι.app x.fst x.snd, fac' := _, uniq' := _}}
The categorical coproduct in Type u is the type theoretic coproduct Σ j, F j.
@[simp]
theorem
category_theory.limits.types.coproduct_iso_ι_comp_hom_apply
{J : Type u}
(F : J → Type u)
(j : J)
(x : ↥(F j)) :
(category_theory.limits.types.coproduct_iso F).hom (category_theory.limits.sigma.ι F j x) = ⟨j, x⟩
@[simp]
theorem
category_theory.limits.types.coproduct_iso_ι_comp_hom
{J : Type u}
(F : J → Type u)
(j : J) :
category_theory.limits.sigma.ι F j ≫ (category_theory.limits.types.coproduct_iso F).hom = λ (x : F j), ⟨j, x⟩
@[simp]
theorem
category_theory.limits.types.coproduct_iso_mk_comp_inv_apply
{J : Type u}
(F : J → Type u)
(j : J)
(x : ↥(F j)) :
@[simp]
theorem
category_theory.limits.types.coproduct_iso_mk_comp_inv
{J : Type u}
(F : J → Type u)
(j : J) :
category_theory.as_hom (λ (x : F j), ⟨j, x⟩) ≫ (category_theory.limits.types.coproduct_iso F).inv = category_theory.limits.sigma.ι F j
noncomputable
def
category_theory.limits.types.type_equalizer_of_unique
{X Y Z : Type u}
(f : X ⟶ Y)
{g h : Y ⟶ Z}
(w : f ≫ g = f ≫ h)
(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
- category_theory.limits.types.type_equalizer_of_unique f w t = category_theory.limits.fork.is_limit.mk' (category_theory.limits.fork.of_ι f w) (λ (s : category_theory.limits.fork g h), ⟨λ (i : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero), classical.some _, _⟩)
theorem
category_theory.limits.types.unique_of_type_equalizer
{X Y Z : Type u}
(f : X ⟶ Y)
{g h : Y ⟶ Z}
(w : f ≫ g = f ≫ h)
(t : category_theory.limits.is_limit (category_theory.limits.fork.of_ι f w))
(y : Y)
(hy : g y = h y) :
∃! (x : X), f x = y
The converse of type_equalizer_of_unique.
theorem
category_theory.limits.types.type_equalizer_iff_unique
{X Y Z : Type u}
(f : X ⟶ Y)
{g h : Y ⟶ Z}
(w : f ≫ g = f ≫ h) :
nonempty (category_theory.limits.is_limit (category_theory.limits.fork.of_ι f w)) ↔ ∀ (y : Y), g y = h y → (∃! (x : X), f x = y)
Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).
Equations
- category_theory.limits.types.equalizer_limit = {cone := category_theory.limits.fork.of_ι subtype.val category_theory.limits.types.equalizer_limit._proof_1, is_limit := category_theory.limits.fork.is_limit.mk' (category_theory.limits.fork.of_ι subtype.val category_theory.limits.types.equalizer_limit._proof_1) (λ (s : category_theory.limits.fork g h), ⟨λ (i : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.zero), ⟨s.ι i, _⟩, _⟩)}
noncomputable
def
category_theory.limits.types.equalizer_iso
{Y Z : Type u}
(g h : Y ⟶ Z) :
category_theory.limits.equalizer g h ≅ {x // g x = h x}
The categorical equalizer in Type u is {x : Y // g x = h x}.
@[simp]
@[simp]
theorem
category_theory.limits.types.equalizer_iso_hom_comp_subtype_apply
{Y Z : Type u}
(g h : Y ⟶ Z)
(x : ↥(category_theory.limits.equalizer g h)) :
@[simp]
@[simp]
theorem
category_theory.limits.types.equalizer_iso_inv_comp_ι_apply
{Y Z : Type u}
(g h : Y ⟶ Z)
(x : ↥{x // g x = h x}) :
- rel : ∀ {X Y : Type u} {f g : X ⟶ Y} (x : X), category_theory.limits.types.coequalizer_rel f g (f x) (g x)
(Implementation) The relation to be quotiented to obtain the coequalizer.
Show that the quotient by the relation generated by f(x) ~ g(x)
is a coequalizer for the pair (f, g).
Equations
- category_theory.limits.types.coequalizer_colimit f g = {cocone := category_theory.limits.cofork.of_π (quot.mk (category_theory.limits.types.coequalizer_rel f g)) _, is_colimit := category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cofork.of_π (quot.mk (category_theory.limits.types.coequalizer_rel f g)) _) (λ (s : category_theory.limits.cofork f g), ⟨quot.lift s.π _, _⟩)}
theorem
category_theory.limits.types.coequalizer_preimage_image_eq_of_preimage_eq
{X Y Z : Type u}
(f g : X ⟶ Y)
(π : Y ⟶ Z)
(e : f ≫ π = g ≫ π)
(h : category_theory.limits.is_colimit (category_theory.limits.cofork.of_π π e))
(U : set Y)
(H : f ⁻¹' U = g ⁻¹' U) :
If π : Y ⟶ Z is an equalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U,
then π ⁻¹' (π '' U) = U.
The categorical coequalizer in Type u is the quotient by f g ~ g x.
@[simp]
theorem
category_theory.limits.types.coequalizer_iso_π_comp_hom_apply
{X Y : Type u}
(f g : X ⟶ Y)
(x : ↥Y) :
(category_theory.limits.types.coequalizer_iso f g).hom (category_theory.limits.coequalizer.π f g x) = quot.mk (category_theory.limits.types.coequalizer_rel f g) x
@[simp]
@[simp]
theorem
category_theory.limits.types.coequalizer_iso_quot_comp_inv_apply
{X Y : Type u}
(f g : X ⟶ Y)
(x : ↥Y) :
@[simp]
@[nolint]
The usual explicit pullback in the category of types, as a subtype of the product.
The full limit_cone data is bundled as pullback_limit_cone f g.
The explicit pullback cone on pullback_obj f g.
This is bundled with the is_limit data as pullback_limit_cone f g.
The explicit pullback in the category of types, bundled up as a limit_cone
for given f and g.
Equations
- category_theory.limits.types.pullback_limit_cone f g = {cone := category_theory.limits.types.pullback_cone f g, is_limit := (category_theory.limits.types.pullback_cone f g).is_limit_aux (λ (s : category_theory.limits.pullback_cone f g) (x : s.X), ⟨(s.fst x, s.snd x), _⟩) _ _ _}
@[simp]
theorem
category_theory.limits.types.pullback_limit_cone_is_limit
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
(category_theory.limits.types.pullback_limit_cone f g).is_limit = (category_theory.limits.types.pullback_cone f g).is_limit_aux (λ (s : category_theory.limits.pullback_cone f g) (x : s.X), ⟨(s.fst x, s.snd x), _⟩) _ _ _
@[simp]
theorem
category_theory.limits.types.pullback_limit_cone_cone
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
noncomputable
def
category_theory.limits.types.pullback_cone_iso_pullback
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
The pullback cone given by the instance has_pullbacks (Type u) is isomorphic to the
explicit pullback cone given by pullback_limit_cone.
noncomputable
def
category_theory.limits.types.pullback_iso_pullback
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
The pullback given by the instance has_pullbacks (Type u) is isomorphic to the
explicit pullback object given by pullback_limit_obj.
@[simp]
theorem
category_theory.limits.types.pullback_iso_pullback_hom_fst
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(p : category_theory.limits.pullback f g) :
@[simp]
theorem
category_theory.limits.types.pullback_iso_pullback_hom_snd
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(p : category_theory.limits.pullback f g) :
@[simp]
theorem
category_theory.limits.types.pullback_iso_pullback_inv_fst
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.limits.types.pullback_iso_pullback_inv_snd
{X Y Z : Type u}
(f : X ⟶ Z)
(g : Y ⟶ Z) :