category_theory.limits.preserves.opposites

source

def category_theory.limits.preserves_limit_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ Cᵒᵖ) (F : C ⥤ D) [category_theory.limits.preserves_colimit K.left_op F] :

category_theory.limits.preserves_limit K F.op

If F : C ⥤ D preserves colimits of K.left_op : Jᵒᵖ ⥤ C, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of K : J ⥤ Cᵒᵖ.

Equations

category_theory.limits.preserves_limit_op K F = {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.is_limit_cone_right_op_of_cocone (K.left_op ⋙ F) (category_theory.limits.is_colimit_of_preserves F (category_theory.limits.is_colimit_cocone_left_op_of_cone K hc))}

source

def category_theory.limits.preserves_limit_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ Cᵒᵖ) (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_colimit K.left_op F] :

category_theory.limits.preserves_limit K F.left_op

If F : C ⥤ Dᵒᵖ preserves colimits of K.left_op : Jᵒᵖ ⥤ C, then F.left_op : Cᵒᵖ ⥤ D preserves limits of K : J ⥤ Cᵒᵖ.

Equations

category_theory.limits.preserves_limit_left_op K F = {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.is_limit_cone_unop_of_cocone (K.left_op ⋙ F) (category_theory.limits.is_colimit_of_preserves F (category_theory.limits.is_colimit_cocone_left_op_of_cone K hc))}

source

def category_theory.limits.preserves_limit_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ C) (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_colimit K.op F] :

category_theory.limits.preserves_limit K F.right_op

If F : Cᵒᵖ ⥤ D preserves colimits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves limits of K : J ⥤ C.

Equations

category_theory.limits.preserves_limit_right_op K F = {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.is_limit_cone_right_op_of_cocone (K.op ⋙ F) (category_theory.limits.is_colimit_of_preserves F (category_theory.limits.is_colimit_cone_op K hc))}

source

def category_theory.limits.preserves_limit_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ C) (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_colimit K.op F] :

category_theory.limits.preserves_limit K F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.unop : C ⥤ D preserves limits of K : J ⥤ C.

Equations

category_theory.limits.preserves_limit_unop K F = {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.is_limit_cone_unop_of_cocone (K.op ⋙ F) (category_theory.limits.is_colimit_of_preserves F (category_theory.limits.is_colimit_cone_op K hc))}

source

def category_theory.limits.preserves_colimit_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ Cᵒᵖ) (F : C ⥤ D) [category_theory.limits.preserves_limit K.left_op F] :

category_theory.limits.preserves_colimit K F.op

If F : C ⥤ D preserves limits of K.left_op : Jᵒᵖ ⥤ C, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of K : J ⥤ Cᵒᵖ.

Equations

category_theory.limits.preserves_colimit_op K F = {preserves := λ (c : category_theory.limits.cocone K) (hc : category_theory.limits.is_colimit c), category_theory.limits.is_colimit_cocone_right_op_of_cone (K.left_op ⋙ F) (category_theory.limits.is_limit_of_preserves F (category_theory.limits.is_limit_cone_left_op_of_cocone K hc))}

source

def category_theory.limits.preserves_colimit_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ Cᵒᵖ) (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_limit K.left_op F] :

category_theory.limits.preserves_colimit K F.left_op

If F : C ⥤ Dᵒᵖ preserves limits of K.left_op : Jᵒᵖ ⥤ C, then F.left_op : Cᵒᵖ ⥤ D preserves colimits of K : J ⥤ Cᵒᵖ.

Equations

category_theory.limits.preserves_colimit_left_op K F = {preserves := λ (c : category_theory.limits.cocone K) (hc : category_theory.limits.is_colimit c), category_theory.limits.is_colimit_cocone_unop_of_cone (K.left_op ⋙ F) (category_theory.limits.is_limit_of_preserves F (category_theory.limits.is_limit_cone_left_op_of_cocone K hc))}

source

def category_theory.limits.preserves_colimit_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ C) (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_limit K.op F] :

category_theory.limits.preserves_colimit K F.right_op

If F : Cᵒᵖ ⥤ D preserves limits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves colimits of K : J ⥤ C.

Equations

category_theory.limits.preserves_colimit_right_op K F = {preserves := λ (c : category_theory.limits.cocone K) (hc : category_theory.limits.is_colimit c), category_theory.limits.is_colimit_cocone_right_op_of_cone (K.op ⋙ F) (category_theory.limits.is_limit_of_preserves F (category_theory.limits.is_limit_cocone_op K hc))}

source

def category_theory.limits.preserves_colimit_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (K : J ⥤ C) (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_limit K.op F] :

category_theory.limits.preserves_colimit K F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.unop : C ⥤ D preserves colimits of K : J ⥤ C.

Equations

