mathlib documentation

category_theory.limits.constructions.limits_of_products_and_equalizers

Constructing limits from products and equalizers. #

If a category has all products, and all equalizers, then it has all limits. Similarly, if it has all finite products, and all equalizers, then it has all finite limits.

If a functor preserves all products and equalizers, then it preserves all limits. Similarly, if it preserves all finite products and equalizers, then it preserves all finite limits.

TODO #

Provide the dual results. Show the analogous results for functors which reflect or create (co)limits.

source
@[simp]
theorem category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit_π_app {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {F : J ⥤ C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd)} (s t : c₁.X ⟶ c₂.X) (hs : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), s ≫ c₂.π.app f = c₁.π.app f.fst.fst ≫ F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), t ≫ c₂.π.app f = c₁.π.app f.fst.snd) (i : category_theory.limits.fork s t) (j : J) :
(category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit s t hs ht i).π.app j = i.ι ≫ c₁.π.app j
source
@[simp]
theorem category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit_X {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {F : J ⥤ C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd)} (s t : c₁.X ⟶ c₂.X) (hs : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), s ≫ c₂.π.app f = c₁.π.app f.fst.fst ≫ F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), t ≫ c₂.π.app f = c₁.π.app f.fst.snd) (i : category_theory.limits.fork s t) :
(category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit s t hs ht i).X = i.X
source
def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {F : J ⥤ C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd)} (s t : c₁.X ⟶ c₂.X) (hs : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), s ≫ c₂.π.app f = c₁.π.app f.fst.fst ≫ F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), t ≫ c₂.π.app f = c₁.π.app f.fst.snd) (i : category_theory.limits.fork s t) :
category_theory.limits.cone F

(Implementation) Given the appropriate product and equalizer cones, build the cone for F which is limiting if the given cones are also.

Equations
source
def category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_is_limit {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {F : J ⥤ C} {c₁ : category_theory.limits.fan F.obj} {c₂ : category_theory.limits.fan (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd)} (s t : c₁.X ⟶ c₂.X) (hs : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), s ≫ c₂.π.app f = c₁.π.app f.fst.fst ≫ F.map f.snd) (ht : ∀ (f : Σ (p : J × J), p.fst ⟶ p.snd), t ≫ c₂.π.app f = c₁.π.app f.fst.snd) {i : category_theory.limits.fork s t} (t₁ : category_theory.limits.is_limit c₁) (t₂ : category_theory.limits.is_limit c₂) (hi : category_theory.limits.is_limit i) :
category_theory.limits.is_limit (category_theory.limits.has_limit_of_has_products_of_has_equalizers.build_limit s t hs ht i)

(Implementation) Show the cone constructed in build_limit is limiting, provided the cones used in its construction are.

Equations
source
theorem category_theory.limits.has_limit_of_equalizer_and_product {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] (F : J ⥤ C) [category_theory.limits.has_limit (category_theory.discrete.functor F.obj)] [category_theory.limits.has_limit (category_theory.discrete.functor (λ (f : Σ (p : J × J), p.fst ⟶ p.snd), F.obj f.fst.snd))] [category_theory.limits.has_equalizers C] :
category_theory.limits.has_limit F

Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of F exists. (This assumes the existence of all equalizers, which is technically stronger than needed.)

source
theorem category_theory.limits.limits_from_equalizers_and_products {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] [category_theory.limits.has_equalizers C] :
category_theory.limits.has_limits C

Any category with products and equalizers has all limits.

See https://stacks.math.columbia.edu/tag/002N.

source
theorem category_theory.limits.finite_limits_from_equalizers_and_finite_products {C : Type u} [category_theory.category C] [category_theory.limits.has_finite_products C] [category_theory.limits.has_equalizers C] :
category_theory.limits.has_finite_limits C

Any category with finite products and equalizers has all finite limits.

See https://stacks.math.columbia.edu/tag/002O.

source
def category_theory.limits.preserves_limit_of_preserves_equalizers_and_product {C : Type u} [category_theory.category C] {J : Type v} [category_theory.small_category J] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_limits_of_shape (category_theory.discrete J) C] [category_theory.limits.has_limits_of_shape (category_theory.discrete (Σ (p : J × J), p.fst ⟶ p.snd)) C] [category_theory.limits.has_equalizers C] (G : C ⥤ D) [category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair G] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete (Σ (p : J × J), p.fst ⟶ p.snd)) G] :
category_theory.limits.preserves_limits_of_shape J G

If a functor preserves equalizers and the appropriate products, it preserves limits.

Equations
source
def category_theory.limits.preserves_finite_limits_of_preserves_equalizers_and_finite_products {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_equalizers C] [category_theory.limits.has_finite_products C] (G : C ⥤ D) [category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair G] [Π (J : Type v) [_inst_8 : fintype J], category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G] (J : Type v) [category_theory.small_category J] [category_theory.fin_category J] :
category_theory.limits.preserves_limits_of_shape J G

If G preserves equalizers and finite products, it preserves finite limits.

Equations
source
def category_theory.limits.preserves_limits_of_preserves_equalizers_and_products {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_equalizers C] [category_theory.limits.has_products C] (G : C ⥤ D) [category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair G] [Π (J : Type v), category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) G] :
category_theory.limits.preserves_limits G

If G preserves equalizers and products, it preserves all limits.

Equations