mathlib3 documentation

category_theory.category.ulift

Basic API for ulift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains a very basic API for working with the categorical instance on ulift C where C is a type with a category instance.

category_theory.ulift.up is the functorial version of the usual ulift.up.
category_theory.ulift.down is the functorial version of the usual ulift.down.
category_theory.ulift.equivalence is the categorical equivalence between C and ulift C.

ulift_hom #

Given a type C : Type u, ulift_hom.{w} C is just an alias for C. If we have category.{v} C, then ulift_hom.{w} C is endowed with a category instance whose morphisms are obtained by applying ulift.{w} to the morphisms from C.

This is a category equivalent to C. The forward direction of the equivalence is ulift_hom.up, the backward direction is ulift_hom.donw and the equivalence is ulift_hom.equiv.

as_small #

This file also contains a construction which takes a type C : Type u with a category instance category.{v} C and makes a small category as_small.{w} C : Type (max w v u) equivalent to C.

The forward direction of the equivalence, C ⥤ as_small C, is denoted as_small.up and the backward direction is as_small.down. The equivalence itself is as_small.equiv.

@[simp]

theorem category_theory.ulift.up_functor_obj_down {C : Type u₁} [category_theory.category C] (down : C) :

(category_theory.ulift.up_functor.obj down).down = down

def category_theory.ulift.up_functor {C : Type u₁} [category_theory.category C] :

The functorial version of ulift.up.

Equations

