feat(category): structured arrows (#6830)

Factored out from #6820.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/elements.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.comma
+import category_theory.structured_arrow
 import category_theory.groupoid
 import category_theory.punit
 
@@ -20,7 +20,7 @@ A morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C`, so `F.map f`
 
 This construction is equivalent to a special case of a comma construction, so this is mostly just a
 more convenient API. We prove the equivalence in
-`category_theory.category_of_elements.comma_equivalence`.
+`category_theory.category_of_elements.structured_arrow_equivalence`.
 
 ## References
 * [Emily Riehl, *Category Theory in Context*, Section 2.4][riehl2017]
@@ -92,36 +92,34 @@ def map {F₁ F₂ : C ⥤ Type w} (α : F₁ ⟶ F₂) : F₁.elements ⥤ F₂
 @[simp] lemma map_π {F₁ F₂ : C ⥤ Type w} (α : F₁ ⟶ F₂) : map α ⋙ π F₂ = π F₁ := rfl
 
 /-- The forward direction of the equivalence `F.elements ≅ (*, F)`. -/
-def to_comma : F.elements ⥤ comma (functor.from_punit punit) F :=
-{ obj := λ X, { left := punit.star, right := X.1, hom := λ _, X.2 },
-  map := λ X Y f, { right := f.val } }
+def to_structured_arrow : F.elements ⥤ structured_arrow punit F :=
+{ obj := λ X, structured_arrow.mk (λ _, X.2),
+  map := λ X Y f, structured_arrow.hom_mk f.val (by tidy) }
 
-@[simp] lemma to_comma_obj (X) :
-  (to_comma F).obj X = { left := punit.star, right := X.1, hom := λ _, X.2 } := rfl
-@[simp] lemma to_comma_map {X Y} (f : X ⟶ Y) :
-  (to_comma F).map f = { right := f.val } := rfl
+@[simp] lemma to_structured_arrow_obj (X) :
+  (to_structured_arrow F).obj X = { left := punit.star, right := X.1, hom := λ _, X.2 } := rfl
+@[simp] lemma to_comma_map_right {X Y} (f : X ⟶ Y) :
+  ((to_structured_arrow F).map f).right = f.val := rfl
 
 /-- The reverse direction of the equivalence `F.elements ≅ (*, F)`. -/
-def from_comma : comma (functor.from_punit punit) F ⥤ F.elements :=
+def from_structured_arrow : structured_arrow punit F ⥤ F.elements :=
 { obj := λ X, ⟨X.right, X.hom (punit.star)⟩,
   map := λ X Y f, ⟨f.right, congr_fun f.w'.symm punit.star⟩ }
 
-@[simp] lemma from_comma_obj (X) :
-  (from_comma F).obj X = ⟨X.right, X.hom (punit.star)⟩ := rfl
-@[simp] lemma from_comma_map {X Y} (f : X ⟶ Y) :
-  (from_comma F).map f = ⟨f.right, congr_fun f.w'.symm punit.star⟩ := rfl
+@[simp] lemma from_structured_arrow_obj (X) :
+  (from_structured_arrow F).obj X = ⟨X.right, X.hom (punit.star)⟩ := rfl
+@[simp] lemma from_structured_arrow_map {X Y} (f : X ⟶ Y) :
+  (from_structured_arrow F).map f = ⟨f.right, congr_fun f.w'.symm punit.star⟩ := rfl
 
 /-- The equivalence between the category of elements `F.elements`
     and the comma category `(*, F)`. -/
-def comma_equivalence : F.elements ≌ comma (functor.from_punit punit) F :=
-equivalence.mk (to_comma F) (from_comma F)
+@[simps]
+def structured_arrow_equivalence : F.elements ≌ structured_arrow punit F :=
+equivalence.mk (to_structured_arrow F) (from_structured_arrow F)
   (nat_iso.of_components (λ X, eq_to_iso (by tidy)) (by tidy))
   (nat_iso.of_components
     (λ X, { hom := { right := 𝟙 _ }, inv := { right := 𝟙 _ } })
     (by tidy))
 
-@[simp] lemma comma_equivalence_functor : (comma_equivalence F).functor = to_comma F := rfl
-@[simp] lemma comma_equivalence_inverse : (comma_equivalence F).inverse = from_comma F := rfl
-
 end category_of_elements
 end category_theory

src/category_theory/limits/cofinal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.punit
-import category_theory.comma
+import category_theory.structured_arrow
 import category_theory.is_connected
 import category_theory.limits.yoneda
 import category_theory.limits.types
@@ -69,15 +69,15 @@ is connected.
 See https://stacks.math.columbia.edu/tag/04E6
 -/
 class cofinal (F : C ⥤ D) : Prop :=
-(out (d : D) : is_connected (comma (functor.from_punit d) F))
+(out (d : D) : is_connected (structured_arrow d F))
 
 attribute [instance] cofinal.out
 
 namespace cofinal
 
 variables (F : C ⥤ D) [cofinal F]
 
-instance (d : D) : nonempty (comma (functor.from_punit d) F) := is_connected.is_nonempty
+instance (d : D) : nonempty (structured_arrow d F) := is_connected.is_nonempty
 
 variables {E : Type u} [category.{v} E] (G : D ⥤ E)
 
@@ -86,14 +86,14 @@ When `F : C ⥤ D` is cofinal, we denote by `lift F d` an arbitrary choice of ob
 there exists a morphism `d ⟶ F.obj (lift F d)`.
 -/
 def lift (d : D) : C :=
-(classical.arbitrary (comma (functor.from_punit d) F)).right
+(classical.arbitrary (structured_arrow d F)).right
 
 /--
 When `F : C ⥤ D` is cofinal, we denote by `hom_to_lift` an arbitrary choice of morphism
 `d ⟶ F.obj (lift F d)`.
 -/
 def hom_to_lift (d : D) : d ⟶ F.obj (lift F d) :=
-(classical.arbitrary (comma (functor.from_punit d) F)).hom
+(classical.arbitrary (structured_arrow d F)).hom
 
 /--
 We provide an induction principle for reasoning about `lift` and `hom_to_lift`.
@@ -113,7 +113,7 @@ lemma induction {d : D} (Z : Π (X : C) (k : d ⟶ F.obj X), Prop)
 begin
   apply nonempty.some,
   apply @is_preconnected_induction _ _ _
-    (λ (Y : comma (functor.from_punit d) F), Z Y.right Y.hom) _ _ { right := X₀, hom := k₀, } z,
+    (λ (Y : structured_arrow d F), Z Y.right Y.hom) _ _ { right := X₀, hom := k₀, } z,
   { intros j₁ j₂ f a, fapply h₁ _ _ _ _ f.right _ a, convert f.w.symm, dsimp, simp, },
   { intros j₁ j₂ f a, fapply h₂ _ _ _ _ f.right _ a, convert f.w.symm, dsimp, simp, },
 end
@@ -420,9 +420,7 @@ as_iso (colimit.pre (coyoneda.obj (op d)) F) ≪≫ coyoneda.colimit_coyoneda_is
 
 lemma zigzag_of_eqv_gen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : Σ X, d ⟶ F.obj X}
   (t : eqv_gen (types.quot.rel (F ⋙ coyoneda.obj (op d))) f₁ f₂) :
-  zigzag
-    ({left := punit.star, right := f₁.1, hom := f₁.2} : comma (functor.from_punit d) F)
-    {left := punit.star, right := f₂.1, hom := f₂.2} :=
+  zigzag (structured_arrow.mk f₁.2) (structured_arrow.mk f₂.2) :=
 begin
   induction t,
   case eqv_gen.rel : x y r
@@ -447,10 +445,10 @@ If `colimit (F ⋙ coyoneda.obj (op d)) ≅ punit` for all `d : D`, then `F` is
 lemma cofinal_of_colimit_comp_coyoneda_iso_punit
   (I : Π d, colimit (F ⋙ coyoneda.obj (op d)) ≅ punit) : cofinal F :=
 ⟨λ d, begin
-  haveI : nonempty (comma (functor.from_punit d) F) := by
+  haveI : nonempty (structured_arrow d F) := by
   { have := (I d).inv punit.star,
     obtain ⟨j, y, rfl⟩ := limits.types.jointly_surjective' this,
-    exact ⟨{right := j, hom := y}⟩, },
+    exact ⟨structured_arrow.mk y⟩, },
   apply zigzag_is_connected,
   rintros ⟨⟨⟩,X₁,f₁⟩ ⟨⟨⟩,X₂,f₂⟩,
   dsimp at *,

src/category_theory/over.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Bhavik Mehta
 -/
-import category_theory.comma
+import category_theory.structured_arrow
 import category_theory.punit
 import category_theory.reflects_isomorphisms
 import category_theory.epi_mono
@@ -34,7 +34,7 @@ triangles.
 See https://stacks.math.columbia.edu/tag/001G.
 -/
 @[derive category]
-def over (X : T) := comma.{v₁ v₁ v₁} (𝟭 T) (functor.from_punit X)
+def over (X : T) := costructured_arrow (𝟭 T) X
 
 -- Satisfying the inhabited linter
 instance over.inhabited [inhabited T] : inhabited (over (default T)) :=
@@ -62,7 +62,7 @@ by have := f.w; tidy
 /-- To give an object in the over category, it suffices to give a morphism with codomain `X`. -/
 @[simps]
 def mk {X Y : T} (f : Y ⟶ X) : over X :=
-{ left := Y, hom := f }
+costructured_arrow.mk f
 
 /-- We can set up a coercion from arrows with codomain `X` to `over X`. This most likely should not
     be a global instance, but it is sometimes useful. -/
@@ -80,7 +80,7 @@ end
 @[simps]
 def hom_mk {U V : over X} (f : U.left ⟶ V.left) (w : f ≫ V.hom = U.hom . obviously) :
   U ⟶ V :=
-{ left := f }
+costructured_arrow.hom_mk f w
 
 /--
 Construct an isomorphism in the over category given isomorphisms of the objects whose forward
@@ -89,7 +89,7 @@ direction gives a commutative triangle.
 @[simps]
 def iso_mk {f g : over X} (hl : f.left ≅ g.left) (hw : hl.hom ≫ g.hom = f.hom . obviously) :
   f ≅ g :=
-comma.iso_mk hl (eq_to_iso (subsingleton.elim _ _)) (by simp [hw])
+costructured_arrow.iso_mk hl hw
 
 section
 variable (X)
@@ -228,7 +228,7 @@ end over
 /-- The under category has as objects arrows with domain `X` and as morphisms commutative
     triangles. -/
 @[derive category]
-def under (X : T) := comma.{v₁ v₁ v₁} (functor.from_punit X) (𝟭 T)
+def under (X : T) := structured_arrow X (𝟭 T)
 
 -- Satisfying the inhabited linter
 instance under.inhabited [inhabited T] : inhabited (under (default T)) :=
@@ -256,21 +256,21 @@ by have := f.w; tidy
 /-- To give an object in the under category, it suffices to give an arrow with domain `X`. -/
 @[simps]
 def mk {X Y : T} (f : X ⟶ Y) : under X :=
-{ right := Y, hom := f }
+structured_arrow.mk f
 
 /-- To give a morphism in the under category, it suffices to give a morphism fitting in a
     commutative triangle. -/
 @[simps]
 def hom_mk {U V : under X} (f : U.right ⟶ V.right) (w : U.hom ≫ f = V.hom . obviously) :
   U ⟶ V :=
-{ right := f }
+structured_arrow.hom_mk f w
 
 /--
 Construct an isomorphism in the over category given isomorphisms of the objects whose forward
 direction gives a commutative triangle.
 -/
 def iso_mk {f g : under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) : f ≅ g :=
-comma.iso_mk (eq_to_iso (subsingleton.elim _ _)) hr (by simp [hw])
+structured_arrow.iso_mk hr hw
 
 @[simp]
 lemma iso_mk_hom_right {f g : under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) :