lint(category_theory/adjunction): add doc-strings (#4415)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Oct 5, 2020 · 6a4fd24 · 6a4fd24
1 parent 17b607f
commit 6a4fd24
Show file tree

Hide file tree

Showing 2 changed files with 62 additions and 6 deletions.
diff --git a/src/category_theory/adjunction/basic.lean b/src/category_theory/adjunction/basic.lean
@@ -135,6 +135,12 @@ end adjunction
 
 namespace adjunction
 
+/--
+This is an auxiliary data structure useful for constructing adjunctions.
+See `adjunction.mk_of_hom_equiv`.
+This structure won't typically be used anywhere else.
+-/
+@[nolint has_inhabited_instance]
 structure core_hom_equiv (F : C ⥤ D) (G : D ⥤ C) :=
 (hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
 (hom_equiv_naturality_left_symm' : Π {X' X Y} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
@@ -160,6 +166,12 @@ by rw [equiv.symm_apply_eq]; simp
 
 end core_hom_equiv
 
+/--
+This is an auxiliary data structure useful for constructing adjunctions.
+See `adjunction.mk_of_hom_equiv`.
+This structure won't typically be used anywhere else.
+-/
+@[nolint has_inhabited_instance]
 structure core_unit_counit (F : C ⥤ D) (G : D ⥤ C) :=
 (unit : 𝟭 C ⟶ F.comp G)
 (counit : G.comp F ⟶ 𝟭 D)

diff --git a/src/category_theory/adjunction/limits.lean b/src/category_theory/adjunction/limits.lean
@@ -23,18 +23,34 @@ include adj
 section preservation_colimits
 variables {J : Type v} [small_category J] (K : J ⥤ C)
 
+/--
+The right adjoint of `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)`.
+
+Auxiliary definition for `functoriality_is_left_adjoint`.
+-/
 def functoriality_right_adjoint : cocone (K ⋙ F) ⥤ cocone K :=
 (cocones.functoriality _ G) ⋙
   (cocones.precompose (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv))
 
 local attribute [reducible] functoriality_right_adjoint
 
+/--
+The unit for the adjunction for `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)`.
+
+Auxiliary definition for `functoriality_is_left_adjoint`.
+-/
 @[simps] def functoriality_unit : 𝟭 (cocone K) ⟶ cocones.functoriality _ F ⋙ functoriality_right_adjoint adj K :=
 { app := λ c, { hom := adj.unit.app c.X } }
 
+/--
+The counit for the adjunction for `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)`.
+
+Auxiliary definition for `functoriality_is_left_adjoint`.
+-/
 @[simps] def functoriality_counit : functoriality_right_adjoint adj K ⋙ cocones.functoriality _ F ⟶ 𝟭 (cocone (K ⋙ F)) :=
 { app := λ c, { hom := adj.counit.app c.X } }
 
+/-- The functor `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)` is a left adjoint. -/
 def functoriality_is_left_adjoint :
   is_left_adjoint (cocones.functoriality K F) :=
 { right := functoriality_right_adjoint adj K,
@@ -83,18 +99,34 @@ end preservation_colimits
 section preservation_limits
 variables {J : Type v} [small_category J] (K : J ⥤ D)
 
+/--
+The left adjoint of `cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.
+
+Auxiliary definition for `functoriality_is_right_adjoint`.
+-/
 def functoriality_left_adjoint : cone (K ⋙ G) ⥤ cone K :=
 (cones.functoriality _ F) ⋙ (cones.postcompose
     ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom))
 
 local attribute [reducible] functoriality_left_adjoint
 
+/--
+The unit for the adjunction for`cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.
+
+Auxiliary definition for `functoriality_is_right_adjoint`.
+-/
 @[simps] def functoriality_unit' : 𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality _ G :=
 { app := λ c, { hom := adj.unit.app c.X, } }
 
+/--
+The counit for the adjunction for`cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.
+
+Auxiliary definition for `functoriality_is_right_adjoint`.
+-/
 @[simps] def functoriality_counit' : cones.functoriality _ G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
 { app := λ c, { hom := adj.counit.app c.X, } }
 
+/-- The functor `cones.functoriality K G : cone K ⥤ cone (K ⋙ G)` is a right adjoint. -/
 def functoriality_is_right_adjoint :
   is_right_adjoint (cones.functoriality K G) :=
 { left := functoriality_left_adjoint adj K,
@@ -182,6 +214,12 @@ def cocones_iso_component_inv {J : Type v} [small_category J] {K : J ⥤ C}
     dsimp, simp
   end }
 
+/--
+When `F ⊣ G`,
+the functor associating to each `Y` the cocones over `K ⋙ F` with cone point `Y`
+is naturally isomorphic to
+the functor associating to each `Y` the cocones over `K` with cone point `G.obj Y`.
+-/
 -- Note: this is natural in K, but we do not yet have the tools to formulate that.
 def cocones_iso {J : Type v} [small_category J] {K : J ⥤ C} :
   (cocones J D).obj (op (K ⋙ F)) ≅ G ⋙ ((cocones J C).obj (op K)) :=
@@ -195,12 +233,12 @@ nat_iso.of_components (λ Y,
 def cones_iso_component_hom {J : Type v} [small_category J] {K : J ⥤ D}
   (X : Cᵒᵖ) (t : (functor.op F ⋙ (cones J D).obj K).obj X) :
   ((cones J C).obj (K ⋙ G)).obj X :=
-  { app := λ j, (adj.hom_equiv (unop X) (K.obj j)) (t.app j),
-    naturality' := λ j j' f,
-    begin
-      erw [← adj.hom_equiv_naturality_right, ← t.naturality, category.id_comp, category.id_comp],
-      refl
-    end }
+{ app := λ j, (adj.hom_equiv (unop X) (K.obj j)) (t.app j),
+  naturality' := λ j j' f,
+  begin
+    erw [← adj.hom_equiv_naturality_right, ← t.naturality, category.id_comp, category.id_comp],
+    refl
+  end }
 
 /-- auxiliary construction for `cones_iso` -/
 @[simps]
@@ -214,6 +252,12 @@ def cones_iso_component_inv {J : Type v} [small_category J] {K : J ⥤ D}
   end }
 
 -- Note: this is natural in K, but we do not yet have the tools to formulate that.
+/--
+When `F ⊣ G`,
+the functor associating to each `X` the cones over `K` with cone point `F.op.obj X`
+is naturally isomorphic to
+the functor associating to each `X` the cones over `K ⋙ G` with cone point `X`.
+-/
 def cones_iso {J : Type v} [small_category J] {K : J ⥤ D} :
   F.op ⋙ ((cones J D).obj K) ≅ (cones J C).obj (K ⋙ G) :=
 nat_iso.of_components (λ X,