category_theory.limits.shapes.finite_limits

source

@[class]

structure category_theory.limits.has_finite_limits (C : Type u) [category_theory.category C] :

Prop

out : ∀ (J : Type) [𝒥 : category_theory.small_category J] [_inst_2 : category_theory.fin_category J], category_theory.limits.has_limits_of_shape J C

A category has all finite limits if every functor J ⥤ C with a fin_category J instance and J : Type has a limit.

This is often called 'finitely complete'.

Instances of this typeclass

source

@[protected, instance]

def category_theory.limits.has_limits_of_shape_of_has_finite_limits (C : Type u) [category_theory.category C] (J : Type w) [category_theory.small_category J] [category_theory.fin_category J] [category_theory.limits.has_finite_limits C] :

category_theory.limits.has_limits_of_shape J C

source

@[protected, instance]

def category_theory.limits.has_finite_limits_of_has_limits_of_size (C : Type u) [category_theory.category C] [category_theory.limits.has_limits_of_size C] :

category_theory.limits.has_finite_limits C

source

@[protected, instance]

def category_theory.limits.has_finite_limits_of_has_limits (C : Type u) [category_theory.category C] [category_theory.limits.has_limits C] :

category_theory.limits.has_finite_limits C

If C has all limits, it has finite limits.

source

theorem category_theory.limits.has_finite_limits_of_has_finite_limits_of_size (C : Type u) [category_theory.category C] (h : ∀ (J : Type w) {𝒥 : category_theory.small_category J}, category_theory.fin_category J → category_theory.limits.has_limits_of_shape J C) :

category_theory.limits.has_finite_limits C

We can always derive has_finite_limits C by providing limits at an arbitrary universe.

source

@[class]

structure category_theory.limits.has_finite_colimits (C : Type u) [category_theory.category C] :

Prop

out : ∀ (J : Type) [𝒥 : category_theory.small_category J] [_inst_2 : category_theory.fin_category J], category_theory.limits.has_colimits_of_shape J C

A category has all finite colimits if every functor J ⥤ C with a fin_category J instance and J : Type has a colimit.

This is often called 'finitely cocomplete'.

Instances of this typeclass

category_theory.limits.has_finite_colimits_of_has_colimits_of_size

source

@[protected, instance]

def category_theory.limits.has_colimits_of_shape_of_has_finite_colimits (C : Type u) [category_theory.category C] (J : Type w) [category_theory.small_category J] [category_theory.fin_category J] [category_theory.limits.has_finite_colimits C] :

category_theory.limits.has_colimits_of_shape J C

source

@[protected, instance]

def category_theory.limits.has_finite_colimits_of_has_colimits_of_size (C : Type u) [category_theory.category C] [category_theory.limits.has_colimits_of_size C] :

category_theory.limits.has_finite_colimits C

source

theorem category_theory.limits.has_finite_colimits_of_has_finite_colimits_of_size (C : Type u) [category_theory.category C] (h : ∀ (J : Type w) {𝒥 : category_theory.small_category J}, category_theory.fin_category J → category_theory.limits.has_colimits_of_shape J C) :

category_theory.limits.has_finite_colimits C

We can always derive has_finite_colimits C by providing colimits at an arbitrary universe.

source

@[protected, instance]

def category_theory.limits.fintype_walking_parallel_pair :

fintype category_theory.limits.walking_parallel_pair

Equations

category_theory.limits.fintype_walking_parallel_pair = {elems := [category_theory.limits.walking_parallel_pair.zero, category_theory.limits.walking_parallel_pair.one].to_finset, complete := category_theory.limits.fintype_walking_parallel_pair._proof_1}

source

@[protected, instance]

def category_theory.limits.walking_parallel_pair.category_theory.fin_category :

category_theory.fin_category category_theory.limits.walking_parallel_pair

Equations

