def
category_theory.adjunction.functoriality_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C) :
Equations
- adj.functoriality_right_adjoint K = category_theory.limits.cocones.functoriality (K ⋙ F) G ⋙ category_theory.limits.cocones.precompose (K.right_unitor.inv ≫ category_theory.whisker_left K adj.unit ≫ (K.associator F G).inv)
def
category_theory.adjunction.functoriality_unit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C) :
Equations
- adj.functoriality_unit K = {app := λ (c : category_theory.limits.cocone K), {hom := adj.unit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_unit_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(c : category_theory.limits.cocone K) :
def
category_theory.adjunction.functoriality_counit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C) :
Equations
- adj.functoriality_counit K = {app := λ (c : category_theory.limits.cocone (K ⋙ F)), {hom := adj.counit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_counit_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(c : category_theory.limits.cocone (K ⋙ F)) :
def
category_theory.adjunction.functoriality_is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C) :
Equations
- adj.functoriality_is_left_adjoint K = {right := adj.functoriality_right_adjoint K, adj := category_theory.adjunction.mk_of_unit_counit {unit := adj.functoriality_unit K, counit := adj.functoriality_counit K, left_triangle' := _, right_triangle' := _}}
def
category_theory.adjunction.left_adjoint_preserves_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C} :
(F ⊣ G) → category_theory.limits.preserves_colimits F
A left adjoint preserves colimits.
Equations
- adj.left_adjoint_preserves_colimits = {preserves_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_colimit := λ (F_1 : J ⥤ C), {preserves := λ (c : category_theory.limits.cocone F_1) (hc : category_theory.limits.is_colimit c), category_theory.limits.is_colimit.iso_unique_cocone_morphism.inv (λ (s : category_theory.limits.cocone (F_1 ⋙ F)), (category_theory.is_left_adjoint.adj.hom_equiv c s).unique)}}}
@[instance]
def
category_theory.adjunction.is_equivalence_preserves_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : C ⥤ D)
[category_theory.is_equivalence E] :
@[instance]
def
category_theory.adjunction.has_colimit_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(E : C ⥤ D)
[category_theory.is_equivalence E]
[category_theory.limits.has_colimit K] :
def
category_theory.adjunction.has_colimit_of_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(E : C ⥤ D)
[category_theory.is_equivalence E]
[category_theory.limits.has_colimit (K ⋙ E)] :
def
category_theory.adjunction.functoriality_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D) :
Equations
- adj.functoriality_left_adjoint K = category_theory.limits.cones.functoriality (K ⋙ G) F ⋙ category_theory.limits.cones.postcompose ((K.associator G F).hom ≫ category_theory.whisker_left K adj.counit ≫ K.right_unitor.hom)
def
category_theory.adjunction.functoriality_unit'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D) :
Equations
- adj.functoriality_unit' K = {app := λ (c : category_theory.limits.cone (K ⋙ G)), {hom := adj.unit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_unit'_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D)
(c : category_theory.limits.cone (K ⋙ G)) :
def
category_theory.adjunction.functoriality_counit'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D) :
Equations
- adj.functoriality_counit' K = {app := λ (c : category_theory.limits.cone K), {hom := adj.counit.app c.X, w' := _}, naturality' := _}
@[simp]
theorem
category_theory.adjunction.functoriality_counit'_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D)
(c : category_theory.limits.cone K) :
def
category_theory.adjunction.functoriality_is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D) :
Equations
- adj.functoriality_is_right_adjoint K = {left := adj.functoriality_left_adjoint K, adj := category_theory.adjunction.mk_of_unit_counit {unit := adj.functoriality_unit' K, counit := adj.functoriality_counit' K, left_triangle' := _, right_triangle' := _}}
def
category_theory.adjunction.right_adjoint_preserves_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C} :
(F ⊣ G) → category_theory.limits.preserves_limits G
A right adjoint preserves limits.
Equations
- adj.right_adjoint_preserves_limits = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_limit := λ (K : J ⥤ D), {preserves := λ (c : category_theory.limits.cone K) (hc : category_theory.limits.is_limit c), category_theory.limits.is_limit.iso_unique_cone_morphism.inv (λ (s : category_theory.limits.cone (K ⋙ G)), (category_theory.is_right_adjoint.adj.hom_equiv s c).symm.unique)}}}
@[instance]
def
category_theory.adjunction.is_equivalence_preserves_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : D ⥤ C)
[category_theory.is_equivalence E] :
@[instance]
def
category_theory.adjunction.is_equivalence_reflects_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(E : D ⥤ C)
[category_theory.is_equivalence E] :
Equations
- category_theory.adjunction.is_equivalence_reflects_limits E = {reflects_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_limit := λ (K : J ⥤ D), {reflects := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit (E.map_cone c)), _.mpr (category_theory.limits.is_limit.map_cone_equiv E.fun_inv_id (category_theory.limits.preserves_limit.preserves t))}}}
@[instance]
def
category_theory.adjunction.is_equivalence_creates_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(H : D ⥤ C)
[category_theory.is_equivalence H] :
Equations
- category_theory.adjunction.is_equivalence_creates_limits H = {creates_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {creates_limit := λ (F : J ⥤ D), {to_reflects_limit := category_theory.limits.reflects_limit_of_reflects_limits_of_shape F H (category_theory.limits.reflects_limits_of_shape_of_reflects_limits H), lifts := λ (c : category_theory.limits.cone (F ⋙ H)) (t : category_theory.limits.is_limit c), {lifted_cone := H.map_cone_inv c, valid_lift := H.map_cone_map_cone_inv c}}}}
@[instance]
def
category_theory.adjunction.has_limit_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D)
(E : D ⥤ C)
[category_theory.is_equivalence E]
[category_theory.limits.has_limit K] :
def
category_theory.adjunction.has_limit_of_comp_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ D)
(E : D ⥤ C)
[category_theory.is_equivalence E]
[category_theory.limits.has_limit (K ⋙ E)] :
def
category_theory.adjunction.cocones_iso_component_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(Y : D) :
((category_theory.cocones J D).obj (opposite.op (K ⋙ F))).obj Y → (G ⋙ (category_theory.cocones J C).obj (opposite.op K)).obj Y
auxiliary construction for cocones_iso
Equations
- adj.cocones_iso_component_hom Y t = {app := λ (j : J), ⇑(adj.hom_equiv (K.obj j) Y) (t.app j), naturality' := _}
@[simp]
theorem
category_theory.adjunction.cocones_iso_component_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(Y : D)
(t : ((category_theory.cocones J D).obj (opposite.op (K ⋙ F))).obj Y)
(j : J) :
@[simp]
theorem
category_theory.adjunction.cocones_iso_component_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(Y : D)
(t : (G ⋙ (category_theory.cocones J C).obj (opposite.op K)).obj Y)
(j : J) :
def
category_theory.adjunction.cocones_iso_component_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(Y : D) :
(G ⋙ (category_theory.cocones J C).obj (opposite.op K)).obj Y → ((category_theory.cocones J D).obj (opposite.op (K ⋙ F))).obj Y
auxiliary construction for cocones_iso
Equations
- adj.cocones_iso_component_inv Y t = {app := λ (j : J), ⇑((adj.hom_equiv (K.obj j) Y).symm) (t.app j), naturality' := _}
def
category_theory.adjunction.cocones_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C} :
(category_theory.cocones J D).obj (opposite.op (K ⋙ F)) ≅ G ⋙ (category_theory.cocones J C).obj (opposite.op K)
Equations
- adj.cocones_iso = category_theory.nat_iso.of_components (λ (Y : D), {hom := adj.cocones_iso_component_hom Y, inv := adj.cocones_iso_component_inv Y, hom_inv_id' := _, inv_hom_id' := _}) _
def
category_theory.adjunction.cones_iso_component_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ D}
(X : Cᵒᵖ) :
(F.op ⋙ (category_theory.cones J D).obj K).obj X → ((category_theory.cones J C).obj (K ⋙ G)).obj X
auxiliary construction for cones_iso
Equations
- adj.cones_iso_component_hom X t = {app := λ (j : J), ⇑(adj.hom_equiv (opposite.unop X) (K.obj j)) (t.app j), naturality' := _}
@[simp]
theorem
category_theory.adjunction.cones_iso_component_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ D}
(X : Cᵒᵖ)
(t : (F.op ⋙ (category_theory.cones J D).obj K).obj X)
(j : J) :
(adj.cones_iso_component_hom X t).app j = ⇑(adj.hom_equiv (opposite.unop X) (K.obj j)) (t.app j)
def
category_theory.adjunction.cones_iso_component_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ D}
(X : Cᵒᵖ) :
((category_theory.cones J C).obj (K ⋙ G)).obj X → (F.op ⋙ (category_theory.cones J D).obj K).obj X
auxiliary construction for cones_iso
Equations
- adj.cones_iso_component_inv X t = {app := λ (j : J), ⇑((adj.hom_equiv (opposite.unop X) (K.obj j)).symm) (t.app j), naturality' := _}
@[simp]
theorem
category_theory.adjunction.cones_iso_component_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ D}
(X : Cᵒᵖ)
(t : ((category_theory.cones J C).obj (K ⋙ G)).obj X)
(j : J) :
(adj.cones_iso_component_inv X t).app j = ⇑((adj.hom_equiv (opposite.unop X) (K.obj j)).symm) (t.app j)
def
category_theory.adjunction.cones_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G)
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ D} :
F.op ⋙ (category_theory.cones J D).obj K ≅ (category_theory.cones J C).obj (K ⋙ G)
Equations
- adj.cones_iso = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), {hom := adj.cones_iso_component_hom X, inv := adj.cones_iso_component_inv X, hom_inv_id' := _, inv_hom_id' := _}) _