category_theory.limits.types

def category_theory.limits.types.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

Equations

category_theory.limits.types.limit_cone F = {X := ↥(F.sections), π := {app := λ (j : J) (u : ((category_theory.functor.const J).obj ↥(F.sections)).obj j), u.val j, naturality' := _}}

def category_theory.limits.types.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

category_theory.limits.is_limit (category_theory.limits.types.limit_cone F)

(internal implementation) the fact that the proposed limit cone is the limit

Equations

category_theory.limits.types.limit_cone_is_limit F = {lift := λ (s : category_theory.limits.cone F) (v : s.X), ⟨λ (j : J), s.π.app j v, _⟩, fac' := _, uniq' := _}

source

@[protected, instance]

def category_theory.limits.types.has_limits_of_size :

category_theory.limits.has_limits_of_size (Type (max v u))

The category of types has all limits.

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

source

@[protected, instance]

def category_theory.limits.types.sort.category_theory.limits.has_limits :

category_theory.limits.has_limits (Type u)

source

def category_theory.limits.types.is_limit_equiv_sections {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {c : category_theory.limits.cone F} (t : category_theory.limits.is_limit c) :

c.X ≃ ↥(F.sections)

The equivalence between a limiting cone of F in Type u and the "concrete" definition as the sections of F.

Equations

category_theory.limits.types.is_limit_equiv_sections t = (t.cone_point_unique_up_to_iso (category_theory.limits.types.limit_cone_is_limit F)).to_equiv

source

@[simp]

theorem category_theory.limits.types.is_limit_equiv_sections_apply {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {c : category_theory.limits.cone F} (t : category_theory.limits.is_limit c) (j : J) (x : c.X) :

↑(⇑(category_theory.limits.types.is_limit_equiv_sections t) x) j = c.π.app j x

source

@[simp]

theorem category_theory.limits.types.is_limit_equiv_sections_symm_apply {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {c : category_theory.limits.cone F} (t : category_theory.limits.is_limit c) (x : ↥(F.sections)) (j : J) :

c.π.app j (⇑((category_theory.limits.types.is_limit_equiv_sections t).symm) x) = ↑x j

source

noncomputable def category_theory.limits.types.limit_equiv_sections {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

category_theory.limits.limit F ≃ ↥(F.sections)

The equivalence between the abstract limit of F in Type u and the "concrete" definition as the sections of F.

Equations

category_theory.limits.types.limit_equiv_sections F = category_theory.limits.types.is_limit_equiv_sections (category_theory.limits.limit.is_limit F)

source

@[simp]

theorem category_theory.limits.types.limit_equiv_sections_apply {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x : category_theory.limits.limit F) (j : J) :

↑(⇑(category_theory.limits.types.limit_equiv_sections F) x) j = category_theory.limits.limit.π F j x

source

@[simp]

theorem category_theory.limits.types.limit_equiv_sections_symm_apply {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x : ↥(F.sections)) (j : J) :

category_theory.limits.limit.π F j (⇑((category_theory.limits.types.limit_equiv_sections F).symm) x) = ↑x j

source

@[simp]

theorem category_theory.limits.types.limit_equiv_sections_symm_apply' {J : Type v} [category_theory.small_category J] (F : J ⥤ Type v) (x : ↥(F.sections)) (j : J) :

category_theory.limits.limit.π F j (⇑((category_theory.limits.types.limit_equiv_sections F).symm) x) = ↑x j

source

@[ext]

noncomputable def category_theory.limits.types.limit.mk {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x : Π (j : J), F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j') :

category_theory.limits.limit F

Construct a term of limit F : Type u from a family of terms x : Π j, F.obj j which are "coherent": ∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j'.

Equations

category_theory.limits.types.limit.mk F x h = ⇑((category_theory.limits.types.limit_equiv_sections F).symm) ⟨x, h⟩

source

@[simp]

theorem category_theory.limits.types.limit.π_mk {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x : Π (j : J), F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j') (j : J) :

category_theory.limits.limit.π F j (category_theory.limits.types.limit.mk F x h) = x j

source

@[simp]

theorem category_theory.limits.types.limit.π_mk' {J : Type v} [category_theory.small_category J] (F : J ⥤ Type v) (x : Π (j : J), F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j') (j : J) :

category_theory.limits.limit.π F j (category_theory.limits.types.limit.mk F x h) = x j

source

@[ext]

theorem category_theory.limits.types.limit_ext {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x y : category_theory.limits.limit F) (w : ∀ (j : J), category_theory.limits.limit.π F j x = category_theory.limits.limit.π F j y) :

x = y

source

@[ext]

theorem category_theory.limits.types.limit_ext' {J : Type v} [category_theory.small_category J] (F : J ⥤ Type v) (x y : category_theory.limits.limit F) (w : ∀ (j : J), category_theory.limits.limit.π F j x = category_theory.limits.limit.π F j y) :

x = y

source

theorem category_theory.limits.types.limit_ext_iff {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x y : category_theory.limits.limit F) :

x = y ↔ ∀ (j : J), category_theory.limits.limit.π F j x = category_theory.limits.limit.π F j y

source

theorem category_theory.limits.types.limit_ext_iff' {J : Type v} [category_theory.small_category J] (F : J ⥤ Type v) (x y : category_theory.limits.limit F) :

x = y ↔ ∀ (j : J), category_theory.limits.limit.π F j x = category_theory.limits.limit.π F j y

source

@[simp]

theorem category_theory.limits.types.limit.w_apply {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {j j' : J} {x : category_theory.limits.limit F} (f : j ⟶ j') :

F.map f (category_theory.limits.limit.π F j x) = category_theory.limits.limit.π F j' x

source

@[simp]

theorem category_theory.limits.types.limit.lift_π_apply {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (s : category_theory.limits.cone F) (j : J) (x : s.X) :

category_theory.limits.limit.π F j (category_theory.limits.limit.lift F s x) = s.π.app j x

source

@[simp]

theorem category_theory.limits.types.limit.map_π_apply {J : Type v} [category_theory.small_category J] {F G : J ⥤ Type (max v u)} (α : F ⟶ G) (j : J) (x : category_theory.limits.limit F) :

category_theory.limits.limit.π G j (category_theory.limits.lim_map α x) = α.app j (category_theory.limits.limit.π F j x)

source

@[simp]

theorem category_theory.limits.types.limit.w_apply' {J : Type v} [category_theory.small_category J] {F : J ⥤ Type v} {j j' : J} {x : category_theory.limits.limit F} (f : j ⟶ j') :

F.map f (category_theory.limits.limit.π F j x) = category_theory.limits.limit.π F j' x

source

@[simp]

theorem category_theory.limits.types.limit.lift_π_apply' {J : Type v} [category_theory.small_category J] (F : J ⥤ Type v) (s : category_theory.limits.cone F) (j : J) (x : s.X) :

category_theory.limits.limit.π F j (category_theory.limits.limit.lift F s x) = s.π.app j x

source

@[simp]

theorem category_theory.limits.types.limit.map_π_apply' {J : Type v} [category_theory.small_category J] {F G : J ⥤ Type v} (α : F ⟶ G) (j : J) (x : category_theory.limits.limit F) :

category_theory.limits.limit.π G j (category_theory.limits.lim_map α x) = α.app j (category_theory.limits.limit.π F j x)

source

def category_theory.limits.types.quot.rel {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

(Σ (j : J), F.obj j) → (Σ (j : J), F.obj j) → Prop

The relation defining the quotient type which implements the colimit of a functor F : J ⥤ Type u. See category_theory.limits.types.quot.

Equations

category_theory.limits.types.quot.rel F = λ (p p' : Σ (j : J), F.obj j), ∃ (f : p.fst ⟶ p'.fst), p'.snd = F.map f p.snd

source

@[nolint]

def category_theory.limits.types.quot {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

Type (max v u)

A quotient type implementing the colimit of a functor F : J ⥤ Type u, as pairs ⟨j, x⟩ where x : F.obj j, modulo the equivalence relation generated by ⟨j, x⟩ ~ ⟨j', x'⟩ whenever there is a morphism f : j ⟶ j' so F.map f x = x'.

Equations

category_theory.limits.types.quot F = quot (category_theory.limits.types.quot.rel F)

Instances for category_theory.limits.types.quot

source

def category_theory.limits.types.colimit_cocone {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

category_theory.limits.cocone F

(internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

Equations

category_theory.limits.types.colimit_cocone F = {X := category_theory.limits.types.quot F, ι := {app := λ (j : J) (x : F.obj j), quot.mk (category_theory.limits.types.quot.rel F) ⟨j, x⟩, naturality' := _}}

source

def category_theory.limits.types.colimit_cocone_is_colimit {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

category_theory.limits.is_colimit (category_theory.limits.types.colimit_cocone F)

(internal implementation) the fact that the proposed colimit cocone is the colimit

Equations

category_theory.limits.types.colimit_cocone_is_colimit F = {desc := λ (s : category_theory.limits.cocone F), quot.lift (λ (p : Σ (j : J), F.obj j), s.ι.app p.fst p.snd) _, fac' := _, uniq' := _}

source

@[protected, instance]

def category_theory.limits.types.has_colimits_of_size :

category_theory.limits.has_colimits_of_size (Type (max v u))

The category of types has all colimits.

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

source

@[protected, instance]

def category_theory.limits.types.sort.category_theory.limits.has_colimits :

category_theory.limits.has_colimits (Type u)

source

noncomputable def category_theory.limits.types.colimit_equiv_quot {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) :

category_theory.limits.colimit F ≃ category_theory.limits.types.quot F

The equivalence between the abstract colimit of F in Type u and the "concrete" definition as a quotient.

Equations

category_theory.limits.types.colimit_equiv_quot F = ((category_theory.limits.colimit.is_colimit F).cocone_point_unique_up_to_iso (category_theory.limits.types.colimit_cocone_is_colimit F)).to_equiv

source

@[simp]

theorem category_theory.limits.types.colimit_equiv_quot_symm_apply {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (j : J) (x : F.obj j) :

⇑((category_theory.limits.types.colimit_equiv_quot F).symm) (quot.mk (category_theory.limits.types.quot.rel F) ⟨j, x⟩) = category_theory.limits.colimit.ι F j x

source

@[simp]

theorem category_theory.limits.types.colimit_equiv_quot_apply {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (j : J) (x : F.obj j) :

⇑(category_theory.limits.types.colimit_equiv_quot F) (category_theory.limits.colimit.ι F j x) = quot.mk (category_theory.limits.types.quot.rel F) ⟨j, x⟩

source

@[simp]

theorem category_theory.limits.types.colimit.w_apply {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {j j' : J} {x : F.obj j} (f : j ⟶ j') :

category_theory.limits.colimit.ι F j' (F.map f x) = category_theory.limits.colimit.ι F j x

source

@[simp]

theorem category_theory.limits.types.colimit.ι_desc_apply {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (s : category_theory.limits.cocone F) (j : J) (x : F.obj j) :

category_theory.limits.colimit.desc F s (category_theory.limits.colimit.ι F j x) = s.ι.app j x

source

@[simp]

theorem category_theory.limits.types.colimit.ι_map_apply {J : Type v} [category_theory.small_category J] {F G : J ⥤ Type (max v u)} (α : F ⟶ G) (j : J) (x : F.obj j) :

category_theory.limits.colim.map α (category_theory.limits.colimit.ι F j x) = category_theory.limits.colimit.ι G j (α.app j x)

source

@[simp]

theorem category_theory.limits.types.colimit.w_apply' {J : Type v} [category_theory.small_category J] {F : J ⥤ Type v} {j j' : J} {x : F.obj j} (f : j ⟶ j') :

category_theory.limits.colimit.ι F j' (F.map f x) = category_theory.limits.colimit.ι F j x

source

@[simp]

theorem category_theory.limits.types.colimit.ι_desc_apply' {J : Type v} [category_theory.small_category J] (F : J ⥤ Type v) (s : category_theory.limits.cocone F) (j : J) (x : F.obj j) :

category_theory.limits.colimit.desc F s (category_theory.limits.colimit.ι F j x) = s.ι.app j x

source

@[simp]

theorem category_theory.limits.types.colimit.ι_map_apply' {J : Type v} [category_theory.small_category J] {F G : J ⥤ Type v} (α : F ⟶ G) (j : J) (x : F.obj j) :

category_theory.limits.colim.map α (category_theory.limits.colimit.ι F j x) = category_theory.limits.colimit.ι G j (α.app j x)

source

theorem category_theory.limits.types.colimit_sound {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : F.map f x = x') :

category_theory.limits.colimit.ι F j x = category_theory.limits.colimit.ι F j' x'

source

theorem category_theory.limits.types.colimit_sound' {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {j j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j ⟶ j'') (f' : j' ⟶ j'') (w : F.map f x = F.map f' x') :

category_theory.limits.colimit.ι F j x = category_theory.limits.colimit.ι F j' x'

source

theorem category_theory.limits.types.colimit_eq {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} {j j' : J} {x : F.obj j} {x' : F.obj j'} (w : category_theory.limits.colimit.ι F j x = category_theory.limits.colimit.ι F j' x') :

eqv_gen (category_theory.limits.types.quot.rel F) ⟨j, x⟩ ⟨j', x'⟩

source

theorem category_theory.limits.types.jointly_surjective {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) {t : category_theory.limits.cocone F} (h : category_theory.limits.is_colimit t) (x : t.X) :

∃ (j : J) (y : F.obj j), t.ι.app j y = x

source

theorem category_theory.limits.types.jointly_surjective' {J : Type v} [category_theory.small_category J] {F : J ⥤ Type (max v u)} (x : category_theory.limits.colimit F) :

∃ (j : J) (y : F.obj j), category_theory.limits.colimit.ι F j y = x

A variant of jointly_surjective for x : colimit F.

source

@[protected]

def category_theory.limits.types.filtered_colimit.rel {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x y : Σ (j : J), F.obj j) :

Prop

An alternative relation on Σ j, F.obj j, which generates the same equivalence relation as we use to define the colimit in Type above, but that is more convenient when working with filtered colimits.

Elements in F.obj j and F.obj j' are equivalent if there is some k : J to the right where their images are equal.

Equations

category_theory.limits.types.filtered_colimit.rel F x y = ∃ (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k), F.map f x.snd = F.map g y.snd

source

theorem category_theory.limits.types.filtered_colimit.rel_of_quot_rel {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x y : Σ (j : J), F.obj j) :

category_theory.limits.types.quot.rel F x y → category_theory.limits.types.filtered_colimit.rel F x y

source

theorem category_theory.limits.types.filtered_colimit.eqv_gen_quot_rel_of_rel {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (x y : Σ (j : J), F.obj j) :

category_theory.limits.types.filtered_colimit.rel F x y → eqv_gen (category_theory.limits.types.quot.rel F) x y

source

noncomputable def category_theory.limits.types.filtered_colimit.is_colimit_of {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) (t : category_theory.limits.cocone F) (hsurj : ∀ (x : t.X), ∃ (i : J) (xi : F.obj i), x = t.ι.app i xi) (hinj : ∀ (i j : J) (xi : F.obj i) (xj : F.obj j), t.ι.app i xi = t.ι.app j xj → (∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj)) :

category_theory.limits.is_colimit t

Recognizing filtered colimits of types.

Equations

category_theory.limits.types.filtered_colimit.is_colimit_of F t hsurj hinj = (category_theory.limits.colimit.is_colimit F).of_iso_colimit (category_theory.limits.cocones.ext (equiv.of_bijective (category_theory.limits.colimit.desc F t) _).to_iso _)

source

@[protected]

theorem category_theory.limits.types.filtered_colimit.rel_equiv {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) [category_theory.is_filtered_or_empty J] :

equivalence (category_theory.limits.types.filtered_colimit.rel F)

source

@[protected]

theorem category_theory.limits.types.filtered_colimit.rel_eq_eqv_gen_quot_rel {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) [category_theory.is_filtered_or_empty J] :

category_theory.limits.types.filtered_colimit.rel F = eqv_gen (category_theory.limits.types.quot.rel F)

source

theorem category_theory.limits.types.filtered_colimit.colimit_eq_iff_aux {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) [category_theory.is_filtered_or_empty J] {i j : J} {xi : F.obj i} {xj : F.obj j} :

(category_theory.limits.types.colimit_cocone F).ι.app i xi = (category_theory.limits.types.colimit_cocone F).ι.app j xj ↔ category_theory.limits.types.filtered_colimit.rel F ⟨i, xi⟩ ⟨j, xj⟩

source

theorem category_theory.limits.types.filtered_colimit.is_colimit_eq_iff {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) [category_theory.is_filtered_or_empty J] {t : category_theory.limits.cocone F} (ht : category_theory.limits.is_colimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} :

t.ι.app i xi = t.ι.app j xj ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj

source

theorem category_theory.limits.types.filtered_colimit.colimit_eq_iff {J : Type v} [category_theory.small_category J] (F : J ⥤ Type (max v u)) [category_theory.is_filtered_or_empty J] {i j : J} {xi : F.obj i} {xj : F.obj j} :

category_theory.limits.colimit.ι F i xi = category_theory.limits.colimit.ι F j xj ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj

source

def category_theory.limits.types.image {α β : Type u} (f : α ⟶ β) :

Type u

the image of a morphism in Type is just set.range f

Equations

category_theory.limits.types.image f = ↥(set.range f)

Instances for category_theory.limits.types.image

category_theory.limits.types.image.inhabited

source

@[protected, instance]

def category_theory.limits.types.image.inhabited {α β : Type u} (f : α ⟶ β) [inhabited α] :

inhabited (category_theory.limits.types.image f)

Equations

category_theory.limits.types.image.inhabited f = {default := ⟨f inhabited.default, _⟩}

source

def category_theory.limits.types.image.ι {α β : Type u} (f : α ⟶ β) :

category_theory.limits.types.image f ⟶ β

the inclusion of image f into the target

Equations

category_theory.limits.types.image.ι f = subtype.val

Instances for category_theory.limits.types.image.ι

category_theory.limits.types.image.ι.category_theory.mono

source

@[protected, instance]

def category_theory.limits.types.image.ι.category_theory.mono {α β : Type u} (f : α ⟶ β) :

category_theory.mono (category_theory.limits.types.image.ι f)

source

noncomputable def category_theory.limits.types.image.lift {α β : Type u} {f : α ⟶ β} (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.types.image f ⟶ F'.I

the universal property for the image factorisation

Equations

category_theory.limits.types.image.lift F' = λ (x : category_theory.limits.types.image f), F'.e (classical.indefinite_description (λ (y : α), f y = x.val) _).val

source

theorem category_theory.limits.types.image.lift_fac {α β : Type u} {f : α ⟶ β} (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.types.image.lift F' ≫ F'.m = category_theory.limits.types.image.ι f

source

def category_theory.limits.types.mono_factorisation {α β : Type u} (f : α ⟶ β) :

category_theory.limits.mono_factorisation f

the factorisation of any morphism in Type through a mono.

Equations

category_theory.limits.types.mono_factorisation f = {I := category_theory.limits.types.image f, m := category_theory.limits.types.image.ι f, m_mono := _, e := set.range_factorization f, fac' := _}

source

noncomputable def category_theory.limits.types.is_image {α β : Type u} (f : α ⟶ β) :

category_theory.limits.is_image (category_theory.limits.types.mono_factorisation f)

the facorisation through a mono has the universal property of the image.

Equations

category_theory.limits.types.is_image f = {lift := category_theory.limits.types.image.lift f, lift_fac' := _}

source

@[protected, instance]

def category_theory.limits.types.category_theory.limits.has_image {α β : Type u} (f : α ⟶ β) :

category_theory.limits.has_image f

source

@[protected, instance]

def category_theory.limits.types.sort.category_theory.limits.has_images :

category_theory.limits.has_images (Type u)

source

@[protected, instance]

def category_theory.limits.types.sort.category_theory.limits.has_image_maps :

category_theory.limits.has_image_maps (Type u)

Equations

category_theory.limits.types.sort.category_theory.limits.has_image_maps = {has_image_map := category_theory.limits.types.sort.category_theory.limits.has_image_maps._proof_1}

mathlib documentation

Limits in the category of types. #