category_theory.limits.preserves_colimit_unop K F = {preserves := λ (c : category_theory.limits.cocone K) (hc : category_theory.limits.is_colimit c), category_theory.limits.is_colimit_cocone_unop_of_cone (K.op ⋙ F) (category_theory.limits.is_limit_of_preserves F (category_theory.limits.is_limit_cocone_op K hc))}

source

def category_theory.limits.preserves_limits_of_shape_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) [category_theory.limits.preserves_colimits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_limits_of_shape J F.op

If F : C ⥤ D preserves colimits of shape Jᵒᵖ, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of shape J.

Equations

category_theory.limits.preserves_limits_of_shape_op J F = {preserves_limit := λ (K : J ⥤ Cᵒᵖ), category_theory.limits.preserves_limit_op K F}

source

def category_theory.limits.preserves_limits_of_shape_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_colimits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_limits_of_shape J F.left_op

If F : C ⥤ Dᵒᵖ preserves colimits of shape Jᵒᵖ, then F.left_op : Cᵒᵖ ⥤ D preserves limits of shape J.

Equations

category_theory.limits.preserves_limits_of_shape_left_op J F = {preserves_limit := λ (K : J ⥤ Cᵒᵖ), category_theory.limits.preserves_limit_left_op K F}

source

def category_theory.limits.preserves_limits_of_shape_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_colimits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_limits_of_shape J F.right_op

If F : Cᵒᵖ ⥤ D preserves colimits of shape Jᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves limits of shape J.

Equations

category_theory.limits.preserves_limits_of_shape_right_op J F = {preserves_limit := λ (K : J ⥤ C), category_theory.limits.preserves_limit_right_op K F}

source

def category_theory.limits.preserves_limits_of_shape_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_colimits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_limits_of_shape J F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of shape Jᵒᵖ, then F.unop : C ⥤ D preserves limits of shape J.

Equations

category_theory.limits.preserves_limits_of_shape_unop J F = {preserves_limit := λ (K : J ⥤ C), category_theory.limits.preserves_limit_unop K F}

source

def category_theory.limits.preserves_colimits_of_shape_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) [category_theory.limits.preserves_limits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_colimits_of_shape J F.op

If F : C ⥤ D preserves limits of shape Jᵒᵖ, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of shape J.

Equations

category_theory.limits.preserves_colimits_of_shape_op J F = {preserves_colimit := λ (K : J ⥤ Cᵒᵖ), category_theory.limits.preserves_colimit_op K F}

source

def category_theory.limits.preserves_colimits_of_shape_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_limits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_colimits_of_shape J F.left_op

If F : C ⥤ Dᵒᵖ preserves limits of shape Jᵒᵖ, then F.left_op : Cᵒᵖ ⥤ D preserves colimits of shape J.

Equations

category_theory.limits.preserves_colimits_of_shape_left_op J F = {preserves_colimit := λ (K : J ⥤ Cᵒᵖ), category_theory.limits.preserves_colimit_left_op K F}

source

def category_theory.limits.preserves_colimits_of_shape_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_limits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_colimits_of_shape J F.right_op

If F : Cᵒᵖ ⥤ D preserves limits of shape Jᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves colimits of shape J.

Equations

category_theory.limits.preserves_colimits_of_shape_right_op J F = {preserves_colimit := λ (K : J ⥤ C), category_theory.limits.preserves_colimit_right_op K F}

source

def category_theory.limits.preserves_colimits_of_shape_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_limits_of_shape Jᵒᵖ F] :

category_theory.limits.preserves_colimits_of_shape J F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of shape Jᵒᵖ, then F.unop : C ⥤ D preserves colimits of shape J.

Equations

category_theory.limits.preserves_colimits_of_shape_unop J F = {preserves_colimit := λ (K : J ⥤ C), category_theory.limits.preserves_colimit_unop K F}

source

def category_theory.limits.preserves_limits_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_colimits F] :

category_theory.limits.preserves_limits F.op

If F : C ⥤ D preserves colimits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits.

Equations

category_theory.limits.preserves_limits_op F = {preserves_limits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_limits_of_shape_op J F}

source

def category_theory.limits.preserves_limits_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_colimits F] :

category_theory.limits.preserves_limits F.left_op

If F : C ⥤ Dᵒᵖ preserves colimits, then F.left_op : Cᵒᵖ ⥤ D preserves limits.

Equations

category_theory.limits.preserves_limits_left_op F = {preserves_limits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_limits_of_shape_left_op J F}

source

def category_theory.limits.preserves_limits_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_colimits F] :

category_theory.limits.preserves_limits F.right_op

If F : Cᵒᵖ ⥤ D preserves colimits, then F.right_op : C ⥤ Dᵒᵖ preserves limits.

Equations

category_theory.limits.preserves_limits_right_op F = {preserves_limits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_limits_of_shape_right_op J F}

source

def category_theory.limits.preserves_limits_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_colimits F] :

category_theory.limits.preserves_limits F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits, then F.unop : C ⥤ D preserves limits.

Equations