category_theory.limits.walking_parallel_pair.category_theory.fin_category = {fintype_obj := category_theory.limits.fintype_walking_parallel_pair, fintype_hom := λ (j j' : category_theory.limits.walking_parallel_pair), category_theory.limits.walking_parallel_pair_hom.fintype j j'}

source

@[protected, instance]

def category_theory.limits.wide_pullback_shape.fintype_obj {J : Type v} [fintype J] :

fintype (category_theory.limits.wide_pullback_shape J)

Equations

category_theory.limits.wide_pullback_shape.fintype_obj = category_theory.limits.wide_pullback_shape.fintype_obj._proof_1.mpr option.fintype

source

@[protected, instance]

noncomputable def category_theory.limits.wide_pullback_shape.fintype_hom {J : Type v} (j j' : category_theory.limits.wide_pullback_shape J) :

fintype (j ⟶ j')

Equations

j.fintype_hom j' = {elems := option.cases_on j' (option.cases_on j {category_theory.limits.wide_pullback_shape.hom.id option.none} (λ (j : J), {category_theory.limits.wide_pullback_shape.hom.term j})) (λ (j' : J), dite (option.some j' = j) (λ (h : option.some j' = j), _.mpr {category_theory.limits.wide_pullback_shape.hom.id j}) (λ (h : ¬option.some j' = j), ∅)), complete := _}

source

@[protected, instance]

def category_theory.limits.wide_pushout_shape.fintype_obj {J : Type v} [fintype J] :

fintype (category_theory.limits.wide_pushout_shape J)

Equations

category_theory.limits.wide_pushout_shape.fintype_obj = category_theory.limits.wide_pushout_shape.fintype_obj._proof_1.mpr option.fintype

source

@[protected, instance]

noncomputable def category_theory.limits.wide_pushout_shape.fintype_hom {J : Type v} (j j' : category_theory.limits.wide_pushout_shape J) :

fintype (j ⟶ j')

Equations

j.fintype_hom j' = {elems := option.cases_on j (option.cases_on j' {category_theory.limits.wide_pushout_shape.hom.id option.none} (λ (j' : J), {category_theory.limits.wide_pushout_shape.hom.init j'})) (λ (j : J), dite (option.some j = j') (λ (h : option.some j = j'), _.mpr {category_theory.limits.wide_pushout_shape.hom.id j'}) (λ (h : ¬option.some j = j'), ∅)), complete := _}

source

@[protected, instance]

noncomputable def category_theory.limits.fin_category_wide_pullback {J : Type v} [fintype J] :

category_theory.fin_category (category_theory.limits.wide_pullback_shape J)

Equations

category_theory.limits.fin_category_wide_pullback = {fintype_obj := category_theory.limits.wide_pullback_shape.fintype_obj _inst_2, fintype_hom := category_theory.limits.wide_pullback_shape.fintype_hom J}

source

@[protected, instance]

noncomputable def category_theory.limits.fin_category_wide_pushout {J : Type v} [fintype J] :

category_theory.fin_category (category_theory.limits.wide_pushout_shape J)

Equations

category_theory.limits.fin_category_wide_pushout = {fintype_obj := category_theory.limits.wide_pushout_shape.fintype_obj _inst_2, fintype_hom := category_theory.limits.wide_pushout_shape.fintype_hom J}

source

@[class]

structure category_theory.limits.has_finite_wide_pullbacks (C : Type u) [category_theory.category C] :

Prop

out : ∀ (J : Type) [_inst_2 : fintype J], category_theory.limits.has_limits_of_shape (category_theory.limits.wide_pullback_shape J) C

has_finite_wide_pullbacks represents a choice of wide pullback for every finite collection of morphisms

source

@[protected, instance]

def category_theory.limits.has_limits_of_shape_wide_pullback_shape (C : Type u) [category_theory.category C] (J : Type) [finite J] [category_theory.limits.has_finite_wide_pullbacks C] :

category_theory.limits.has_limits_of_shape (category_theory.limits.wide_pullback_shape J) C

source

@[class]

structure category_theory.limits.has_finite_wide_pushouts (C : Type u) [category_theory.category C] :

Prop

out : ∀ (J : Type) [_inst_2 : fintype J], category_theory.limits.has_colimits_of_shape (category_theory.limits.wide_pushout_shape J) C

has_finite_wide_pushouts represents a choice of wide pushout for every finite collection of morphisms

source

@[protected, instance]

def category_theory.limits.has_colimits_of_shape_wide_pushout_shape (C : Type u) [category_theory.category C] (J : Type) [finite J] [category_theory.limits.has_finite_wide_pushouts C] :

category_theory.limits.has_colimits_of_shape (category_theory.limits.wide_pushout_shape J) C

source

theorem category_theory.limits.has_finite_wide_pullbacks_of_has_finite_limits (C : Type u) [category_theory.category C] [category_theory.limits.has_finite_limits C] :

category_theory.limits.has_finite_wide_pullbacks C

Finite wide pullbacks are finite limits, so if C has all finite limits, it also has finite wide pullbacks

source

theorem category_theory.limits.has_finite_wide_pushouts_of_has_finite_limits (C : Type u) [category_theory.category C] [category_theory.limits.has_finite_colimits C] :

category_theory.limits.has_finite_wide_pushouts C

Finite wide pushouts are finite colimits, so if C has all finite colimits, it also has finite wide pushouts

source

@[protected, instance]

def category_theory.limits.fintype_walking_pair :

fintype category_theory.limits.walking_pair

Equations

category_theory.limits.fintype_walking_pair = {elems := {category_theory.limits.walking_pair.left, category_theory.limits.walking_pair.right}, complete := category_theory.limits.fintype_walking_pair._proof_1}

mathlib3 documentation

Categories with finite limits. #