The category of "structured arrows" #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For T : C ⥤ D, a T-structured arrow with source S : D
is just a morphism S ⟶ T.obj Y, for some Y : C.
These form a category with morphisms g : Y ⟶ Y' making the obvious diagram commute.
We prove that 𝟙 (T.obj Y) is the initial object in T-structured objects with source T.obj Y.
@[nolint]
def
category_theory.structured_arrow
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : D)
(T : C ⥤ D) :
Type (max u₁ v₂)
The category of T-structured arrows with domain S : D (here T : C ⥤ D),
has as its objects D-morphisms of the form S ⟶ T Y, for some Y : C,
and morphisms C-morphisms Y ⟶ Y' making the obvious triangle commute.
Equations
Instances for category_theory.structured_arrow
- category_theory.structured_arrow.category
- category_theory.structured_arrow.has_limits_of_shape
- category_theory.structured_arrow.has_limits
- category_theory.representably_flat.cofiltered
- category_theory.Ran_is_sheaf_of_cover_lifting.category_theory.limits.has_limits_of_shape
- category_theory.functor.final.out
- category_theory.functor.final.category_theory.structured_arrow.nonempty
- Top.presheaf.sheaf_condition.category_theory.structured_arrow.nonempty
- category_theory.structured_arrow.well_powered_structured_arrow
@[protected, instance]
def
category_theory.structured_arrow.category
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : D)
(T : C ⥤ D) :
@[simp]
theorem
category_theory.structured_arrow.proj_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : D)
(T : C ⥤ D)
(_x _x_1 : category_theory.comma (category_theory.functor.from_punit S) T)
(f : _x ⟶ _x_1) :
(category_theory.structured_arrow.proj S T).map f = f.right
def
category_theory.structured_arrow.proj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : D)
(T : C ⥤ D) :
The obvious projection functor from structured arrows.
Equations
Instances for category_theory.structured_arrow.proj
@[simp]
theorem
category_theory.structured_arrow.proj_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : D)
(T : C ⥤ D)
(X : category_theory.comma (category_theory.functor.from_punit S) T) :
(category_theory.structured_arrow.proj S T).obj X = X.right
def
category_theory.structured_arrow.mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{Y : C}
{T : C ⥤ D}
(f : S ⟶ T.obj Y) :
Construct a structured arrow from a morphism.
@[simp]
theorem
category_theory.structured_arrow.mk_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{Y : C}
{T : C ⥤ D}
(f : S ⟶ T.obj Y) :
(category_theory.structured_arrow.mk f).left = {as := punit.star}
@[simp]
theorem
category_theory.structured_arrow.mk_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{Y : C}
{T : C ⥤ D}
(f : S ⟶ T.obj Y) :
@[simp]
theorem
category_theory.structured_arrow.mk_hom_eq_self
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{Y : C}
{T : C ⥤ D}
(f : S ⟶ T.obj Y) :
@[simp]
theorem
category_theory.structured_arrow.w_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f : A ⟶ B)
{X' : D}
(f' : T.obj B.right ⟶ X') :
@[simp]
theorem
category_theory.structured_arrow.w
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f : A ⟶ B) :
def
category_theory.structured_arrow.hom_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ⟶ f'.right)
(w : f.hom ≫ T.map g = f'.hom) :
f ⟶ f'
To construct a morphism of structured arrows, we need a morphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- category_theory.structured_arrow.hom_mk g w = {left := category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1, right := g, w' := _}
Instances for category_theory.structured_arrow.hom_mk
@[simp]
theorem
category_theory.structured_arrow.hom_mk_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ⟶ f'.right)
(w : f.hom ≫ T.map g = f'.hom) :
(category_theory.structured_arrow.hom_mk g w).left = category_theory.eq_to_hom category_theory.structured_arrow.hom_mk._proof_1
@[simp]
theorem
category_theory.structured_arrow.hom_mk_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ⟶ f'.right)
(w : f.hom ≫ T.map g = f'.hom) :
def
category_theory.structured_arrow.hom_mk'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{X : D}
{Y : C}
(U : category_theory.structured_arrow X F)
(f : U.right ⟶ Y) :
U ⟶ category_theory.structured_arrow.mk (U.hom ≫ F.map f)
Given a structured arrow X ⟶ F(U), and an arrow U ⟶ Y, we can construct a morphism of
structured arrow given by (X ⟶ F(U)) ⟶ (X ⟶ F(U) ⟶ F(Y)).
@[simp]
theorem
category_theory.structured_arrow.iso_mk_inv_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ≅ f'.right)
(w : f.hom ≫ T.map g.hom = f'.hom) :
def
category_theory.structured_arrow.iso_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ≅ f'.right)
(w : f.hom ≫ T.map g.hom = f'.hom) :
f ≅ f'
To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes.
Equations
- category_theory.structured_arrow.iso_mk g w = category_theory.comma.iso_mk (category_theory.eq_to_iso category_theory.structured_arrow.iso_mk._proof_1) g _
@[simp]
theorem
category_theory.structured_arrow.iso_mk_inv_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ≅ f'.right)
(w : f.hom ≫ T.map g.hom = f'.hom) :
@[simp]
theorem
category_theory.structured_arrow.iso_mk_hom_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ≅ f'.right)
(w : f.hom ≫ T.map g.hom = f'.hom) :
(category_theory.structured_arrow.iso_mk g w).hom.left = category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
@[simp]
theorem
category_theory.structured_arrow.iso_mk_hom_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f f' : category_theory.structured_arrow S T}
(g : f.right ≅ f'.right)
(w : f.hom ≫ T.map g.hom = f'.hom) :
theorem
category_theory.structured_arrow.ext
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f g : A ⟶ B) :
theorem
category_theory.structured_arrow.ext_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f g : A ⟶ B) :
@[protected, instance]
def
category_theory.structured_arrow.proj_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D} :
theorem
category_theory.structured_arrow.mono_of_mono_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f : A ⟶ B)
[h : category_theory.mono f.right] :
The converse of this is true with additional assumptions, see mono_iff_mono_right.
theorem
category_theory.structured_arrow.epi_of_epi_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f : A ⟶ B)
[h : category_theory.epi f.right] :
@[protected, instance]
def
category_theory.structured_arrow.mono_hom_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f : A.right ⟶ B.right)
(w : A.hom ≫ T.map f = B.hom)
[h : category_theory.mono f] :
@[protected, instance]
def
category_theory.structured_arrow.epi_hom_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{A B : category_theory.structured_arrow S T}
(f : A.right ⟶ B.right)
(w : A.hom ≫ T.map f = B.hom)
[h : category_theory.epi f] :
theorem
category_theory.structured_arrow.eq_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
(f : category_theory.structured_arrow S T) :
Eta rule for structured arrows. Prefer structured_arrow.eta, since equality of objects tends
to cause problems.
@[simp]
theorem
category_theory.structured_arrow.eta_inv_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
(f : category_theory.structured_arrow S T) :
@[simp]
theorem
category_theory.structured_arrow.eta_hom_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
(f : category_theory.structured_arrow S T) :
f.eta.hom.left = category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
def
category_theory.structured_arrow.eta
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
(f : category_theory.structured_arrow S T) :
Eta rule for structured arrows.
Equations
@[simp]
theorem
category_theory.structured_arrow.eta_inv_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
(f : category_theory.structured_arrow S T) :
@[simp]
theorem
category_theory.structured_arrow.eta_hom_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
(f : category_theory.structured_arrow S T) :
def
category_theory.structured_arrow.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{T : C ⥤ D}
(f : S ⟶ S') :
A morphism between source objects S ⟶ S'
contravariantly induces a functor between structured arrows,
structured_arrow S' T ⥤ structured_arrow S T.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat.
@[simp]
theorem
category_theory.structured_arrow.map_map_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{T : C ⥤ D}
(f : S ⟶ S')
(X Y : category_theory.comma (category_theory.functor.from_punit S') T)
(f_1 : X ⟶ Y) :
((category_theory.structured_arrow.map f).map f_1).left = f_1.left
@[simp]
theorem
category_theory.structured_arrow.map_obj_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{T : C ⥤ D}
(f : S ⟶ S')
(X : category_theory.comma (category_theory.functor.from_punit S') T) :
((category_theory.structured_arrow.map f).obj X).right = X.right
@[simp]
theorem
category_theory.structured_arrow.map_map_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{T : C ⥤ D}
(f : S ⟶ S')
(X Y : category_theory.comma (category_theory.functor.from_punit S') T)
(f_1 : X ⟶ Y) :
((category_theory.structured_arrow.map f).map f_1).right = f_1.right
@[simp]
theorem
category_theory.structured_arrow.map_obj_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{T : C ⥤ D}
(f : S ⟶ S')
(X : category_theory.comma (category_theory.functor.from_punit S') T) :
@[simp]
theorem
category_theory.structured_arrow.map_obj_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{T : C ⥤ D}
(f : S ⟶ S')
(X : category_theory.comma (category_theory.functor.from_punit S') T) :
((category_theory.structured_arrow.map f).obj X).left = X.left
@[simp]
theorem
category_theory.structured_arrow.map_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' : D}
{Y : C}
{T : C ⥤ D}
{f : S' ⟶ T.obj Y}
(g : S ⟶ S') :
@[simp]
theorem
category_theory.structured_arrow.map_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{f : category_theory.structured_arrow S T} :
(category_theory.structured_arrow.map (𝟙 S)).obj f = f
@[simp]
theorem
category_theory.structured_arrow.map_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S S' S'' : D}
{T : C ⥤ D}
{f : S ⟶ S'}
{f' : S' ⟶ S''}
{h : category_theory.structured_arrow S'' T} :
(category_theory.structured_arrow.map (f ≫ f')).obj h = (category_theory.structured_arrow.map f).obj ((category_theory.structured_arrow.map f').obj h)
@[protected, instance]
def
category_theory.structured_arrow.proj_reflects_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D} :
def
category_theory.structured_arrow.mk_id_initial
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{Y : C}
{T : C ⥤ D}
[category_theory.full T]
[category_theory.faithful T] :
The identity structured arrow is initial.
Equations
- category_theory.structured_arrow.mk_id_initial = {desc := λ (c : category_theory.limits.cocone (category_theory.functor.empty (category_theory.structured_arrow (T.obj Y) T))), category_theory.structured_arrow.hom_mk (T.preimage c.X.hom) _, fac' := _, uniq' := _}
@[simp]
theorem
category_theory.structured_arrow.pre_obj_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : D)
(F : B ⥤ C)
(G : C ⥤ D)
(X : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G)) :
((category_theory.structured_arrow.pre S F G).obj X).hom = X.hom
@[simp]
theorem
category_theory.structured_arrow.pre_obj_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : D)
(F : B ⥤ C)
(G : C ⥤ D)
(X : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G)) :
((category_theory.structured_arrow.pre S F G).obj X).left = X.left
@[simp]
theorem
category_theory.structured_arrow.pre_obj_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : D)
(F : B ⥤ C)
(G : C ⥤ D)
(X : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G)) :
@[simp]
theorem
category_theory.structured_arrow.pre_map_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : D)
(F : B ⥤ C)
(G : C ⥤ D)
(X Y : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G))
(f : X ⟶ Y) :
((category_theory.structured_arrow.pre S F G).map f).left = f.left
def
category_theory.structured_arrow.pre
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : D)
(F : B ⥤ C)
(G : C ⥤ D) :
The functor (S, F ⋙ G) ⥤ (S, G).
Equations
@[simp]
theorem
category_theory.structured_arrow.pre_map_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : D)
(F : B ⥤ C)
(G : C ⥤ D)
(X Y : category_theory.comma (category_theory.functor.from_punit S) (F ⋙ G))
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.structured_arrow.post_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : C)
(F : B ⥤ C)
(G : C ⥤ D)
(X : category_theory.structured_arrow S F) :
(category_theory.structured_arrow.post S F G).obj X = category_theory.structured_arrow.mk (G.map X.hom)
@[simp]
theorem
category_theory.structured_arrow.post_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : C)
(F : B ⥤ C)
(G : C ⥤ D)
(X Y : category_theory.structured_arrow S F)
(f : X ⟶ Y) :
def
category_theory.structured_arrow.post
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(S : C)
(F : B ⥤ C)
(G : C ⥤ D) :
category_theory.structured_arrow S F ⥤ category_theory.structured_arrow (G.obj S) (F ⋙ G)
The functor (S, F) ⥤ (G(S), F ⋙ G).
Equations
- category_theory.structured_arrow.post S F G = {obj := λ (X : category_theory.structured_arrow S F), category_theory.structured_arrow.mk (G.map X.hom), map := λ (X Y : category_theory.structured_arrow S F) (f : X ⟶ Y), category_theory.structured_arrow.hom_mk f.right _, map_id' := _, map_comp' := _}
@[protected, instance]
def
category_theory.structured_arrow.small_proj_preimage_of_locally_small
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{S : D}
{T : C ⥤ D}
{𝒢 : set C}
[small ↥𝒢]
[category_theory.locally_small D] :
small ↥((category_theory.structured_arrow.proj S T).obj ⁻¹' 𝒢)
@[nolint]
def
category_theory.costructured_arrow
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : C ⥤ D)
(T : D) :
Type (max u₁ v₂)
The category of S-costructured arrows with target T : D (here S : C ⥤ D),
has as its objects D-morphisms of the form S Y ⟶ T, for some Y : C,
and morphisms C-morphisms Y ⟶ Y' making the obvious triangle commute.
Equations
Instances for category_theory.costructured_arrow
@[protected, instance]
def
category_theory.costructured_arrow.category
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : C ⥤ D)
(T : D) :
@[simp]
theorem
category_theory.costructured_arrow.proj_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : C ⥤ D)
(T : D)
(X : category_theory.comma S (category_theory.functor.from_punit T)) :
(category_theory.costructured_arrow.proj S T).obj X = X.left
def
category_theory.costructured_arrow.proj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : C ⥤ D)
(T : D) :
The obvious projection functor from costructured arrows.
Equations
Instances for category_theory.costructured_arrow.proj
@[simp]
theorem
category_theory.costructured_arrow.proj_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(S : C ⥤ D)
(T : D)
(_x _x_1 : category_theory.comma S (category_theory.functor.from_punit T))
(f : _x ⟶ _x_1) :
(category_theory.costructured_arrow.proj S T).map f = f.left
def
category_theory.costructured_arrow.mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{Y : C}
{S : C ⥤ D}
(f : S.obj Y ⟶ T) :
Construct a costructured arrow from a morphism.
@[simp]
theorem
category_theory.costructured_arrow.mk_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{Y : C}
{S : C ⥤ D}
(f : S.obj Y ⟶ T) :
@[simp]
theorem
category_theory.costructured_arrow.mk_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{Y : C}
{S : C ⥤ D}
(f : S.obj Y ⟶ T) :
(category_theory.costructured_arrow.mk f).right = {as := punit.star}
@[simp]
theorem
category_theory.costructured_arrow.mk_hom_eq_self
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{Y : C}
{S : C ⥤ D}
(f : S.obj Y ⟶ T) :
@[simp]
theorem
category_theory.costructured_arrow.w
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f : A ⟶ B) :
@[simp]
theorem
category_theory.costructured_arrow.w_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f : A ⟶ B)
{X' : D}
(f' : (category_theory.functor.from_punit T).obj B.right ⟶ X') :
@[simp]
theorem
category_theory.costructured_arrow.hom_mk_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ⟶ f'.left)
(w : S.map g ≫ f'.hom = f.hom) :
(category_theory.costructured_arrow.hom_mk g w).right = category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1
def
category_theory.costructured_arrow.hom_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ⟶ f'.left)
(w : S.map g ≫ f'.hom = f.hom) :
f ⟶ f'
To construct a morphism of costructured arrows, we need a morphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- category_theory.costructured_arrow.hom_mk g w = {left := g, right := category_theory.eq_to_hom category_theory.costructured_arrow.hom_mk._proof_1, w' := _}
Instances for category_theory.costructured_arrow.hom_mk
@[simp]
theorem
category_theory.costructured_arrow.hom_mk_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ⟶ f'.left)
(w : S.map g ≫ f'.hom = f.hom) :
@[simp]
theorem
category_theory.costructured_arrow.iso_mk_inv_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ≅ f'.left)
(w : S.map g.hom ≫ f'.hom = f.hom) :
@[simp]
theorem
category_theory.costructured_arrow.iso_mk_hom_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ≅ f'.left)
(w : S.map g.hom ≫ f'.hom = f.hom) :
(category_theory.costructured_arrow.iso_mk g w).hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[simp]
theorem
category_theory.costructured_arrow.iso_mk_inv_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ≅ f'.left)
(w : S.map g.hom ≫ f'.hom = f.hom) :
def
category_theory.costructured_arrow.iso_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ≅ f'.left)
(w : S.map g.hom ≫ f'.hom = f.hom) :
f ≅ f'
To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, and to check that the triangle commutes.
Equations
- category_theory.costructured_arrow.iso_mk g w = category_theory.comma.iso_mk g (category_theory.eq_to_iso category_theory.costructured_arrow.iso_mk._proof_1) _
@[simp]
theorem
category_theory.costructured_arrow.iso_mk_hom_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f f' : category_theory.costructured_arrow S T}
(g : f.left ≅ f'.left)
(w : S.map g.hom ≫ f'.hom = f.hom) :
theorem
category_theory.costructured_arrow.ext
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f g : A ⟶ B)
(h : f.left = g.left) :
f = g
theorem
category_theory.costructured_arrow.ext_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f g : A ⟶ B) :
@[protected, instance]
def
category_theory.costructured_arrow.proj_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D} :
theorem
category_theory.costructured_arrow.mono_of_mono_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f : A ⟶ B)
[h : category_theory.mono f.left] :
theorem
category_theory.costructured_arrow.epi_of_epi_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f : A ⟶ B)
[h : category_theory.epi f.left] :
The converse of this is true with additional assumptions, see epi_iff_epi_left.
@[protected, instance]
def
category_theory.costructured_arrow.mono_hom_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f : A.left ⟶ B.left)
(w : S.map f ≫ B.hom = A.hom)
[h : category_theory.mono f] :
@[protected, instance]
def
category_theory.costructured_arrow.epi_hom_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{A B : category_theory.costructured_arrow S T}
(f : A.left ⟶ B.left)
(w : S.map f ≫ B.hom = A.hom)
[h : category_theory.epi f] :
theorem
category_theory.costructured_arrow.eq_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
(f : category_theory.costructured_arrow S T) :
Eta rule for costructured arrows. Prefer costructured_arrow.eta, as equality of objects tends
to cause problems.
@[simp]
theorem
category_theory.costructured_arrow.eta_hom_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
(f : category_theory.costructured_arrow S T) :
f.eta.hom.right = category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[simp]
theorem
category_theory.costructured_arrow.eta_inv_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
(f : category_theory.costructured_arrow S T) :
@[simp]
theorem
category_theory.costructured_arrow.eta_hom_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
(f : category_theory.costructured_arrow S T) :
@[simp]
theorem
category_theory.costructured_arrow.eta_inv_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
(f : category_theory.costructured_arrow S T) :
def
category_theory.costructured_arrow.eta
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
(f : category_theory.costructured_arrow S T) :
Eta rule for costructured arrows.
Equations
@[simp]
theorem
category_theory.costructured_arrow.map_map_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{S : C ⥤ D}
(f : T ⟶ T')
(X Y : category_theory.comma S (category_theory.functor.from_punit T))
(f_1 : X ⟶ Y) :
((category_theory.costructured_arrow.map f).map f_1).right = f_1.right
@[simp]
theorem
category_theory.costructured_arrow.map_obj_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{S : C ⥤ D}
(f : T ⟶ T')
(X : category_theory.comma S (category_theory.functor.from_punit T)) :
def
category_theory.costructured_arrow.map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{S : C ⥤ D}
(f : T ⟶ T') :
A morphism between target objects T ⟶ T'
covariantly induces a functor between costructured arrows,
costructured_arrow S T ⥤ costructured_arrow S T'.
Ideally this would be described as a 2-functor from D
(promoted to a 2-category with equations as 2-morphisms)
to Cat.
@[simp]
theorem
category_theory.costructured_arrow.map_obj_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{S : C ⥤ D}
(f : T ⟶ T')
(X : category_theory.comma S (category_theory.functor.from_punit T)) :
((category_theory.costructured_arrow.map f).obj X).right = X.right
@[simp]
theorem
category_theory.costructured_arrow.map_map_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{S : C ⥤ D}
(f : T ⟶ T')
(X Y : category_theory.comma S (category_theory.functor.from_punit T))
(f_1 : X ⟶ Y) :
((category_theory.costructured_arrow.map f).map f_1).left = f_1.left
@[simp]
theorem
category_theory.costructured_arrow.map_obj_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{S : C ⥤ D}
(f : T ⟶ T')
(X : category_theory.comma S (category_theory.functor.from_punit T)) :
((category_theory.costructured_arrow.map f).obj X).left = X.left
@[simp]
theorem
category_theory.costructured_arrow.map_mk
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' : D}
{Y : C}
{S : C ⥤ D}
{f : S.obj Y ⟶ T}
(g : T ⟶ T') :
@[simp]
theorem
category_theory.costructured_arrow.map_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{f : category_theory.costructured_arrow S T} :
(category_theory.costructured_arrow.map (𝟙 T)).obj f = f
@[simp]
theorem
category_theory.costructured_arrow.map_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T T' T'' : D}
{S : C ⥤ D}
{f : T ⟶ T'}
{f' : T' ⟶ T''}
{h : category_theory.costructured_arrow S T} :
@[protected, instance]
def
category_theory.costructured_arrow.proj_reflects_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D} :
def
category_theory.costructured_arrow.mk_id_terminal
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{Y : C}
{S : C ⥤ D}
[category_theory.full S]
[category_theory.faithful S] :
The identity costructured arrow is terminal.
Equations
- category_theory.costructured_arrow.mk_id_terminal = {lift := λ (c : category_theory.limits.cone (category_theory.functor.empty (category_theory.costructured_arrow S (S.obj Y)))), category_theory.costructured_arrow.hom_mk (S.preimage c.X.hom) _, fac' := _, uniq' := _}
@[simp]
theorem
category_theory.costructured_arrow.pre_obj_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : D)
(X : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) :
((category_theory.costructured_arrow.pre F G S).obj X).hom = X.hom
@[simp]
theorem
category_theory.costructured_arrow.pre_obj_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : D)
(X : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) :
((category_theory.costructured_arrow.pre F G S).obj X).right = X.right
def
category_theory.costructured_arrow.pre
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : D) :
The functor (F ⋙ G, S) ⥤ (G, S).
Equations
@[simp]
theorem
category_theory.costructured_arrow.pre_map_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : D)
(X Y : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S))
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.costructured_arrow.pre_map_right
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : D)
(X Y : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S))
(f : X ⟶ Y) :
((category_theory.costructured_arrow.pre F G S).map f).right = f.right
@[simp]
theorem
category_theory.costructured_arrow.pre_obj_left
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : D)
(X : category_theory.comma (F ⋙ G) (category_theory.functor.from_punit S)) :
@[simp]
theorem
category_theory.costructured_arrow.post_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : C)
(X Y : category_theory.costructured_arrow F S)
(f : X ⟶ Y) :
def
category_theory.costructured_arrow.post
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : C) :
category_theory.costructured_arrow F S ⥤ category_theory.costructured_arrow (F ⋙ G) (G.obj S)
The functor (F, S) ⥤ (F ⋙ G, G(S)).
Equations
- category_theory.costructured_arrow.post F G S = {obj := λ (X : category_theory.costructured_arrow F S), category_theory.costructured_arrow.mk (G.map X.hom), map := λ (X Y : category_theory.costructured_arrow F S) (f : X ⟶ Y), category_theory.costructured_arrow.hom_mk f.left _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.costructured_arrow.post_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{B : Type u₄}
[category_theory.category B]
(F : B ⥤ C)
(G : C ⥤ D)
(S : C)
(X : category_theory.costructured_arrow F S) :
@[protected, instance]
def
category_theory.costructured_arrow.small_proj_preimage_of_locally_small
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{T : D}
{S : C ⥤ D}
{𝒢 : set C}
[small ↥𝒢]
[category_theory.locally_small D] :
small ↥((category_theory.costructured_arrow.proj S T).obj ⁻¹' 𝒢)
@[simp]
theorem
category_theory.structured_arrow.to_costructured_arrow_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X : (category_theory.structured_arrow d F)ᵒᵖ) :
@[simp]
theorem
category_theory.structured_arrow.to_costructured_arrow_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X Y : (category_theory.structured_arrow d F)ᵒᵖ)
(f : X ⟶ Y) :
def
category_theory.structured_arrow.to_costructured_arrow
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D) :
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of structured arrows d ⟶ F.obj c to the category of costructured arrows
F.op.obj c ⟶ (op d).
Equations
- category_theory.structured_arrow.to_costructured_arrow F d = {obj := λ (X : (category_theory.structured_arrow d F)ᵒᵖ), category_theory.costructured_arrow.mk (opposite.unop X).hom.op, map := λ (X Y : (category_theory.structured_arrow d F)ᵒᵖ) (f : X ⟶ Y), category_theory.costructured_arrow.hom_mk f.unop.right.op _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.structured_arrow.to_costructured_arrow'_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X Y : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.structured_arrow.to_costructured_arrow'_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ) :
def
category_theory.structured_arrow.to_costructured_arrow'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D) :
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of structured arrows op d ⟶ F.op.obj c to the category of costructured arrows
F.obj c ⟶ d.
Equations
- category_theory.structured_arrow.to_costructured_arrow' F d = {obj := λ (X : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ), category_theory.costructured_arrow.mk (opposite.unop X).hom.unop, map := λ (X Y : (category_theory.structured_arrow (opposite.op d) F.op)ᵒᵖ) (f : X ⟶ Y), category_theory.costructured_arrow.hom_mk f.unop.right.unop _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.costructured_arrow.to_structured_arrow_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X Y : (category_theory.costructured_arrow F d)ᵒᵖ)
(f : X ⟶ Y) :
def
category_theory.costructured_arrow.to_structured_arrow
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D) :
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of costructured arrows F.obj c ⟶ d to the category of structured arrows
op d ⟶ F.op.obj c.
Equations
- category_theory.costructured_arrow.to_structured_arrow F d = {obj := λ (X : (category_theory.costructured_arrow F d)ᵒᵖ), category_theory.structured_arrow.mk (opposite.unop X).hom.op, map := λ (X Y : (category_theory.costructured_arrow F d)ᵒᵖ) (f : X ⟶ Y), category_theory.structured_arrow.hom_mk f.unop.left.op _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.costructured_arrow.to_structured_arrow_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X : (category_theory.costructured_arrow F d)ᵒᵖ) :
def
category_theory.costructured_arrow.to_structured_arrow'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D) :
For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the
category of costructured arrows F.op.obj c ⟶ op d to the category of structured arrows
d ⟶ F.obj c.
Equations
- category_theory.costructured_arrow.to_structured_arrow' F d = {obj := λ (X : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ), category_theory.structured_arrow.mk (opposite.unop X).hom.unop, map := λ (X Y : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ) (f : X ⟶ Y), category_theory.structured_arrow.hom_mk f.unop.left.unop _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.costructured_arrow.to_structured_arrow'_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ) :
@[simp]
theorem
category_theory.costructured_arrow.to_structured_arrow'_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D)
(X Y : (category_theory.costructured_arrow F.op (opposite.op d))ᵒᵖ)
(f : X ⟶ Y) :
def
category_theory.structured_arrow_op_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D) :
For a functor F : C ⥤ D and an object d : D, the category of structured arrows d ⟶ F.obj c
is contravariantly equivalent to the category of costructured arrows F.op.obj c ⟶ op d.
Equations
- category_theory.structured_arrow_op_equivalence F d = category_theory.equivalence.mk (category_theory.structured_arrow.to_costructured_arrow F d) (category_theory.costructured_arrow.to_structured_arrow' F d).right_op (category_theory.nat_iso.of_components (λ (X : (category_theory.structured_arrow d F)ᵒᵖ), (category_theory.structured_arrow.iso_mk (category_theory.iso.refl (category_theory.structured_arrow.mk (opposite.unop X).hom).right) _).op) _) (category_theory.nat_iso.of_components (λ (X : category_theory.costructured_arrow F.op (opposite.op d)), category_theory.costructured_arrow.iso_mk (category_theory.iso.refl (category_theory.costructured_arrow.mk X.hom).left) _) _)
def
category_theory.costructured_arrow_op_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(d : D) :
For a functor F : C ⥤ D and an object d : D, the category of costructured arrows
F.obj c ⟶ d is contravariantly equivalent to the category of structured arrows
op d ⟶ F.op.obj c.
Equations
- category_theory.costructured_arrow_op_equivalence F d = category_theory.equivalence.mk (category_theory.costructured_arrow.to_structured_arrow F d) (category_theory.structured_arrow.to_costructured_arrow' F d).right_op (category_theory.nat_iso.of_components (λ (X : (category_theory.costructured_arrow F d)ᵒᵖ), (category_theory.costructured_arrow.iso_mk (category_theory.iso.refl (category_theory.costructured_arrow.mk (opposite.unop X).hom).left) _).op) _) (category_theory.nat_iso.of_components (λ (X : category_theory.structured_arrow (opposite.op d) F.op), category_theory.structured_arrow.iso_mk (category_theory.iso.refl (category_theory.structured_arrow.mk X.hom).right) _) _)