mathlib docs: category_theory.limits.shapes.finite

source

@[class]

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

Prop

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

This is often called 'finitely complete'.

Equations

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

Instances

source

@[instance]

def category_theory.limits.has_limits_of_shape_of_has_finite_limits (C : Type u) [category_theory.category C] (J : Type v) [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

theorem 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

@[class]

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

Prop

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

This is often called 'finitely cocomplete'.

Equations

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

Instances

category_theory.limits.complete_lattice.has_finite_colimits_of_semilattice_sup_bot

source

@[instance]

def category_theory.limits.has_colimits_of_shape_of_has_finite_colimits (C : Type u) [category_theory.category C] (J : Type v) [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

theorem category_theory.limits.has_finite_colimits_of_has_colimits (C : Type u) [category_theory.category C] [category_theory.limits.has_colimits C] :

category_theory.limits.has_finite_colimits C

If C has all colimits, it has finite colimits.

source

@[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

@[instance]

def category_theory.limits.category_theory.fin_category :

category_theory.fin_category category_theory.limits.walking_parallel_pair

Equations

category_theory.limits.category_theory.fin_category = {decidable_eq_obj := λ (a b : category_theory.limits.walking_parallel_pair), category_theory.limits.walking_parallel_pair.decidable_eq a b, fintype_obj := category_theory.limits.fintype_walking_parallel_pair, decidable_eq_hom := λ (j j' : category_theory.limits.walking_parallel_pair) (a b : j ⟶ j'), category_theory.limits.walking_parallel_pair_hom.decidable_eq j j' a b, fintype_hom := λ (j j' : category_theory.limits.walking_parallel_pair), category_theory.limits.fintype j j'}

source

@[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

@[instance]

def category_theory.limits.wide_pullback_shape.fintype_hom {J : Type v} [decidable_eq J] (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 none} (λ (j : J), {category_theory.limits.wide_pullback_shape.hom.term j})) (λ (j' : J), dite (some j' = j) (λ (h : some j' = j), _.mpr {category_theory.limits.wide_pullback_shape.hom.id j}) (λ (h : ¬some j' = j), ∅)), complete := _}

source

@[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

@[instance]

def category_theory.limits.wide_pushout_shape.fintype_hom {J : Type v} [decidable_eq J] (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 none} (λ (j' : J), {category_theory.limits.wide_pushout_shape.hom.init j'})) (λ (j : J), dite (some j = j') (λ (h : some j = j'), _.mpr {category_theory.limits.wide_pushout_shape.hom.id j'}) (λ (h : ¬some j = j'), ∅)), complete := _}

source

@[instance]

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

category_theory.fin_category (category_theory.limits.wide_pullback_shape J)

Equations

category_theory.limits.fin_category_wide_pullback = {decidable_eq_obj := λ (a b : category_theory.limits.wide_pullback_shape J), option.decidable_eq a b, fintype_obj := category_theory.limits.wide_pullback_shape.fintype_obj _inst_3, decidable_eq_hom := λ (j j' : category_theory.limits.wide_pullback_shape J) (a b : j ⟶ j'), category_theory.limits.wide_pullback_shape.hom.decidable_eq j j' a b, fintype_hom := category_theory.limits.wide_pullback_shape.fintype_hom (λ (a b : J), _inst_2 a b)}

source

@[instance]

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

category_theory.fin_category (category_theory.limits.wide_pushout_shape J)

Equations

category_theory.limits.fin_category_wide_pushout = {decidable_eq_obj := λ (a b : category_theory.limits.wide_pushout_shape J), option.decidable_eq a b, fintype_obj := category_theory.limits.wide_pushout_shape.fintype_obj _inst_3, decidable_eq_hom := λ (j j' : category_theory.limits.wide_pushout_shape J) (a b : j ⟶ j'), category_theory.limits.wide_pushout_shape.hom.decidable_eq j j' a b, fintype_hom := category_theory.limits.wide_pushout_shape.fintype_hom (λ (a b : J), _inst_2 a b)}

source

@[class]

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

Prop

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

Equations

category_theory.limits.has_finite_wide_pullbacks C = ∀ (J : Type v) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape (category_theory.limits.wide_pullback_shape J) C

source

@[instance]

def category_theory.limits.has_limits_of_shape_wide_pullback_shape (C : Type u) [category_theory.category C] (J : Type v) [fintype 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]

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

Prop

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

Equations

category_theory.limits.has_finite_wide_pushouts C = ∀ (J : Type v) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_colimits_of_shape (category_theory.limits.wide_pushout_shape J) C

source

@[instance]

def category_theory.limits.has_colimits_of_shape_wide_pushout_shape (C : Type u) [category_theory.category C] (J : Type v) [fintype 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

@[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}

mathlib documentation

Categories with finite limits.