category_theory.limits.preserves_limits_unop F = {preserves_limits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_limits_of_shape_unop J F}

source

def category_theory.limits.perserves_colimits_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits F] :

category_theory.limits.preserves_colimits F.op

If F : C ⥤ D preserves limits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits.

Equations

category_theory.limits.perserves_colimits_op F = {preserves_colimits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_colimits_of_shape_op J F}

source

def category_theory.limits.preserves_colimits_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_limits F] :

category_theory.limits.preserves_colimits F.left_op

If F : C ⥤ Dᵒᵖ preserves limits, then F.left_op : Cᵒᵖ ⥤ D preserves colimits.

Equations

category_theory.limits.preserves_colimits_left_op F = {preserves_colimits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_colimits_of_shape_left_op J F}

source

def category_theory.limits.preserves_colimits_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_limits F] :

category_theory.limits.preserves_colimits F.right_op

If F : Cᵒᵖ ⥤ D preserves limits, then F.right_op : C ⥤ Dᵒᵖ preserves colimits.

Equations

category_theory.limits.preserves_colimits_right_op F = {preserves_colimits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_colimits_of_shape_right_op J F}

source

def category_theory.limits.preserves_colimits_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_limits F] :

category_theory.limits.preserves_colimits F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits, then F.unop : C ⥤ D preserves colimits.

Equations

category_theory.limits.preserves_colimits_unop F = {preserves_colimits_of_shape := λ (J : Type v₂) (_x : category_theory.category J), category_theory.limits.preserves_colimits_of_shape_unop J F}

source

def category_theory.limits.preserves_finite_limits_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_colimits F] :

category_theory.limits.preserves_finite_limits F.op

If F : C ⥤ D preserves finite colimits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite limits.

Equations

category_theory.limits.preserves_finite_limits_op F = {preserves_finite_limits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_limits_of_shape_op J F}

source

def category_theory.limits.preserves_finite_limits_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_finite_colimits F] :

category_theory.limits.preserves_finite_limits F.left_op

If F : C ⥤ Dᵒᵖ preserves finite colimits, then F.left_op : Cᵒᵖ ⥤ D preserves finite limits.

Equations

category_theory.limits.preserves_finite_limits_left_op F = {preserves_finite_limits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_limits_of_shape_left_op J F}

source

def category_theory.limits.preserves_finite_limits_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_finite_colimits F] :

category_theory.limits.preserves_finite_limits F.right_op

If F : Cᵒᵖ ⥤ D preserves finite colimits, then F.right_op : C ⥤ Dᵒᵖ preserves finite limits.

Equations

category_theory.limits.preserves_finite_limits_right_op F = {preserves_finite_limits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_limits_of_shape_right_op J F}

source

def category_theory.limits.preserves_finite_limits_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_finite_colimits F] :

category_theory.limits.preserves_finite_limits F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite colimits, then F.unop : C ⥤ D preserves finite limits.

Equations

category_theory.limits.preserves_finite_limits_unop F = {preserves_finite_limits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_limits_of_shape_unop J F}

source

def category_theory.limits.preserves_finite_colimits_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] :

category_theory.limits.preserves_finite_colimits F.op

If F : C ⥤ D preserves finite limits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite colimits.

Equations

category_theory.limits.preserves_finite_colimits_op F = {preserves_finite_colimits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_colimits_of_shape_op J F}

source

def category_theory.limits.preserves_finite_colimits_left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) [category_theory.limits.preserves_finite_limits F] :

category_theory.limits.preserves_finite_colimits F.left_op

If F : C ⥤ Dᵒᵖ preserves finite limits, then F.left_op : Cᵒᵖ ⥤ D preserves finite colimits.

Equations

category_theory.limits.preserves_finite_colimits_left_op F = {preserves_finite_colimits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_colimits_of_shape_left_op J F}

source

def category_theory.limits.preserves_finite_colimits_right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) [category_theory.limits.preserves_finite_limits F] :

category_theory.limits.preserves_finite_colimits F.right_op

If F : Cᵒᵖ ⥤ D preserves finite limits, then F.right_op : C ⥤ Dᵒᵖ preserves finite colimits.

Equations

category_theory.limits.preserves_finite_colimits_right_op F = {preserves_finite_colimits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_colimits_of_shape_right_op J F}

source

def category_theory.limits.preserves_finite_colimits_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) [category_theory.limits.preserves_finite_limits F] :

category_theory.limits.preserves_finite_colimits F.unop

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite limits, then F.unop : C ⥤ D preserves finite colimits.

Equations

category_theory.limits.preserves_finite_colimits_unop F = {preserves_finite_colimits := λ (J : Type) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), category_theory.limits.preserves_colimits_of_shape_unop J F}

mathlib3 documentation

Future work #

Limit preservation properties of functor.op and related constructions #

Future work #

Limit preservation properties of `functor.op` and related constructions #