mathlib docs: category_theory.limits.shapes.finite

source

@[instance]

def category_theory.discrete_fintype {α : Type u_1} [fintype α] :

fintype (category_theory.discrete α)

Equations

category_theory.discrete_fintype = id _inst_1

source

@[instance]

def category_theory.discrete_hom_fintype {α : Type u_1} [decidable_eq α] (X Y : category_theory.discrete α) :

fintype (X ⟶ Y)

Equations

category_theory.discrete_hom_fintype X Y = ulift.fintype (plift (X = Y))

source

@[class]

structure category_theory.fin_category (J : Type v) [category_theory.small_category J] :

Type v

decidable_eq_obj : decidable_eq J . "apply_instance"
fintype_obj : fintype J . "apply_instance"
decidable_eq_hom : (Π (j j' : J), decidable_eq (j ⟶ j')) . "apply_instance"
fintype_hom : (Π (j j' : J), fintype (j ⟶ j')) . "apply_instance"

A category with a fintype of objects, and a fintype for each morphism space.

Instances

source

@[instance]

def category_theory.fin_category_discrete_of_decidable_fintype (J : Type v) [decidable_eq J] [fintype J] :

category_theory.fin_category (category_theory.discrete J)

Equations

category_theory.fin_category_discrete_of_decidable_fintype J = {decidable_eq_obj := λ (a b : category_theory.discrete J), _inst_1 a b, fintype_obj := category_theory.discrete_fintype _inst_2, decidable_eq_hom := λ (j j' : category_theory.discrete J) (a b : j ⟶ j'), ulift.decidable_eq a b, fintype_hom := λ (j j' : category_theory.discrete J), category_theory.discrete_hom_fintype j j'}

source

@[class]

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

Type (max (v+1) u)

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

Equations

category_theory.limits.has_limits_of_shape_of_has_finite_limits C J = _inst_4 J

source

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.

Equations

category_theory.limits.has_finite_limits_of_has_limits C = λ (J : Type v) (𝒥₁ : category_theory.small_category J) (𝒥₂ : category_theory.fin_category J), infer_instance

source

@[class]

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

Type (max (v+1) u)

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.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

Equations

category_theory.limits.has_colimits_of_shape_of_has_finite_colimits C J = _inst_4 J

source

def 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.

Equations

category_theory.limits.has_finite_colimits_of_has_colimits C = λ (J : Type v) (𝒥₁ : category_theory.small_category J) (𝒥₂ : category_theory.fin_category J), infer_instance

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

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

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

Type (max (v+1) u)

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) [decidable_eq J] [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

Equations

category_theory.limits.has_limits_of_shape_wide_pullback_shape C J = _inst_4 J

source

@[class]

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

Type (max (v+1) u)

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) [decidable_eq J] [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

Equations

category_theory.limits.has_colimits_of_shape_wide_pushout_shape C J = _inst_4 J

source

def 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

Equations

category_theory.limits.has_finite_wide_pullbacks_of_has_finite_limits C = λ (J : Type v) (_x : decidable_eq J) (_x_1 : fintype J), category_theory.limits.has_limits_of_shape_of_has_finite_limits C (category_theory.limits.wide_pullback_shape J)

source

def 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

Equations

category_theory.limits.has_finite_wide_pushouts_of_has_finite_limits C = λ (J : Type v) (_x : decidable_eq J) (_x_1 : fintype J), category_theory.limits.has_colimits_of_shape_of_has_finite_colimits C (category_theory.limits.wide_pushout_shape J)

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

category_theory.limits.shapes.finite_limits

General documentation

Additional documentation

Library

mathlib documentation

category_theory.​limits.​shapes.​finite_limits

General documentation

Additional documentation

Library

category_theory.limits.shapes.finite_limits