category_theory.ulift.up_functor = {obj := ulift.up C, map := λ (X Y : C) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.ulift.up_functor_map {C : Type u₁} [category_theory.category C] (X Y : C) (f : X ⟶ Y) :

category_theory.ulift.up_functor.map f = f

def category_theory.ulift.down_functor {C : Type u₁} [category_theory.category C] :

The functorial version of ulift.down.

Equations

category_theory.ulift.down_functor = {obj := ulift.down C, map := λ (X Y : ulift C) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.ulift.down_functor_obj {C : Type u₁} [category_theory.category C] (self : ulift C) :

category_theory.ulift.down_functor.obj self = self.down

@[simp]

theorem category_theory.ulift.down_functor_map {C : Type u₁} [category_theory.category C] (X Y : ulift C) (f : X ⟶ Y) :

category_theory.ulift.down_functor.map f = f

@[simp]

theorem category_theory.ulift.equivalence_inverse {C : Type u₁} [category_theory.category C] :

category_theory.ulift.equivalence.inverse = category_theory.ulift.down_functor

@[simp]

theorem category_theory.ulift.equivalence_counit_iso_inv_app {C : Type u₁} [category_theory.category C] (X : ulift C) :

category_theory.ulift.equivalence.counit_iso.inv.app X = 𝟙 ((𝟭 (ulift C)).obj X).down

@[simp]

theorem category_theory.ulift.equivalence_unit_iso_inv {C : Type u₁} [category_theory.category C] :

category_theory.ulift.equivalence.unit_iso.inv = 𝟙 (category_theory.ulift.up_functor ⋙ category_theory.ulift.down_functor)

@[simp]

theorem category_theory.ulift.equivalence_counit_iso_hom_app {C : Type u₁} [category_theory.category C] (X : ulift C) :

category_theory.ulift.equivalence.counit_iso.hom.app X = 𝟙 ((category_theory.ulift.down_functor ⋙ category_theory.ulift.up_functor).obj X).down

@[simp]

theorem category_theory.ulift.equivalence_unit_iso_hom {C : Type u₁} [category_theory.category C] :

category_theory.ulift.equivalence.unit_iso.hom = 𝟙 (𝟭 C)

@[simp]

theorem category_theory.ulift.equivalence_functor {C : Type u₁} [category_theory.category C] :

category_theory.ulift.equivalence.functor = category_theory.ulift.up_functor

def category_theory.ulift.equivalence {C : Type u₁} [category_theory.category C] :

The categorical equivalence between C and ulift C.

Equations

category_theory.ulift.equivalence = {functor := category_theory.ulift.up_functor _inst_1, inverse := category_theory.ulift.down_functor _inst_1, unit_iso := {hom := 𝟙 (𝟭 C), inv := 𝟙 (category_theory.ulift.up_functor ⋙ category_theory.ulift.down_functor), hom_inv_id' := _, inv_hom_id' := _}, counit_iso := {hom := {app := λ (X : ulift C), 𝟙 ((category_theory.ulift.down_functor ⋙ category_theory.ulift.up_functor).obj X).down, naturality' := _}, inv := {app := λ (X : ulift C), 𝟙 ((𝟭 (ulift C)).obj X).down, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}, functor_unit_iso_comp' := _}

def category_theory.ulift_hom (C : Type u) :

ulift_hom.{w} C is an alias for C, which is endowed with a category instance whose morphisms are obtained by applying ulift.{w} to the morphisms from C.

Equations

category_theory.ulift_hom C = C

Instances for category_theory.ulift_hom

@[protected, instance]

def category_theory.ulift_hom.inhabited {C : Type u_1} [inhabited C] :

inhabited (category_theory.ulift_hom C)

Equations

category_theory.ulift_hom.inhabited = {default := arbitrary C _inst_2}

def category_theory.ulift_hom.obj_down {C : Type u_1} (A : category_theory.ulift_hom C) :

C

The obvious function ulift_hom C → C.

Equations

A.obj_down = A

def category_theory.ulift_hom.obj_up {C : Type u_1} (A : C) :

category_theory.ulift_hom C

The obvious function C → ulift_hom C.

Equations

category_theory.ulift_hom.obj_up A = A

@[simp]

theorem category_theory.obj_down_obj_up {C : Type u_1} (A : C) :

(category_theory.ulift_hom.obj_up A).obj_down = A

@[simp]

theorem category_theory.obj_up_obj_down {C : Type u_1} (A : category_theory.ulift_hom C) :

category_theory.ulift_hom.obj_up A.obj_down = A

@[protected, instance]

def category_theory.ulift_hom.category {C : Type u₁} [category_theory.category C] :

category_theory.category (category_theory.ulift_hom C)

Equations

category_theory.ulift_hom.category = {to_category_struct := {to_quiver := {hom := λ (A B : category_theory.ulift_hom C), ulift (A.obj_down ⟶ B.obj_down)}, id := λ (A : category_theory.ulift_hom C), {down := 𝟙 A.obj_down}, comp := λ (A B C_1 : category_theory.ulift_hom C) (f : A ⟶ B) (g : B ⟶ C_1), {down := f.down ≫ g.down}}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.ulift_hom.up_obj {C : Type u₁} [category_theory.category C] (A : C) :

category_theory.ulift_hom.up.obj A = category_theory.ulift_hom.obj_up A

def category_theory.ulift_hom.up {C : Type u₁} [category_theory.category C] :

C ⥤ category_theory.ulift_hom C

One half of the quivalence between C and ulift_hom C.

Equations

category_theory.ulift_hom.up = {obj := category_theory.ulift_hom.obj_up C, map := λ (X Y : C) (f : X ⟶ Y), {down := f}, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.ulift_hom.up_map_down {C : Type u₁} [category_theory.category C] (X Y : C) (f : X ⟶ Y) :

(category_theory.ulift_hom.up.map f).down = f

def category_theory.ulift_hom.down {C : Type u₁} [category_theory.category C] :

category_theory.ulift_hom C ⥤ C

One half of the quivalence between C and ulift_hom C.

Equations

category_theory.ulift_hom.down = {obj := category_theory.ulift_hom.obj_down C, map := λ (X Y : category_theory.ulift_hom C) (f : X ⟶ Y), f.down, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.ulift_hom.down_map {C : Type u₁} [category_theory.category C] (X Y : category_theory.ulift_hom C) (f : X ⟶ Y) :

category_theory.ulift_hom.down.map f = f.down

@[simp]

theorem category_theory.ulift_hom.down_obj {C : Type u₁} [category_theory.category C] (A : category_theory.ulift_hom C) :

category_theory.ulift_hom.down.obj A = A.obj_down

def category_theory.ulift_hom.equiv {C : Type u₁} [category_theory.category C] :

C ≌ category_theory.ulift_hom C

The equivalence between C and ulift_hom C.

Equations

category_theory.ulift_hom.equiv = {functor := category_theory.ulift_hom.up _inst_1, inverse := category_theory.ulift_hom.down _inst_1, unit_iso := category_theory.nat_iso.of_components (λ (A : C), category_theory.eq_to_iso _) category_theory.ulift_hom.equiv._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (A : category_theory.ulift_hom C), category_theory.eq_to_iso _) category_theory.ulift_hom.equiv._proof_4, functor_unit_iso_comp' := _}

@[nolint]

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

Type (max u w v)

as_small C is a small category equivalent to C. More specifically, if C : Type u is endowed with category.{v} C, then as_small.{w} C : Type (max w v u) is endowed with an instance of a small category.

The objects and morphisms of as_small C are defined by applying ulift to the objects and morphisms of C.

Note: We require a category instance for this definition in order to have direct access to the universe level v.

Equations

category_theory.as_small C = ulift C

Instances for category_theory.as_small

@[protected, instance]

def category_theory.as_small.small_category {C : Type u₁} [category_theory.category C] :

category_theory.small_category (category_theory.as_small C)

Equations

category_theory.as_small.small_category = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.as_small C), ulift (X.down ⟶ Y.down)}, id := λ (X : category_theory.as_small C), {down := 𝟙 X.down}, comp := λ (X Y Z : category_theory.as_small C) (f : X ⟶ Y) (g : Y ⟶ Z), {down := f.down ≫ g.down}}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.as_small.up_obj_down {C : Type u₁} [category_theory.category C] (X : C) :

(category_theory.as_small.up.obj X).down = X

@[simp]

theorem category_theory.as_small.up_map_down {C : Type u₁} [category_theory.category C] (X Y : C) (f : X ⟶ Y) :

(category_theory.as_small.up.map f).down = f

def category_theory.as_small.up {C : Type u₁} [category_theory.category C] :

C ⥤ category_theory.as_small C

One half of the equivalence between C and as_small C.

Equations

category_theory.as_small.up = {obj := λ (X : C), {down := X}, map := λ (X Y : C) (f : X ⟶ Y), {down := f}, map_id' := _, map_comp' := _}

def category_theory.as_small.down {C : Type u₁} [category_theory.category C] :

category_theory.as_small C ⥤ C

One half of the equivalence between C and as_small C.

Equations

category_theory.as_small.down = {obj := λ (X : category_theory.as_small C), X.down, map := λ (X Y : category_theory.as_small C) (f : X ⟶ Y), f.down, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.as_small.down_map {C : Type u₁} [category_theory.category C] (X Y : category_theory.as_small C) (f : X ⟶ Y) :

category_theory.as_small.down.map f = f.down

@[simp]

theorem category_theory.as_small.down_obj {C : Type u₁} [category_theory.category C] (X : category_theory.as_small C) :

category_theory.as_small.down.obj X = X.down

def category_theory.as_small.equiv {C : Type u₁} [category_theory.category C] :

C ≌ category_theory.as_small C

The equivalence between C and as_small C.

Equations

category_theory.as_small.equiv = {functor := category_theory.as_small.up _inst_1, inverse := category_theory.as_small.down _inst_1, unit_iso := category_theory.nat_iso.of_components (λ (X : C), category_theory.eq_to_iso _) category_theory.as_small.equiv._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.as_small C), category_theory.eq_to_iso _) category_theory.as_small.equiv._proof_4, functor_unit_iso_comp' := _}

@[simp]

theorem category_theory.as_small.equiv_functor {C : Type u₁} [category_theory.category C] :

category_theory.as_small.equiv.functor = category_theory.as_small.up

@[simp]

theorem category_theory.as_small.equiv_inverse {C : Type u₁} [category_theory.category C] :

category_theory.as_small.equiv.inverse = category_theory.as_small.down

@[simp]

theorem category_theory.as_small.equiv_counit_iso {C : Type u₁} [category_theory.category C] :

category_theory.as_small.equiv.counit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.as_small C), category_theory.eq_to_iso _) category_theory.as_small.equiv._proof_4

@[simp]

theorem category_theory.as_small.equiv_unit_iso {C : Type u₁} [category_theory.category C] :

category_theory.as_small.equiv.unit_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.eq_to_iso _) category_theory.as_small.equiv._proof_2

@[protected, instance]

def category_theory.as_small.inhabited {C : Type u₁} [category_theory.category C] [inhabited C] :

inhabited (category_theory.as_small C)

Equations

category_theory.as_small.inhabited = {default := {down := arbitrary C _inst_2}}

def category_theory.ulift_hom_ulift_category.equiv (C : Type u) [category_theory.category C] :

C ≌ category_theory.ulift_hom (ulift C)

The equivalence between C and ulift_hom (ulift C).

Equations

category_theory.ulift_hom_ulift_category.equiv C = category_theory.ulift.equivalence.trans category_theory.ulift_hom.equiv